# mathlib3documentation

order.jordan_holder

# Jordan-Hölder Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the Jordan Hölder theorem for a jordan_holder_lattice, a class also defined in this file. Examples of jordan_holder_lattice 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 seperately for both groups and modules, the proof in this file can be applied to both.

## Main definitions #

The main definitions in this file are jordan_holder_lattice and composition_series, and the relation equivalent on composition_series

A jordan_holder_lattice 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, is_maximal, and a notion of isomorphism of pairs iso. In the example of subgroups of a group, is_maximal H K means that H is a maximal normal subgroup of K, and iso (H₁, K₁) (H₂, K₂) means that the quotient H₁ / K₁ is isomorphic to the quotient H₂ / K₂. iso must be symmetric and transitive and must satisfy the second isomorphism theorem iso (H, H ⊔ K) (H ⊓ K, K).

A composition_series 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 composition_series 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.top is the largest element of the series, and s.bot is the least element.

Two composition_series 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 composition_series.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 jordan_holder_lattice for both submodules and subgroups, and potentially for modular lattices.

It is not entirely clear how this should be done. Possibly there should be no global instances of jordan_holder_lattice, and the instances should only be defined locally in order to prove the Jordan-Hölder theorem for modules/groups and the API should be transferred because many of the theorems in this file will have stronger versions for modules. There will also need to be an API for mapping composition series across homomorphisms. It is also probably possible to provide an instance of jordan_holder_lattice for any modular_lattice, and in this case the Jordan-Hölder theorem will say that there is a well defined notion of length of a modular lattice. However an instance of jordan_holder_lattice for a modular lattice will not be able to contain the correct notion of isomorphism for modules, so a separate instance for modules will still be required and this will clash with the instance for modular lattices, and so at least one of these instances should not be a global instance.

@[class]
structure jordan_holder_lattice (X : Type u) [lattice X] :

A jordan_holder_lattice 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, is_maximal, and a notion of isomorphism of pairs iso. In the example of subgroups of a group, is_maximal H K means that H is a maximal normal subgroup of K, and iso (H₁, K₁) (H₂, K₂) means that the quotient H₁ / K₁ is isomorphic to the quotient H₂ / K₂. iso must be symmetric and transitive and must satisfy the second isomorphism theorem iso (H, H ⊔ K) (H ⊓ K, K). Examples include subgroup G if G is a group, and submodule R M if M is an R-module.

Instances of this typeclass
Instances of other typeclasses for jordan_holder_lattice
• jordan_holder_lattice.has_sizeof_inst
theorem jordan_holder_lattice.is_maximal_inf_right_of_is_maximal_sup {X : Type u} [lattice X] {x y : X} (hxz : (x y)) (hyz : (x y)) :
theorem jordan_holder_lattice.is_maximal_of_eq_inf {X : Type u} [lattice X] (x b : X) {a y : X} (ha : x y = a) (hxy : x y) (hxb : b) (hyb : b) :
theorem jordan_holder_lattice.second_iso_of_eq {X : Type u} [lattice X] {x y a b : X} (hm : a) (ha : x y = a) (hb : x y = b) :
(b, y)
theorem jordan_holder_lattice.is_maximal.iso_refl {X : Type u} [lattice X] {x y : X} (h : y) :
(x, y)
structure composition_series (X : Type u) [lattice X]  :

A composition_series X is a finite nonempty series of elements of a jordan_holder_lattice such that each element is maximal inside the next. The length of a composition_series 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.top is the largest element of the series, and s.bot is the least element.

Instances for composition_series
@[protected, instance]
def composition_series.has_coe_to_fun {X : Type u} [lattice X]  :
(λ (x : , fin (x.length + 1) X)
Equations
@[protected, instance]
Equations
theorem composition_series.step {X : Type u} [lattice X] (s : composition_series X) (i : fin s.length) :
(s i.succ)
@[simp]
theorem composition_series.coe_fn_mk {X : Type u} [lattice X] (length : ) (series : fin (length + 1) X) (step : (i : fin length), jordan_holder_lattice.is_maximal (series (fin.cast_succ i)) (series i.succ)) :
{length := length, series := series, step' := step} = series
theorem composition_series.lt_succ {X : Type u} [lattice X] (s : composition_series X) (i : fin s.length) :
@[protected]
@[protected]
@[protected, simp]
theorem composition_series.inj {X : Type u} [lattice X] (s : composition_series X) {i j : fin s.length.succ} :
s i = s j i = j
@[protected, instance]
Equations
theorem composition_series.mem_def {X : Type u} [lattice X] {x : X} {s : composition_series X} :
x s x
theorem composition_series.total {X : Type u} [lattice X] {s : composition_series X} {x y : X} (hx : x s) (hy : y s) :
x y y x

The ordered list X of elements of a composition_series X.

Equations
theorem composition_series.ext_fun {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (hl : s₁.length = s₂.length) (h : (i : fin (s₁.length + 1)), s₁ i = s₂ ((fin.cast _) i)) :
s₁ = s₂

Two composition_series are equal if they are the same length and have the same ith element for every i

@[simp]
theorem composition_series.mem_to_list {X : Type u} [lattice X] {s : composition_series X} {x : X} :
x s.to_list x s
def composition_series.of_list {X : Type u} [lattice X] (l : list X) (hl : l list.nil)  :

Make a composition_series X from the ordered list of its elements.

Equations
theorem composition_series.length_of_list {X : Type u} [lattice X] (l : list X) (hl : l list.nil)  :
hc).length = l.length - 1
@[simp]
theorem composition_series.to_list_of_list {X : Type u} [lattice X] (l : list X) (hl : l list.nil)  :
hc).to_list = l
@[ext]
theorem composition_series.ext {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : (x : X), x s₁ x s₂) :
s₁ = s₂

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

def composition_series.top {X : Type u} [lattice X] (s : composition_series X) :
X

The largest element of a composition_series

Equations
@[simp]
theorem composition_series.le_top {X : Type u} [lattice X] {s : composition_series X} (i : fin (s.length + 1)) :
s i s.top
theorem composition_series.le_top_of_mem {X : Type u} [lattice X] {s : composition_series X} {x : X} (hx : x s) :
x s.top
def composition_series.bot {X : Type u} [lattice X] (s : composition_series X) :
X

The smallest element of a composition_series

Equations
@[simp]
theorem composition_series.bot_le {X : Type u} [lattice X] {s : composition_series X} (i : fin (s.length + 1)) :
s.bot s i
theorem composition_series.bot_le_of_mem {X : Type u} [lattice X] {s : composition_series X} {x : X} (hx : x s) :
s.bot x
theorem composition_series.length_pos_of_mem_ne {X : Type u} [lattice X] {s : composition_series X} {x y : X} (hx : x s) (hy : y s) (hxy : x y) :
0 < s.length
theorem composition_series.forall_mem_eq_of_length_eq_zero {X : Type u} [lattice X] {s : composition_series X} (hs : s.length = 0) {x y : X} (hx : x s) (hy : y s) :
x = y

Remove the largest element from a composition_series. If the series s has length zero, then s.erase_top = s

Equations
@[simp]
theorem composition_series.erase_top_series {X : Type u} [lattice X] (s : composition_series X) (i : fin (s.length - 1 + 1)) :
(s.erase_top) i = s i, _⟩
theorem composition_series.mem_erase_top_of_ne_of_mem {X : Type u} [lattice X] {s : composition_series X} {x : X} (hx : x s.top) (hxs : x s) :
theorem composition_series.mem_erase_top {X : Type u} [lattice X] {s : composition_series X} {x : X} (h : 0 < s.length) :
x s.erase_top x s.top x s
theorem composition_series.lt_top_of_mem_erase_top {X : Type u} [lattice X] {s : composition_series X} {x : X} (h : 0 < s.length) (hx : x s.erase_top) :
x < s.top
theorem composition_series.append_cast_add_aux {α : Type u_1} {m n : } (a : fin m.succ α) (b : fin n.succ α) (i : fin m) :
theorem composition_series.append_succ_cast_add_aux {α : Type u_1} {m n : } (a : fin m.succ α) (b : fin n.succ α) (i : fin m) (h : a (fin.last m) = b 0) :
b ((fin.cast_add n) i).succ = a i.succ
theorem composition_series.append_nat_add_aux {α : Type u_1} {m n : } (a : fin m.succ α) (b : fin n.succ α) (i : fin n) :
theorem composition_series.append_succ_nat_add_aux {α : Type u_1} {m n : } (a : fin m.succ α) (b : fin n.succ α) (i : fin n) :
b ((fin.nat_add m) i).succ = b i.succ
def composition_series.append {X : Type u} [lattice X] (s₁ s₂ : composition_series X) (h : s₁.top = s₂.bot) :

Append two composition series s₁ and s₂ such that the least element of s₁ is the maximum element of s₂.

Equations
@[simp]
theorem composition_series.append_length {X : Type u} [lattice X] (s₁ s₂ : composition_series X) (h : s₁.top = s₂.bot) :
(s₁.append s₂ h).length = s₁.length + s₂.length
theorem composition_series.coe_append {X : Type u} [lattice X] (s₁ s₂ : composition_series X) (h : s₁.top = s₂.bot) :
(s₁.append s₂ h) = s₂
@[simp]
theorem composition_series.append_cast_add {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : s₁.top = s₂.bot) (i : fin s₁.length) :
(s₁.append s₂ h) (fin.cast_succ ((fin.cast_add s₂.length) i)) = s₁
@[simp]
theorem composition_series.append_succ_cast_add {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : s₁.top = s₂.bot) (i : fin s₁.length) :
(s₁.append s₂ h) ((fin.cast_add s₂.length) i).succ = s₁ i.succ
@[simp]
theorem composition_series.append_nat_add {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : s₁.top = s₂.bot) (i : fin s₂.length) :
(s₁.append s₂ h) (fin.cast_succ ((fin.nat_add s₁.length) i)) = s₂
@[simp]
theorem composition_series.append_succ_nat_add {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : s₁.top = s₂.bot) (i : fin s₂.length) :
(s₁.append s₂ h) ((fin.nat_add s₁.length) i).succ = s₂ i.succ
def composition_series.snoc {X : Type u} [lattice X] (s : composition_series X) (x : X) (hsat : x) :

Add an element to the top of a composition_series

Equations
@[simp]
theorem composition_series.snoc_length {X : Type u} [lattice X] (s : composition_series X) (x : X) (hsat : x) :
(s.snoc x hsat).length = s.length + 1
@[simp]
theorem composition_series.top_snoc {X : Type u} [lattice X] (s : composition_series X) (x : X) (hsat : x) :
(s.snoc x hsat).top = x
@[simp]
theorem composition_series.snoc_last {X : Type u} [lattice X] (s : composition_series X) (x : X) (hsat : x) :
(s.snoc x hsat) (fin.last (s.length + 1)) = x
@[simp]
theorem composition_series.snoc_cast_succ {X : Type u} [lattice X] (s : composition_series X) (x : X) (hsat : x) (i : fin (s.length + 1)) :
(s.snoc x hsat) = s i
@[simp]
theorem composition_series.bot_snoc {X : Type u} [lattice X] (s : composition_series X) (x : X) (hsat : x) :
(s.snoc x hsat).bot = s.bot
theorem composition_series.mem_snoc {X : Type u} [lattice X] {s : composition_series X} {x y : X} {hsat : x} :
y s.snoc x hsat y s y = x
def composition_series.equivalent {X : Type u} [lattice X] (s₁ s₂ : composition_series X) :
Prop

Two composition_series 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
@[symm]
theorem composition_series.equivalent.symm {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : s₁.equivalent s₂) :
s₂.equivalent s₁
@[trans]
theorem composition_series.equivalent.trans {X : Type u} [lattice X] {s₁ s₂ s₃ : composition_series X} (h₁ : s₁.equivalent s₂) (h₂ : s₂.equivalent s₃) :
s₁.equivalent s₃
theorem composition_series.equivalent.append {X : Type u} [lattice X] {s₁ s₂ t₁ t₂ : composition_series X} (hs : s₁.top = s₂.bot) (ht : t₁.top = t₂.bot) (h₁ : s₁.equivalent t₁) (h₂ : s₂.equivalent t₂) :
(s₁.append s₂ hs).equivalent (t₁.append t₂ ht)
@[protected]
theorem composition_series.equivalent.snoc {X : Type u} [lattice X] {s₁ s₂ : composition_series X} {x₁ x₂ : X} {hsat₁ : x₁} {hsat₂ : x₂} (hequiv : s₁.equivalent s₂) (htop : jordan_holder_lattice.iso (s₁.top, x₁) (s₂.top, x₂)) :
(s₁.snoc x₁ hsat₁).equivalent (s₂.snoc x₂ hsat₂)
theorem composition_series.equivalent.length_eq {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (h : s₁.equivalent s₂) :
s₁.length = s₂.length
theorem composition_series.equivalent.snoc_snoc_swap {X : Type u} [lattice X] {s : composition_series X} {x₁ x₂ y₁ y₂ : X} {hsat₁ : x₁} {hsat₂ : x₂} {hsaty₁ : jordan_holder_lattice.is_maximal (s.snoc x₁ hsat₁).top y₁} {hsaty₂ : jordan_holder_lattice.is_maximal (s.snoc x₂ hsat₂).top y₂} (hr₁ : jordan_holder_lattice.iso (s.top, x₁) (x₂, y₂)) (hr₂ : jordan_holder_lattice.iso (x₁, y₁) (s.top, x₂)) :
((s.snoc x₁ hsat₁).snoc y₁ hsaty₁).equivalent ((s.snoc x₂ hsat₂).snoc y₂ hsaty₂)
theorem composition_series.length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) (hs₁ : s₁.length = 0) :
s₂.length = 0
theorem composition_series.length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) :
0 < s₁.length 0 < s₂.length
theorem composition_series.eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {X : Type u} [lattice X] {s₁ s₂ : composition_series X} (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) (hs₁0 : s₁.length = 0) :
s₁ = s₂
theorem composition_series.exists_top_eq_snoc_equivalant {X : Type u} [lattice X] (s : composition_series X) (x : X) (hm : s.top) (hb : s.bot x) :
(t : , t.bot = s.bot t.length + 1 = s.length (htx : t.top = x), s.equivalent (t.snoc s.top _)

Given a composition_series, s, and an element x such that x is maximal inside s.top there is a series, t, such that t.top = x, t.bot = s.bot and snoc t s.top _ is equivalent to s.

theorem composition_series.jordan_holder {X : Type u} [lattice X] (s₁ s₂ : composition_series X) (hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) :
s₁.equivalent s₂

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