English
Let G and H be groups and f: G ≃* H be an isomorphism. The operation comapSubgroup(f) sends each subgroup of H to its preimage in G, establishing an order isomorphism between the lattices of subgroups of H and G; its inverse is comapSubgroup(f.symm).
Русский
Пусть G и H — группы, и f: G ≃* H — изоморфизм. Операция comapSubgroup(f) отображает любую подгруппу H в её предобраз в G, задавая изоморфизм частиразностей между решётками подгрупп H и G; обратное отображение задаётся comapSubgroup(f.symm).
LaTeX
$$$\\operatorname{comapSubgroup}(f): \\mathrm{Subgroup}(H) \\cong_{\\mathrm{ord}} \\mathrm{Subgroup}(G)$$$
Lean4
/-- An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their inverse images.
See also `MulEquiv.mapSubgroup` which maps subgroups to their forward images.
-/
@[to_additive (attr := simps) /-- An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their inverse images.
See also `AddEquiv.mapAddSubgroup` which maps subgroups to their forward images. -/
]
def comapSubgroup (f : G ≃* H) : Subgroup H ≃o Subgroup G
where
toFun := Subgroup.comap f
invFun := Subgroup.comap f.symm
left_inv sg := by simp [Subgroup.comap_comap]
right_inv sh := by simp [Subgroup.comap_comap]
map_rel_iff'
{sg1
sg2} :=
⟨fun h => by simpa [Subgroup.comap_comap] using Subgroup.comap_mono (f := (f.symm : H →* G)) h, Subgroup.comap_mono⟩
