English
Constructions that lift isomorphisms between G' and H' to quotient isomorphisms between G/G' and H/H' preserve composition and inverses.
Русский
Построения, которые поднимают изоморфизмы между G' и H' до изоморфизмов между G/G' и H/H', сохраняют композицию и обратные.
LaTeX
$$$\\text{congr} : G' \\to G \\; \\Rightarrow\\; H' \\to H$ induces a MulEquiv $(G/G') \\;\\simeq\\; (H/H')$ respecting maps.$$
Lean4
/-- `QuotientGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
given that `e` maps `G` to `H`. -/
@[to_additive /-- `QuotientAddGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
given that `e` maps `G` to `H`. -/
]
def congr (e : G ≃* H) (he : G'.map e = H') : G ⧸ G' ≃* H ⧸ H' :=
{
map G' H' e
(he ▸ G'.le_comap_map
(e : G →* H)) with
toFun := map G' H' e (he ▸ G'.le_comap_map (e : G →* H))
invFun := map H' G' e.symm (he ▸ (G'.map_equiv_eq_comap_symm e).le)
left_inv := fun x =>
by
rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H)) (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm, MulEquiv.coe_monoidHom_refl, map_id_apply]
right_inv := fun x =>
by
rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le) (he ▸ G'.le_comap_map (e : G →* H))]
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self, MulEquiv.coe_monoidHom_refl, map_id_apply] }
