English
There is an isomorphism of groups between the Coxeter group of the reindexed matrix and the Coxeter group of the original matrix.
Русский
Существует изоморфизм групп между группами Коксетера для перенормированной и исходной матриц.
LaTeX
$$$ (M.\mathrm{reindex} \ e).\mathrm{Group} \cong M.\mathrm{Group} $$$
Lean4
/-- The isomorphism between the Coxeter group associated to the reindexed matrix `M.reindex e` and
the Coxeter group associated to `M`. -/
def reindexGroupEquiv : (M.reindex e).Group ≃* M.Group :=
.symm <|
QuotientGroup.congr (Subgroup.normalClosure M.relationsSet) (Subgroup.normalClosure (M.reindex e).relationsSet)
(FreeGroup.freeGroupCongr e)
(by
rw [reindex_relationsSet,
Subgroup.map_normalClosure _ _ (by simpa using (FreeGroup.freeGroupCongr e).surjective), MonoidHom.coe_coe])
