closure_rels_subset_ker — Mathlib

English

If a map f: α → G sends every rel r to the identity, then the normal closure of rels lies inside the kernel of the corresponding homomorphism.

Русский

Если отображение f отправляет каждое отношение в единицу, то нормальное замыкание rels подпадает под ядро гомоморфизма.

LaTeX

$$If $\forall r\in \mathrm{rels}, \mathrm{FreeGroup.lift}(f,r) = 1$, then $\mathrm{normalClosure}(\mathrm{rels}) \le \ker F$.$$

Lean4

theorem closure_rels_subset_ker (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    Subgroup.normalClosure rels ≤ MonoidHom.ker F :=
  Subgroup.normalClosure_le_normal fun x w ↦ MonoidHom.mem_ker.2 (h x w)

Похожие утверждения