English
Under the action of an isomorphism, forward and backward subgroup operations correspond; the order structure of Subgroup lattices is preserved by both forward-image and inverse-image constructions.
Русский
При действии изоморфизма операции над подгруппа переходят друг к другу: упорядоченная структура решёток подгрупп сохраняется как для образа, так и для обратного образа.
LaTeX
$$$\\text{Under an isomorphism } f, \\ \mathrm{Subgroup}(G) \\cong_{\\mathrm{ord}} \\mathrm{Subgroup}(H) \\text{ via } \\mathrm{map} \\text{ and } \\mathrm{comap}.$$$
Lean4
@[to_additive (attr := simp, norm_cast)]
theorem comap_toSubmonoid (e : G ≃* N) (s : Subgroup N) : (s.comap e).toSubmonoid = s.toSubmonoid.comap e.toMonoidHom :=
rfl
