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, and a notion of isomorphism of pairs Iso. In the example of subgroups of a group, IsMaximal 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 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.top is the largest element of the series, and s.bot is the least element.

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 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 JordanHolderLattice, 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 JordanHolderLattice for any ModularLattice, 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 JordanHolderLattice 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 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, and a notion of isomorphism of pairs Iso. In the example of subgroups of a group, IsMaximal 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.

• IsMaximal : X → X → Prop
• lt_of_isMaximal : ∀ {x y : X}, JordanHolderLattice.IsMaximal x y → x < y
• sup_eq_of_isMaximal : ∀ {x y z : X}, JordanHolderLattice.IsMaximal x z → JordanHolderLattice.IsMaximal y z → x ≠ y → x ⊔ y = z
• isMaximal_inf_left_of_isMaximal_sup : ∀ {x y : X}, JordanHolderLattice.IsMaximal x (x ⊔ y) → JordanHolderLattice.IsMaximal y (x ⊔ y) → JordanHolderLattice.IsMaximal (x ⊓ y) x
• Iso : X × X → X × X → Prop
• iso_symm : ∀ {x y : X × X}, JordanHolderLattice.Iso x y → JordanHolderLattice.Iso y x
• iso_trans : ∀ {x y z : X × X}, JordanHolderLattice.Iso x y → JordanHolderLattice.Iso y z → JordanHolderLattice.Iso x z
• second_iso : ∀ {x y : X}, JordanHolderLattice.IsMaximal x (x ⊔ y) → JordanHolderLattice.Iso (x, x ⊔ y) (x ⊓ y, y)

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

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

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

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

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

• length : ℕ
• series : Fin (self.length + 1) → X
• step' : ∀ (i : Fin self.length), JordanHolderLattice.IsMaximal (self.series (Fin.castSucc i)) (self.series (Fin.succ i))

instance CompositionSeries.coeFun {X : Type u} [Lattice X] [JordanHolderLattice X] : CoeFun (CompositionSeries X) fun (x : CompositionSeries X) => Fin (x.length + 1) → X

Equations

• CompositionSeries.coeFun = { coe := CompositionSeries.series }

instance CompositionSeries.inhabited {X : Type u} [Lattice X] [JordanHolderLattice X] [Inhabited X] : Inhabited (CompositionSeries X)

Equations

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

theorem CompositionSeries.step {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (i : Fin s.length) : JordanHolderLattice.IsMaximal (s.series (Fin.castSucc i)) (s.series (Fin.succ i))

theorem CompositionSeries.coeFn_mk {X : Type u} [Lattice X] [JordanHolderLattice X] (length : ℕ) (series : Fin (length + 1) → X) (step : ∀ (i : Fin length), JordanHolderLattice.IsMaximal (series (Fin.castSucc i)) (series (Fin.succ i))) : { length := length, series := series, step' := step }.series = series

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

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

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

@[simp]

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

instance CompositionSeries.membership {X : Type u} [Lattice X] [JordanHolderLattice X] : Membership X (CompositionSeries X)

Equations

• CompositionSeries.membership = { mem := fun (x : X) (s : CompositionSeries X) => x ∈ Set.range s.series }

theorem CompositionSeries.mem_def {X : Type u} [Lattice X] [JordanHolderLattice X] {x : X} {s : CompositionSeries X} : x ∈ s ↔ x ∈ Set.range s.series

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

def CompositionSeries.toList {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : List X

The ordered List X of elements of a CompositionSeries X.

Equations

• CompositionSeries.toList s = List.ofFn s.series

theorem CompositionSeries.ext_fun {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (hl : s₁.length = s₂.length) (h : ∀ (i : Fin (s₁.length + 1)), s₁.series i = s₂.series (Fin.cast (_ : Nat.succ s₁.length = Nat.succ s₂.length) i)) : s₁ = s₂

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

@[simp]

theorem CompositionSeries.length_toList {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : List.length (CompositionSeries.toList s) = s.length + 1

theorem CompositionSeries.toList_ne_nil {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.toList s ≠ []

theorem CompositionSeries.toList_injective {X : Type u} [Lattice X] [JordanHolderLattice X] : Function.Injective CompositionSeries.toList

theorem CompositionSeries.chain'_toList {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : List.Chain' JordanHolderLattice.IsMaximal (CompositionSeries.toList s)

theorem CompositionSeries.toList_sorted {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : List.Sorted (fun (x x_1 : X) => x < x_1) (CompositionSeries.toList s)

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

@[simp]

theorem CompositionSeries.mem_toList {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} : x ∈ CompositionSeries.toList s ↔ x ∈ s

def CompositionSeries.ofList {X : Type u} [Lattice X] [JordanHolderLattice X] (l : List X) (hl : l ≠ []) (hc : List.Chain' JordanHolderLattice.IsMaximal l) : CompositionSeries X

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

Equations

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

theorem CompositionSeries.length_ofList {X : Type u} [Lattice X] [JordanHolderLattice X] (l : List X) (hl : l ≠ []) (hc : List.Chain' JordanHolderLattice.IsMaximal l) : (CompositionSeries.ofList l hl hc).length = List.length l - 1

theorem CompositionSeries.ofList_toList {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.ofList (CompositionSeries.toList s) (_ : CompositionSeries.toList s ≠ []) (_ : List.Chain' JordanHolderLattice.IsMaximal (CompositionSeries.toList s)) = s

@[simp]

theorem CompositionSeries.ofList_toList' {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.ofList (CompositionSeries.toList s) (_ : CompositionSeries.toList s ≠ []) (_ : List.Chain' JordanHolderLattice.IsMaximal (CompositionSeries.toList s)) = s

@[simp]

theorem CompositionSeries.toList_ofList {X : Type u} [Lattice X] [JordanHolderLattice X] (l : List X) (hl : l ≠ []) (hc : List.Chain' JordanHolderLattice.IsMaximal l) : CompositionSeries.toList (CompositionSeries.ofList l hl hc) = l

theorem CompositionSeries.ext {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {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.

def CompositionSeries.top {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : X

The largest element of a CompositionSeries

Equations

• CompositionSeries.top s = s.series (Fin.last s.length)

theorem CompositionSeries.top_mem {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.top s ∈ s

@[simp]

theorem CompositionSeries.le_top {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (i : Fin (s.length + 1)) : s.series i ≤ CompositionSeries.top s

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

def CompositionSeries.bot {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : X

The smallest element of a CompositionSeries

Equations

• CompositionSeries.bot s = s.series 0

theorem CompositionSeries.bot_mem {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.bot s ∈ s

@[simp]

theorem CompositionSeries.bot_le {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (i : Fin (s.length + 1)) : CompositionSeries.bot s ≤ s.series i

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

theorem CompositionSeries.length_pos_of_mem_ne {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} {y : X} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : 0 < s.length

theorem CompositionSeries.forall_mem_eq_of_length_eq_zero {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (hs : s.length = 0) {x : X} {y : X} (hx : x ∈ s) (hy : y ∈ s) : x = y

@[simp]

theorem CompositionSeries.eraseTop_series {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (i : Fin (s.length - 1 + 1)) : (CompositionSeries.eraseTop s).series i = s.series { val := ↑i, isLt := (_ : ↑i < s.length + 1) }

@[simp]

theorem CompositionSeries.eraseTop_length {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : (CompositionSeries.eraseTop s).length = s.length - 1

def CompositionSeries.eraseTop {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries X

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

Equations

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

theorem CompositionSeries.top_eraseTop {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.top (CompositionSeries.eraseTop s) = s.series { val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }

theorem CompositionSeries.eraseTop_top_le {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.top (CompositionSeries.eraseTop s) ≤ CompositionSeries.top s

@[simp]

theorem CompositionSeries.bot_eraseTop {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) : CompositionSeries.bot (CompositionSeries.eraseTop s) = CompositionSeries.bot s

theorem CompositionSeries.mem_eraseTop_of_ne_of_mem {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (hx : x ≠ CompositionSeries.top s) (hxs : x ∈ s) : x ∈ CompositionSeries.eraseTop s

theorem CompositionSeries.mem_eraseTop {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (h : 0 < s.length) : x ∈ CompositionSeries.eraseTop s ↔ x ≠ CompositionSeries.top s ∧ x ∈ s

theorem CompositionSeries.lt_top_of_mem_eraseTop {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} (h : 0 < s.length) (hx : x ∈ CompositionSeries.eraseTop s) : x < CompositionSeries.top s

theorem CompositionSeries.isMaximal_eraseTop_top {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (h : 0 < s.length) : JordanHolderLattice.IsMaximal (CompositionSeries.top (CompositionSeries.eraseTop s)) (CompositionSeries.top s)

theorem CompositionSeries.append_castAdd_aux {α : Type u_1} {m : ℕ} {n : ℕ} (a : Fin (Nat.succ m) → α) (b : Fin (Nat.succ n) → α) (i : Fin m) : Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.castSucc (Fin.castAdd n i)) = a (Fin.castSucc i)

theorem CompositionSeries.append_succ_castAdd_aux {α : Type u_1} {m : ℕ} {n : ℕ} (a : Fin (Nat.succ m) → α) (b : Fin (Nat.succ n) → α) (i : Fin m) (h : a (Fin.last m) = b 0) : Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.succ (Fin.castAdd n i)) = a (Fin.succ i)

theorem CompositionSeries.append_natAdd_aux {α : Type u_1} {m : ℕ} {n : ℕ} (a : Fin (Nat.succ m) → α) (b : Fin (Nat.succ n) → α) (i : Fin n) : Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.castSucc (Fin.natAdd m i)) = b (Fin.castSucc i)

theorem CompositionSeries.append_succ_natAdd_aux {α : Type u_1} {m : ℕ} {n : ℕ} (a : Fin (Nat.succ m) → α) (b : Fin (Nat.succ n) → α) (i : Fin n) : Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.succ (Fin.natAdd m i)) = b (Fin.succ i)

@[simp]

theorem CompositionSeries.append_length {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ : CompositionSeries X) (s₂ : CompositionSeries X) (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) : (CompositionSeries.append s₁ s₂ h).length = s₁.length + s₂.length

def CompositionSeries.append {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ : CompositionSeries X) (s₂ : CompositionSeries X) (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) : CompositionSeries X

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

Equations

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

theorem CompositionSeries.coe_append {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ : CompositionSeries X) (s₂ : CompositionSeries X) (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) : (CompositionSeries.append s₁ s₂ h).series = Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc) s₂.series

@[simp]

theorem CompositionSeries.append_castAdd {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) (i : Fin s₁.length) : (CompositionSeries.append s₁ s₂ h).series (Fin.castSucc (Fin.castAdd s₂.length i)) = s₁.series (Fin.castSucc i)

@[simp]

theorem CompositionSeries.append_succ_castAdd {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) (i : Fin s₁.length) : (CompositionSeries.append s₁ s₂ h).series (Fin.succ (Fin.castAdd s₂.length i)) = s₁.series (Fin.succ i)

@[simp]

theorem CompositionSeries.append_natAdd {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) (i : Fin s₂.length) : (CompositionSeries.append s₁ s₂ h).series (Fin.castSucc (Fin.natAdd s₁.length i)) = s₂.series (Fin.castSucc i)

@[simp]

theorem CompositionSeries.append_succ_natAdd {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (h : CompositionSeries.top s₁ = CompositionSeries.bot s₂) (i : Fin s₂.length) : (CompositionSeries.append s₁ s₂ h).series (Fin.succ (Fin.natAdd s₁.length i)) = s₂.series (Fin.succ i)

@[simp]

theorem CompositionSeries.snoc_length {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x) : (CompositionSeries.snoc s x hsat).length = s.length + 1

def CompositionSeries.snoc {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x) : CompositionSeries X

Add an element to the top of a CompositionSeries

Equations

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

@[simp]

theorem CompositionSeries.top_snoc {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x) : CompositionSeries.top (CompositionSeries.snoc s x hsat) = x

@[simp]

theorem CompositionSeries.snoc_last {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x) : (CompositionSeries.snoc s x hsat).series (Fin.last (s.length + 1)) = x

@[simp]

theorem CompositionSeries.snoc_castSucc {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x) (i : Fin (s.length + 1)) : (CompositionSeries.snoc s x hsat).series (Fin.castSucc i) = s.series i

@[simp]

theorem CompositionSeries.bot_snoc {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x) : CompositionSeries.bot (CompositionSeries.snoc s x hsat) = CompositionSeries.bot s

theorem CompositionSeries.mem_snoc {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} {x : X} {y : X} {hsat : JordanHolderLattice.IsMaximal (CompositionSeries.top s) x} : y ∈ CompositionSeries.snoc s x hsat ↔ y ∈ s ∨ y = x

theorem CompositionSeries.eq_snoc_eraseTop {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (h : 0 < s.length) : s = CompositionSeries.snoc (CompositionSeries.eraseTop s) (CompositionSeries.top s) (_ : JordanHolderLattice.IsMaximal (CompositionSeries.top (CompositionSeries.eraseTop s)) (CompositionSeries.top s))

@[simp]

theorem CompositionSeries.snoc_eraseTop_top {X : Type u} [Lattice X] [JordanHolderLattice X] {s : CompositionSeries X} (h : JordanHolderLattice.IsMaximal (CompositionSeries.top (CompositionSeries.eraseTop s)) (CompositionSeries.top s)) : CompositionSeries.snoc (CompositionSeries.eraseTop s) (CompositionSeries.top s) h = s

def CompositionSeries.Equivalent {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ : CompositionSeries X) (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) : CompositionSeries.Equivalent s s

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

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

theorem CompositionSeries.Equivalent.append {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} {t₁ : CompositionSeries X} {t₂ : CompositionSeries X} (hs : CompositionSeries.top s₁ = CompositionSeries.bot s₂) (ht : CompositionSeries.top t₁ = CompositionSeries.bot t₂) (h₁ : CompositionSeries.Equivalent s₁ t₁) (h₂ : CompositionSeries.Equivalent s₂ t₂) : CompositionSeries.Equivalent (CompositionSeries.append s₁ s₂ hs) (CompositionSeries.append t₁ t₂ ht)

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

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

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

theorem CompositionSeries.length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (hb : CompositionSeries.bot s₁ = CompositionSeries.bot s₂) (ht : CompositionSeries.top s₁ = CompositionSeries.top s₂) (hs₁ : s₁.length = 0) : s₂.length = 0

theorem CompositionSeries.length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (hb : CompositionSeries.bot s₁ = CompositionSeries.bot s₂) (ht : CompositionSeries.top s₁ = CompositionSeries.top s₂) : 0 < s₁.length → 0 < s₂.length

theorem CompositionSeries.eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {X : Type u} [Lattice X] [JordanHolderLattice X] {s₁ : CompositionSeries X} {s₂ : CompositionSeries X} (hb : CompositionSeries.bot s₁ = CompositionSeries.bot s₂) (ht : CompositionSeries.top s₁ = CompositionSeries.top s₂) (hs₁0 : s₁.length = 0) : s₁ = s₂

theorem CompositionSeries.exists_top_eq_snoc_equivalant {X : Type u} [Lattice X] [JordanHolderLattice X] (s : CompositionSeries X) (x : X) (hm : JordanHolderLattice.IsMaximal x (CompositionSeries.top s)) (hb : CompositionSeries.bot s ≤ x) : ∃ (t : CompositionSeries X), CompositionSeries.bot t = CompositionSeries.bot s ∧ t.length + 1 = s.length ∧ ∃ (htx : CompositionSeries.top t = x), CompositionSeries.Equivalent s (CompositionSeries.snoc t (CompositionSeries.top s) (_ : JordanHolderLattice.IsMaximal (CompositionSeries.top t) (CompositionSeries.top s)))

Given a CompositionSeries, 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 CompositionSeries.jordan_holder {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ : CompositionSeries X) (s₂ : CompositionSeries X) (hb : CompositionSeries.bot s₁ = CompositionSeries.bot s₂) (ht : CompositionSeries.top s₁ = CompositionSeries.top s₂) : CompositionSeries.Equivalent s₁ s₂

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