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.

inductive AddSubgroup.IsSubnormal {G : Type u_2} [AddGroup G] : AddSubgroup G → Prop

An additive subgroup H of an additive group G satisfies IsSubnormal if

• either H = ⊤;
• or there is an additive 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 additive subgroups H₀ ≤ H₁ ≤ ... ≤ Hₙ such that

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

See isSubnormal_iff for this characterisation.

• top {G : Type u_2} [AddGroup G] : ⊤.IsSubnormal

  The whole additive subgroup G is subnormal in itself.

• step {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.addSubgroupOf K).Normal) : H.IsSubnormal

  An additive subgroup H is subnormal if there is a subnormal additive 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.

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

A normal additive subgroup is subnormal.

@[simp]

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

The trivial subgroup is subnormal.

@[simp]

theorem AddSubgroup.IsSubnormal.bot {G : Type u_1} [AddGroup G] : ⊥.IsSubnormal

The trivial additive 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 AddSubgroup.IsSubnormal.normal_of_isSimpleAddGroup {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hG : IsSimpleAddGroup G) (hN : H.IsSubnormal) : H.Normal

A subnormal additive subgroup of a simple additive 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 AddSubgroup.IsSubnormal.eq_bot_or_top_of_isSimpleAddGroup {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hG : IsSimpleAddGroup G) (hN : H.IsSubnormal) : H = ⊥ ∨ H = ⊤

A subnormal additive subgroup of a simple additive 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 AddSubgroup.IsSubnormal.iff_eq_top_or_exists {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.IsSubnormal ↔ H = ⊤ ∨ ∃ (K : AddSubgroup G), H < K ∧ K.IsSubnormal ∧ (H.addSubgroupOf 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 AddSubgroup.IsSubnormal.exists_normal_and_le_and_lt_top_of_ne {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hN : H.IsSubnormal) (ne_top : H ≠ ⊤) : ∃ (K : AddSubgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

A proper subnormal additive subgroup is contained in a proper normal additive 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 AddSubgroup.IsSubnormal.lt_normal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hN : H.IsSubnormal) : H = ⊤ ∨ ∃ (K : AddSubgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

A subnormal additive subgroup is either the whole group or it is contained in a proper normal additive 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 AddSubgroup.IsSubnormal.isSubnormal_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.IsSubnormal ↔ ∃ (n : ℕ) (f : ℕ → AddSubgroup G), Monotone f ∧ (∀ (i : ℕ), ((f i).addSubgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤

A characterisation of satisfying IsSubnormal in terms of chains of additive 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 AddSubgroup.IsSubnormal.trans' {G : Type u_1} [AddGroup G] {K : AddSubgroup G} {H : AddSubgroup ↥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.

theorem AddSubgroup.IsSubnormal.trans {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (HK : H ≤ K) (Hsn : (H.addSubgroupOf K).IsSubnormal) (Ksn : K.IsSubnormal) : H.IsSubnormal

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