subgroup_closure_range_simple — Mathlib

English

There is a group isomorphism between (M.reindex e).Group and M.Group, given by the natural transport of generators under e.

Русский

Существует изоморфизм групп между (M.reindex e).Group и M.Group, реализованный естественным переносом генераторов через e.

LaTeX

$$$(M.\mathrm{reindex}~e).\mathrm{Group} \cong M.\mathrm{Group}$$$

Lean4

/-- The simple reflections of `W` generate `W` as a group. -/
theorem subgroup_closure_range_simple : Subgroup.closure (range cs.simple) = ⊤ :=
  by
  have : cs.simple = cs.mulEquiv.symm ∘ PresentedGroup.of := rfl
  rw [this, Set.range_comp, ← MulEquiv.coe_toMonoidHom, ← MonoidHom.map_closure, PresentedGroup.closure_range_of, ←
    MonoidHom.range_eq_map]
  exact MonoidHom.range_eq_top.2 (MulEquiv.surjective _)

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