equivPresentedGroup — Mathlib

English

Presented groups are isomorphic when their generator types are isomorphic via an equivalence.

Русский

Представленные группы изоморфны при изоморфизме типов генераторов.

LaTeX

$$equivPresentedGroup rels e : PresentedGroup rels ≃* PresentedGroup (FreeGroupCongr e '' rels)$$

Lean4

/-- Presented groups of isomorphic types are isomorphic. -/
def equivPresentedGroup (rels : Set (FreeGroup α)) (e : α ≃ β) :
    PresentedGroup rels ≃* PresentedGroup (FreeGroup.freeGroupCongr e '' rels) :=
  QuotientGroup.congr (Subgroup.normalClosure rels) (Subgroup.normalClosure ((FreeGroup.freeGroupCongr e) '' rels))
    (FreeGroup.freeGroupCongr e)
    (Subgroup.map_normalClosure rels (FreeGroup.freeGroupCongr e).toMonoidHom (FreeGroup.freeGroupCongr e).surjective)

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