English
Normal subgroups correspond to congruence relations on a group; the order isomorphism maps between these structures.
Русский
Нормальные подгруппы соответствуют конгруэнциям на группе; отображение порядка устанавливает изоморфизм.
LaTeX
$$Subgroup.orderIsoCon : { N : Subgroup G // N.Normal } ≃o Con G$$
Lean4
/-- The normal subgroups correspond to the congruence relations on a group.
-/
@[to_additive (attr := simps) AddSubgroup.orderIsoAddCon /--
The normal subgroups correspond to the additive congruence relations on an `AddGroup`. -/
]
def _root_.Subgroup.orderIsoCon : { N : Subgroup G // N.Normal } ≃o Con G
where
toFun
N :=
letI : N.val.Normal := N.prop;
QuotientGroup.con N
invFun c := ⟨c.subgroup, inferInstance⟩
left_inv := fun ⟨N, _⟩ ↦ Subtype.mk_eq_mk.mpr (Con.subgroup_quotientGroupCon N)
right_inv c := QuotientGroup.con_subgroup c
map_rel_iff' := by
simp only [QuotientGroup.con, Equiv.coe_fn_mk, Con.le_def, Con.rel_mk, leftRel_apply]
refine ⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩
specialize @h 1 x
simp_all
