Covering subgroups

The subgroups of G contained in a subgroup K are order-isomorphic to the subgroups of K (Subgroup.MapSubtype.orderIso). Under that isomorphism, a subgroup H covered by K in the subgroup lattice of G becomes a maximal subgroup of K.

Main result

• CovBy.isCoatom_subgroupOf: if H ⋖ K, then H.subgroupOf K is a coatom in the subgroup lattice of K.

theorem CovBy.isCoatom_subgroupOf {G : Type u_1} [Group G] {H K : Subgroup G} (hHK : H ⋖ K) : IsCoatom (H.subgroupOf K)

If H is covered by K in the subgroup lattice of G, then H, regarded as a subgroup of K, is a maximal subgroup of K.