Jordan-Hölder Theorem

This file proves the Jordan Hölder theorem for a JordanHolderLattice, a class also defined in this file. Examples of JordanHolderLattice include Subgroup G if G is a group, and Submodule R M if M is an R-module. Using this approach the theorem need not be proved separately for both groups and modules, the proof in this file can be applied to both.

Main definitions

The main definitions in this file are JordanHolderLattice and CompositionSeries, and the relation Equivalent on CompositionSeries

A JordanHolderLattice is the class for which the Jordan Hölder theorem is proved. A Jordan Hölder lattice is a lattice equipped with a notion of maximality, IsMaximal. In the example of subgroups of a group, IsMaximal H K means that H is a maximal normal subgroup of K.

A CompositionSeries X is a finite nonempty series of elements of the lattice X such that each element is maximal inside the next. The length of a CompositionSeries X is one less than the number of elements in the series. Note that there is no stipulation that a series start from the bottom of the lattice and finish at the top. For a composition series s, s.last is the largest element of the series, and s.head is the least element.

We define an equivalence relation JordanHolderLattice.Iso on intervals generated by the relations Iso (x, x ⊔ y) (x ⊓ y, y) for IsMaximal x (x ⊔ y). This is the strongest possible equivalence relation for which we can prove the Jordan Hölder theorem. For any specific JordanHolderLattice, one must verify that Iso implies the desired weaker notion (e.g., isomorphism of quotients).

Two CompositionSeries X, s₁ and s₂ are equivalent if there is a bijection e : Fin s₁.length ≃ Fin s₂.length such that for any i, Iso (s₁ i, s₁ i.succ) (s₂ (e i), s₂ (e i.succ))

Main theorems

The main theorem is CompositionSeries.jordan_holder, which says that if two composition series have the same least element and the same largest element, then they are Equivalent.

TODO

Provide instances of JordanHolderLattice for subgroups.

class JordanHolderLattice (X : Type u) [Lattice X] : Type u

A JordanHolderLattice is the class for which the Jordan Hölder theorem is proved. A Jordan Hölder lattice is a lattice equipped with a notion of maximality, IsMaximal.

Examples include Subgroup G if G is a group, and Submodule R M if M is an R-module.

In the example of subgroups, IsMaximal H K means that H is a maximal normal subgroup of K. In the example of submodules, IsMaximal M N means that M is a maximal submodule of N.

• IsMaximal : X → X → Prop
• lt_of_isMaximal {x y : X} : IsMaximal x y → x < y
• sup_eq_of_isMaximal {x y z : X} : IsMaximal x z → IsMaximal y z → x ≠ y → x ⊔ y = z
• isMaximal_inf_left_of_isMaximal_sup {x y : X} : IsMaximal x (x ⊔ y) → IsMaximal y (x ⊔ y) → IsMaximal (x ⊓ y) x

@[instance_reducible]

instance JordanHolderLattice.instOfIsModularLattice (X : Type u) [Lattice X] [IsModularLattice X] : JordanHolderLattice X

Every modular lattice is a Jordan Hölder lattice.

Equations

• JordanHolderLattice.instOfIsModularLattice X = { IsMaximal := fun (x1 x2 : X) => x1 ⋖ x2, lt_of_isMaximal := ⋯, sup_eq_of_isMaximal := ⋯, isMaximal_inf_left_of_isMaximal_sup := ⋯ }

def JordanHolderLattice.Iso {X : Type u} [Lattice X] [JordanHolderLattice X] : X × X → X × X → Prop

The equivalence relation on intervals generated by the relations Iso (x, x ⊔ y) (x ⊓ y, y) for IsMaximal x (x ⊔ y). This is the strongest possibly equivalence relation for which we can prove the Jordan Hölder theorem. For any specific JordanHolderLattice, use Iso.rel to verify that Iso implies the desired weaker notion (e.g., isomorphism of quotients).

Equations

• One or more equations did not get rendered due to their size.

theorem JordanHolderLattice.iso_refl {X : Type u} [Lattice X] [JordanHolderLattice X] {x : X × X} : Iso x x

theorem JordanHolderLattice.iso_symm {X : Type u} [Lattice X] [JordanHolderLattice X] {x y : X × X} (h : Iso x y) : Iso y x

theorem JordanHolderLattice.iso_trans {X : Type u} [Lattice X] [JordanHolderLattice X] {x y z : X × X} (hxy : Iso x y) (hyz : Iso y z) : Iso x z

theorem JordanHolderLattice.second_iso {X : Type u} [Lattice X] [JordanHolderLattice X] {x y : X} (h : IsMaximal x (x ⊔ y)) : Iso (x, x ⊔ y) (x ⊓ y, y)

theorem JordanHolderLattice.Iso.rel {X : Type u} [Lattice X] [JordanHolderLattice X] (e : X × X → X × X → Prop) (h_refl : ∀ {x : X × X}, e x x) (h_symm : ∀ {x y : X × X}, e x y → e y x) (h_trans : ∀ {x y z : X × X}, e x y → e y z → e x z) (h_rel : ∀ {x y : X}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)) {x y : X × X} (h_iso : Iso x y) : e x y

The equivalence relation on intervals implies any other notions of isomorphism.

theorem JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup {X : Type u} [Lattice X] [JordanHolderLattice X] {x y : X} (hxz : IsMaximal x (x ⊔ y)) (hyz : IsMaximal y (x ⊔ y)) : IsMaximal (x ⊓ y) y

theorem JordanHolderLattice.isMaximal_of_eq_inf {X : Type u} [Lattice X] [JordanHolderLattice X] (x b : X) {a y : X} (ha : x ⊓ y = a) (hxy : x ≠ y) (hxb : IsMaximal x b) (hyb : IsMaximal y b) : IsMaximal a y

theorem JordanHolderLattice.second_iso_of_eq {X : Type u} [Lattice X] [JordanHolderLattice X] {x y a b : X} (hm : IsMaximal x a) (ha : x ⊔ y = a) (hb : x ⊓ y = b) : Iso (x, a) (b, y)

@[deprecated JordanHolderLattice.iso_refl (since := "2026-07-11")]

theorem JordanHolderLattice.IsMaximal.iso_refl {X : Type u} [Lattice X] [JordanHolderLattice X] {x : X × X} : Iso x x

Alias of JordanHolderLattice.iso_refl.

@[reducible, inline]

abbrev CompositionSeries (X : Type u) [Lattice X] [JordanHolderLattice X] : Type u

A CompositionSeries X is a finite nonempty series of elements of a JordanHolderLattice such that each element is maximal inside the next. The length of a CompositionSeries X is one less than the number of elements in the series. Note that there is no stipulation that a series start from the bottom of the lattice and finish at the top. For a composition series s, s.last is the largest element of the series, and s.head is the least element.

Equations

• CompositionSeries X = RelSeries {(x, y) : X × X | JordanHolderLattice.IsMaximal x y}

theorem CompositionSeries.lt_succ {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (i : Fin s.length) : s.toFun i.castSucc < s.toFun i.succ

theorem CompositionSeries.strictMono {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : StrictMono s.toFun

theorem CompositionSeries.injective {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : Function.Injective s.toFun

@[simp]

theorem CompositionSeries.inj {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) {i j : Fin s.length.succ} : s.toFun i = s.toFun j ↔ i = j

theorem CompositionSeries.total {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s) : x ≤ y ∨ y ≤ x

theorem CompositionSeries.toList_sorted {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : (RelSeries.toList s).SortedLT

theorem CompositionSeries.toList_nodup {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : (RelSeries.toList s).Nodup

theorem CompositionSeries.ext {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} (h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂

Two CompositionSeries are equal if they have the same elements. See also ext_fun.

theorem CompositionSeries.ext_iff {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} : s₁ = s₂ ↔ ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂

@[simp]

theorem CompositionSeries.le_last {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (i : Fin (s.length + 1)) : s.toFun i ≤ RelSeries.last s

theorem CompositionSeries.le_last_of_mem {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (hx : x ∈ s) : x ≤ RelSeries.last s

@[simp]

theorem CompositionSeries.head_le {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (i : Fin (s.length + 1)) : RelSeries.head s ≤ s.toFun i

theorem CompositionSeries.head_le_of_mem {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (hx : x ∈ s) : RelSeries.head s ≤ x

theorem CompositionSeries.last_eraseLast_le {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : (RelSeries.eraseLast s).last ≤ RelSeries.last s

theorem CompositionSeries.mem_eraseLast_of_ne_of_mem {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (hx : x ≠ RelSeries.last s) (hxs : x ∈ s) : x ∈ RelSeries.eraseLast s

theorem CompositionSeries.mem_eraseLast {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (h : 0 < s.length) : x ∈ RelSeries.eraseLast s ↔ x ≠ RelSeries.last s ∧ x ∈ s

theorem CompositionSeries.lt_last_of_mem_eraseLast {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (h : 0 < s.length) (hx : x ∈ RelSeries.eraseLast s) : x < RelSeries.last s

theorem CompositionSeries.isMaximal_eraseLast_last {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (h : 0 < s.length) : JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)

theorem CompositionSeries.eq_snoc_eraseLast {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (h : 0 < s.length) : s = (RelSeries.eraseLast s).snoc (RelSeries.last s) ⋯

@[simp]

theorem CompositionSeries.snoc_eraseLast_last {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (h : JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)) : (RelSeries.eraseLast s).snoc (RelSeries.last s) h = s

def CompositionSeries.Equivalent {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ s₂ : CompositionSeries X) : Prop

Two CompositionSeries X, s₁ and s₂ are equivalent if there is a bijection e : Fin s₁.length ≃ Fin s₂.length such that for any i, Iso (s₁ i) (s₁ i.succ) (s₂ (e i), s₂ (e i.succ))

Equations

• One or more equations did not get rendered due to their size.

theorem CompositionSeries.Equivalent.refl {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : s.Equivalent s

theorem CompositionSeries.Equivalent.symm {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} (h : s₁.Equivalent s₂) : s₂.Equivalent s₁

theorem CompositionSeries.Equivalent.trans {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ s₃ : CompositionSeries X} (h₁ : s₁.Equivalent s₂) (h₂ : s₂.Equivalent s₃) : s₁.Equivalent s₃

theorem CompositionSeries.Equivalent.smash {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ t₁ t₂ : CompositionSeries X} (hs : RelSeries.last s₁ = RelSeries.head s₂) (ht : RelSeries.last t₁ = RelSeries.head t₂) (h₁ : s₁.Equivalent t₁) (h₂ : s₂.Equivalent t₂) : Equivalent (RelSeries.smash s₁ s₂ hs) (RelSeries.smash t₁ t₂ ht)

theorem CompositionSeries.Equivalent.snoc {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X} {hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s₁) x₁} {hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s₂) x₂} (hequiv : s₁.Equivalent s₂) (hlast : JordanHolderLattice.Iso (RelSeries.last s₁, x₁) (RelSeries.last s₂, x₂)) : Equivalent (RelSeries.snoc s₁ x₁ hsat₁) (RelSeries.snoc s₂ x₂ hsat₂)

theorem CompositionSeries.Equivalent.length_eq {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} (h : s₁.Equivalent s₂) : s₁.length = s₂.length

theorem CompositionSeries.Equivalent.snoc_snoc_swap {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x₁ x₂ y₁ y₂ : X} {hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₁} {hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₂} {hsaty₁ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₁ hsat₁).last y₁} {hsaty₂ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₂ hsat₂).last y₂} (hr₁ : JordanHolderLattice.Iso (RelSeries.last s, x₁) (x₂, y₂)) (hr₂ : JordanHolderLattice.Iso (x₁, y₁) (RelSeries.last s, x₂)) : Equivalent ((RelSeries.snoc s x₁ hsat₁).snoc y₁ hsaty₁) ((RelSeries.snoc s x₂ hsat₂).snoc y₂ hsaty₂)

theorem CompositionSeries.length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} (hb : RelSeries.head s₁ = RelSeries.head s₂) (ht : RelSeries.last s₁ = RelSeries.last s₂) (hs₁ : s₁.length = 0) : s₂.length = 0

theorem CompositionSeries.length_pos_of_head_eq_head_of_last_eq_last_of_length_pos {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} (hb : RelSeries.head s₁ = RelSeries.head s₂) (ht : RelSeries.last s₁ = RelSeries.last s₂) : 0 < s₁.length → 0 < s₂.length

theorem CompositionSeries.eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} (hb : RelSeries.head s₁ = RelSeries.head s₂) (ht : RelSeries.last s₁ = RelSeries.last s₂) (hs₁0 : s₁.length = 0) : s₁ = s₂

theorem CompositionSeries.exists_last_eq_snoc_equivalent {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hm : JordanHolderLattice.IsMaximal x (RelSeries.last s)) (hb : RelSeries.head s ≤ x) : ∃ (t : CompositionSeries X), RelSeries.head t = RelSeries.head s ∧ t.length + 1 = s.length ∧ ∃ (htx : RelSeries.last t = x), s.Equivalent (RelSeries.snoc t (RelSeries.last s) ⋯)

Given a CompositionSeries, s, and an element x such that x is maximal inside s.last there is a series, t, such that t.last = x, t.head = s.head and snoc t s.last _ is equivalent to s.

theorem CompositionSeries.jordan_holder {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ s₂ : CompositionSeries X) (hb : RelSeries.head s₁ = RelSeries.head s₂) (ht : RelSeries.last s₁ = RelSeries.last s₂) : s₁.Equivalent s₂

The Jordan-Hölder theorem, stated for any JordanHolderLattice. If two composition series start and finish at the same place, they are equivalent.