Subnormal subgroups

In this file, we define subnormal subgroups.

We also show some basic results about the interaction of subnormality and simplicity of groups. These should cover most of the results needed in this case.

Main Definition

IsSubnormal H: A subgroup H of a group G satisfies IsSubnormal if

• either H = ⊤;
• or there is a subgroup K of G containing H and such that H is normal in K and K satisfies IsSubnormal.

Main Statements

• eq_bot_or_top_of_isSimpleGroup: the only subnormal subgroups of simple groups are ⊥, the trivial subgroup, and ⊤, the whole group.
• isSubnormal_iff: Shows that IsSubnormal H holds if and only if there is an increasing chain of subgroups, each normal in the following, starting from H and reaching ⊤ in a finite number of steps.
• IsSubnormal.trans: The relation of being IsSubnormal is transitive.

Implementation Notes

We deviate from the common informal definition of subnormality and use an inductive predicate. This turns out to be more convenient to work with. We show the equivalence of the current definition with the existence of chains in isSubnormal_iff.

inductive Subgroup.IsSubnormal {G : Type u_1} [Group G] : Subgroup G → Prop

A subgroup H of a group G satisfies IsSubnormal if

• either H = ⊤;
• or there is a subgroup K of G containing H and such that H is normal in K and K satisfies IsSubnormal.

Equivalently, H.IsSubnormal means that there is a chain of subgroups H₀ ≤ H₁ ≤ ... ≤ Hₙ such that

• H = H₀,
• G = Hₙ,
• for each i ∈ {0, ..., n - 1}, Hᵢ is a normal subgroup of Hᵢ₊₁.

See isSubnormal_iff for this characterisation.

• top {G : Type u_1} [Group G] : ⊤.IsSubnormal

  The whole subgroup G is subnormal in itself.

• step {G : Type u_1} [Group G] (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal) : H.IsSubnormal

  A subgroup H is subnormal if there is a subnormal subgroup K containing H that is subnormal itself and such that H is normal in K.

theorem Subgroup.Normal.isSubnormal {G : Type u_1} [Group G] {H : Subgroup G} (hn : H.Normal) : H.IsSubnormal

A normal subgroup is subnormal.

@[simp]

theorem Subgroup.IsSubnormal.bot {G : Type u_1} [Group G] : ⊥.IsSubnormal

The trivial subgroup is subnormal.

theorem Subgroup.IsSubnormal.normal_of_isSimpleGroup {G : Type u_1} [Group G] {H : Subgroup G} (hG : IsSimpleGroup G) (hN : H.IsSubnormal) : H.Normal

A subnormal subgroup of a simple group is normal.

theorem Subgroup.IsSubnormal.eq_bot_or_top_of_isSimpleGroup {G : Type u_1} [Group G] {H : Subgroup G} (hG : IsSimpleGroup G) (hN : H.IsSubnormal) : H = ⊥ ∨ H = ⊤

A subnormal subgroup of a simple group is either trivial or the whole group.

theorem Subgroup.IsSubnormal.iff_eq_top_or_exists {G : Type u_1} [Group G] {H : Subgroup G} : H.IsSubnormal ↔ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

theorem Subgroup.IsSubnormal.exists_normal_and_le_and_lt_top_of_ne {G : Type u_1} [Group G] {H : Subgroup G} (hN : H.IsSubnormal) (ne_top : H ≠ ⊤) : ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

A proper subnormal subgroup is contained in a proper normal subgroup.

theorem Subgroup.IsSubnormal.lt_normal {G : Type u_1} [Group G] {H : Subgroup G} (hN : H.IsSubnormal) : H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

A subnormal subgroup is either the whole group or it is contained in a proper normal subgroup.

theorem Subgroup.IsSubnormal.isSubnormal_iff {G : Type u_1} [Group G] {H : Subgroup G} : H.IsSubnormal ↔ ∃ (n : ℕ) (f : ℕ → Subgroup G), Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤

A characterisation of satisfying IsSubnormal in terms of chains of subgroups, each normal in the following one.

The sequence stabilises once it reaches ⊤, which is guaranteed at the asserted n.

theorem Subgroup.IsSubnormal.exists_chain {G : Type u_1} [Group G] {H : Subgroup G} : H.IsSubnormal → ∃ (n : ℕ) (f : ℕ → Subgroup G), Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤

Alias of the forward direction of Subgroup.IsSubnormal.isSubnormal_iff.

---

A characterisation of satisfying IsSubnormal in terms of chains of subgroups, each normal in the following one.

The sequence stabilises once it reaches ⊤, which is guaranteed at the asserted n.

theorem Subgroup.IsSubnormal.trans' {G : Type u_1} [Group G] {K : Subgroup G} {H : Subgroup ↥K} (Hsn : H.IsSubnormal) (Ksn : K.IsSubnormal) : (map K.subtype H).IsSubnormal

Subnormality is transitive.

This version involves an explicit subtype; the version IsSubnormal.trans does not.

theorem Subgroup.IsSubnormal.trans {G : Type u_1} [Group G] {H K : Subgroup G} (HK : H ≤ K) (Hsn : (H.subgroupOf K).IsSubnormal) (Ksn : K.IsSubnormal) : H.IsSubnormal

If H is a subnormal subgroup of K and K is a subnormal subgroup of G, then H is a subnormal subgroup of G.