Mathlib.Order.JordanHolder

Module docstring

{"# 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.last is the largest element of the series, and s.head 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 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.

[!NOTE] The previous paragraph indicates that the instance of JordanHolderLattice for submodules should be obtained via ModularLattice. This is not the case in mathlib4. See JordanHolderModule.instJordanHolderLattice. "}

JordanHolderLattice structure

(X : Type u) [Lattice X]

Full source

/-- 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.
-/
class JordanHolderLattice (X : Type u) [Lattice X] where
  IsMaximal : X → X → Prop
  lt_of_isMaximal : ∀ {x y}, IsMaximal x y → x < y
  sup_eq_of_isMaximal : ∀ {x y z}, IsMaximal x z → IsMaximal y z → x ≠ y → x ⊔ y = z
  isMaximal_inf_left_of_isMaximal_sup :
    ∀ {x y}, IsMaximal x (x ⊔ y) → IsMaximal y (x ⊔ y) → IsMaximal (x ⊓ y) x
  Iso : X × X → X × X → Prop
  iso_symm : ∀ {x y}, Iso x y → Iso y x
  iso_trans : ∀ {x y z}, Iso x y → Iso y z → Iso x z
  second_iso : ∀ {x y}, IsMaximal x (x ⊔ y) → Iso (x, x ⊔ y) (x ⊓ y, y)

Jordan-Hölder Lattice

Informal description

A Jordan-Hölder lattice is a lattice $X$ equipped with: 1. A notion of maximality: for $x, y \in X$, $\text{IsMaximal}\ x\ y$ indicates that $x$ is maximal in $y$ 2. A notion of isomorphism between pairs: $\text{Iso}\ (x₁, y₁)\ (x₂, y₂)$ indicates that the intervals $[x₁, y₁]$ and $[x₂, y₂]$ are isomorphic These must satisfy: - $\text{Iso}$ is symmetric and transitive - The second isomorphism theorem: $\text{Iso}\ (x, x ⊔ y)\ (x ⊓ y, y)$ for any $x, y \in X$ Examples include the lattice of subgroups of a group (where $\text{IsMaximal}\ H\ K$ means $H$ is a maximal normal subgroup of $K$) and the lattice of submodules of a module.

JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup theorem

{x y : X} (hxz : IsMaximal x (x ⊔ y)) (hyz : IsMaximal y (x ⊔ y)) : IsMaximal (x ⊓ y) y

Full source

theorem isMaximal_inf_right_of_isMaximal_sup {x y : X} (hxz : IsMaximal x (x ⊔ y))
    (hyz : IsMaximal y (x ⊔ y)) : IsMaximal (x ⊓ y) y := by
  rw [inf_comm]
  rw [sup_comm] at hxz hyz
  exact isMaximal_inf_left_of_isMaximal_sup hyz hxz

Maximality of Meet under Maximality Conditions in a Jordan-Hölder Lattice

Informal description

Let $X$ be a Jordan-Hölder lattice, and let $x, y \in X$. If $x$ is maximal in $x \sqcup y$ and $y$ is maximal in $x \sqcup y$, then $x \sqcap y$ is maximal in $y$.

JordanHolderLattice.isMaximal_of_eq_inf theorem

(x b : X) {a y : X} (ha : x ⊓ y = a) (hxy : x ≠ y) (hxb : IsMaximal x b) (hyb : IsMaximal y b) : IsMaximal a y

Full source

theorem isMaximal_of_eq_inf (x b : X) {a y : X} (ha : x ⊓ y = a) (hxy : x ≠ y) (hxb : IsMaximal x b)
    (hyb : IsMaximal y b) : IsMaximal a y := by
  have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
  substs a b
  exact isMaximal_inf_right_of_isMaximal_sup hxb hyb

Maximality of Meet under Distinct Maximal Elements in a Jordan-Hölder Lattice

Informal description

Let $X$ be a Jordan-Hölder lattice, and let $x, b, a, y \in X$ such that: 1. The meet of $x$ and $y$ equals $a$ (i.e., $x \sqcap y = a$) 2. $x$ and $y$ are distinct (i.e., $x \neq y$) 3. $x$ is maximal in $b$ (i.e., $\text{IsMaximal}(x, b)$) 4. $y$ is maximal in $b$ (i.e., $\text{IsMaximal}(y, b)$) Then $a$ is maximal in $y$ (i.e., $\text{IsMaximal}(a, y)$).

JordanHolderLattice.second_iso_of_eq theorem

{x y a b : X} (hm : IsMaximal x a) (ha : x ⊔ y = a) (hb : x ⊓ y = b) : Iso (x, a) (b, y)

Full source

theorem second_iso_of_eq {x y a b : X} (hm : IsMaximal x a) (ha : x ⊔ y = a) (hb : x ⊓ y = b) :
    Iso (x, a) (b, y) := by substs a b; exact second_iso hm

Second Isomorphism Theorem in Jordan-Hölder Lattices

Informal description

Let $X$ be a Jordan-Hölder lattice, and let $x, y, a, b \in X$ such that: 1. $x$ is maximal in $a$ (i.e., $\text{IsMaximal}(x, a)$) 2. The join $x \sqcup y = a$ 3. The meet $x \sqcap y = b$ Then the intervals $[x, a]$ and $[b, y]$ are isomorphic (i.e., $\text{Iso}(x, a)(b, y)$ holds).

JordanHolderLattice.IsMaximal.iso_refl theorem

{x y : X} (h : IsMaximal x y) : Iso (x, y) (x, y)

Full source

theorem IsMaximal.iso_refl {x y : X} (h : IsMaximal x y) : Iso (x, y) (x, y) :=
  second_iso_of_eq h (sup_eq_right.2 (le_of_lt (lt_of_isMaximal h)))
    (inf_eq_left.2 (le_of_lt (lt_of_isMaximal h)))

Reflexivity of Interval Isomorphism under Maximality in Jordan-Hölder Lattices

Informal description

For any elements $x$ and $y$ in a Jordan-Hölder lattice $X$, if $x$ is maximal in $y$ (i.e., $\text{IsMaximal}(x, y)$ holds), then the interval $[x, y]$ is isomorphic to itself (i.e., $\text{Iso}(x, y)(x, y)$ holds).

CompositionSeries abbrev

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

Full source

/-- 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.
-/
abbrev CompositionSeries (X : Type u) [Lattice X] [JordanHolderLattice X] : Type u :=
  RelSeries (IsMaximal (X := X))

Definition of Composition Series in a Jordan-Hölder Lattice

Informal description

A *composition series* for a Jordan-Hölder lattice $X$ is a finite strictly increasing sequence of elements $s_0 < s_1 < \cdots < s_n$ in $X$ where each consecutive pair $(s_i, s_{i+1})$ satisfies the maximality condition $\text{IsMaximal}(s_i, s_{i+1})$. The *length* of the series is defined as $n$ (one less than the number of elements). The first element $s_0$ is called the *head* and the last element $s_n$ is called the *last* element of the series.

CompositionSeries.lt_succ theorem

(s : CompositionSeries X) (i : Fin s.length) : s (Fin.castSucc i) < s (Fin.succ i)

Full source

theorem lt_succ (s : CompositionSeries X) (i : Fin s.length) :
    s (Fin.castSucc i) < s (Fin.succ i) :=
  lt_of_isMaximal (s.step _)

Strict Monotonicity of Composition Series Elements

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any index $i$ in the range $\{0, \ldots, \text{length}(s) - 1\}$, the $i$-th element $s_i$ is strictly less than the $(i+1)$-th element $s_{i+1}$ in the series.

CompositionSeries.strictMono theorem

(s : CompositionSeries X) : StrictMono s

Full source

protected theorem strictMono (s : CompositionSeries X) : StrictMono s :=
  Fin.strictMono_iff_lt_succ.2 s.lt_succ

Strict Monotonicity of Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, the function $s$ is strictly monotone. That is, for any indices $i < j$ in the series, we have $s_i < s_j$.

CompositionSeries.injective theorem

(s : CompositionSeries X) : Function.Injective s

Full source

protected theorem injective (s : CompositionSeries X) : Function.Injective s :=
  s.strictMono.injective

Injectivity of Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, the function $s$ is injective. That is, if $s_i = s_j$ for some indices $i$ and $j$, then $i = j$.

CompositionSeries.inj theorem

(s : CompositionSeries X) {i j : Fin s.length.succ} : s i = s j ↔ i = j

Full source

@[simp]
protected theorem inj (s : CompositionSeries X) {i j : Fin s.length.succ} : s i = s j ↔ i = j :=
  s.injective.eq_iff

Injectivity of Composition Series Elements

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any indices $i, j$ in the series, the elements $s_i$ and $s_j$ are equal if and only if the indices $i$ and $j$ are equal.

CompositionSeries.total theorem

{s : CompositionSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s) : x ≤ y ∨ y ≤ x

Full source

theorem total {s : CompositionSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s) : x ≤ y ∨ y ≤ x := by
  rcases Set.mem_range.1 hx with ⟨i, rfl⟩
  rcases Set.mem_range.1 hy with ⟨j, rfl⟩
  rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]
  exact le_total i j

Total Order Property of Composition Series Elements

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any two elements $x, y \in X$ that belong to $s$, either $x \leq y$ or $y \leq x$ holds. In other words, the elements of a composition series are totally ordered.

CompositionSeries.toList_sorted theorem

(s : CompositionSeries X) : s.toList.Sorted (· < ·)

Full source

theorem toList_sorted (s : CompositionSeries X) : s.toList.Sorted (· < ·) :=
  List.pairwise_iff_get.2 fun i j h => by
    dsimp only [RelSeries.toList]
    rw [List.get_ofFn, List.get_ofFn]
    exact s.strictMono h

Composition Series Elements Are Strictly Increasing

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, the list of elements in $s$ is strictly increasing (sorted with respect to the strict order relation $<$).

CompositionSeries.toList_nodup theorem

(s : CompositionSeries X) : s.toList.Nodup

Full source

theorem toList_nodup (s : CompositionSeries X) : s.toList.Nodup :=
  s.toList_sorted.nodup

Distinctness of Elements in a Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, the list of elements in $s$ has no duplicates. In other words, all elements in the series are distinct.

CompositionSeries.ext theorem

{s₁ s₂ : CompositionSeries X} (h : ∀ x, x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂

Full source

/-- Two `CompositionSeries` are equal if they have the same elements. See also `ext_fun`. -/
@[ext]
theorem ext {s₁ s₂ : CompositionSeries X} (h : ∀ x, x ∈ s₁x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂ :=
  toList_injective <|
    List.eq_of_perm_of_sorted
      (by
        classical
        exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
          (Finset.ext <| by simpa only [List.mem_toFinset, RelSeries.mem_toList]))
      s₁.toList_sorted s₂.toList_sorted

Equality of Composition Series with Identical Elements

Informal description

Let $s₁$ and $s₂$ be two composition series in a Jordan-Hölder lattice $X$. If for every element $x \in X$ we have $x \in s₁$ if and only if $x \in s₂$, then $s₁ = s₂$.

CompositionSeries.le_last theorem

{s : CompositionSeries X} (i : Fin (s.length + 1)) : s i ≤ s.last

Full source

@[simp]
theorem le_last {s : CompositionSeries X} (i : Fin (s.length + 1)) : s i ≤ s.last :=
  s.strictMono.monotone (Fin.le_last _)

Last Element is Maximal in Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any index $i$ in the series (where $i$ ranges from $0$ to the length of $s$), the $i$-th element $s_i$ is less than or equal to the last element $s_{\text{last}}$ of the series.

CompositionSeries.le_last_of_mem theorem

{s : CompositionSeries X} {x : X} (hx : x ∈ s) : x ≤ s.last

Full source

theorem le_last_of_mem {s : CompositionSeries X} {x : X} (hx : x ∈ s) : x ≤ s.last :=
  let ⟨_i, hi⟩ := Set.mem_range.2 hx
  hi ▸ le_last _

Last Element is Upper Bound in Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any element $x \in X$ that appears in $s$, we have $x \leq s_{\text{last}}$, where $s_{\text{last}}$ is the last element of the series.

CompositionSeries.head_le theorem

{s : CompositionSeries X} (i : Fin (s.length + 1)) : s.head ≤ s i

Full source

@[simp]
theorem head_le {s : CompositionSeries X} (i : Fin (s.length + 1)) : s.head ≤ s i :=
  s.strictMono.monotone (Fin.zero_le _)

Head Element is Minimal in Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any index $i$ in the series, the head element $s_0$ is less than or equal to the element $s_i$.

CompositionSeries.head_le_of_mem theorem

{s : CompositionSeries X} {x : X} (hx : x ∈ s) : s.head ≤ x

Full source

theorem head_le_of_mem {s : CompositionSeries X} {x : X} (hx : x ∈ s) : s.head ≤ x :=
  let ⟨_i, hi⟩ := Set.mem_range.2 hx
  hi ▸ head_le _

Minimality of Head Element in Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any element $x \in X$ that belongs to $s$, the head element $s_0$ of the series is less than or equal to $x$.

CompositionSeries.last_eraseLast_le theorem

(s : CompositionSeries X) : s.eraseLast.last ≤ s.last

Full source

theorem last_eraseLast_le (s : CompositionSeries X) : s.eraseLast.last ≤ s.last := by
  simp [eraseLast, last, s.strictMono.le_iff_le, Fin.le_iff_val_le_val]

Monotonicity of Last Element Under Series Truncation in Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, the last element of the series obtained by removing the last element of $s$ (denoted $s.\text{eraseLast}$) is less than or equal to the last element of $s$ itself. In other words, if $s = (s_0 < s_1 < \cdots < s_n)$, then $s_{n-1} \leq s_n$.

CompositionSeries.mem_eraseLast_of_ne_of_mem theorem

{s : CompositionSeries X} {x : X} (hx : x ≠ s.last) (hxs : x ∈ s) : x ∈ s.eraseLast

Full source

theorem mem_eraseLast_of_ne_of_mem {s : CompositionSeries X} {x : X}
    (hx : x ≠ s.last) (hxs : x ∈ s) : x ∈ s.eraseLast := by
  rcases hxs with ⟨i, rfl⟩
  have hi : (i : ℕ) < (s.length - 1).succ := by
    conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]
    exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)
  refine ⟨Fin.castSucc (n := s.length + 1) i, ?_⟩
  simp [Fin.ext_iff, Nat.mod_eq_of_lt hi]

Membership in Truncated Composition Series for Non-Last Elements

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ and any element $x \in X$, if $x$ is not the last element of $s$ ($x \neq s.\text{last}$) and $x$ belongs to $s$ ($x \in s$), then $x$ belongs to the series obtained by removing the last element of $s$ ($x \in s.\text{eraseLast}$).

CompositionSeries.mem_eraseLast theorem

{s : CompositionSeries X} {x : X} (h : 0 < s.length) : x ∈ s.eraseLast ↔ x ≠ s.last ∧ x ∈ s

Full source

theorem mem_eraseLast {s : CompositionSeries X} {x : X} (h : 0 < s.length) :
    x ∈ s.eraseLastx ∈ s.eraseLast ↔ x ≠ s.last ∧ x ∈ s := by
  simp only [RelSeries.mem_def, eraseLast]
  constructor
  · rintro ⟨i, rfl⟩
    have hi : (i : ℕ) < s.length := by
      conv_rhs => rw [← Nat.add_one_sub_one s.length, Nat.succ_sub h]
      exact i.2
    simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
  · intro h
    exact mem_eraseLast_of_ne_of_mem h.1 h.2

Characterization of Membership in Truncated Composition Series

Informal description

Let $X$ be a Jordan-Hölder lattice and $s$ a composition series in $X$ with positive length. For any element $x \in X$, we have $x \in s.\text{eraseLast}$ if and only if $x$ is not the last element of $s$ ($x \neq s.\text{last}$) and $x$ belongs to $s$ ($x \in s$).

CompositionSeries.lt_last_of_mem_eraseLast theorem

{s : CompositionSeries X} {x : X} (h : 0 < s.length) (hx : x ∈ s.eraseLast) : x < s.last

Full source

theorem lt_last_of_mem_eraseLast {s : CompositionSeries X} {x : X} (h : 0 < s.length)
    (hx : x ∈ s.eraseLast) : x < s.last :=
  lt_of_le_of_ne (le_last_of_mem ((mem_eraseLast h).1 hx).2) ((mem_eraseLast h).1 hx).1

Elements in Truncated Composition Series are Strictly Below Last Element

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ with positive length, and any element $x \in X$ that belongs to the series obtained by removing the last element of $s$ (i.e., $x \in s.\text{eraseLast}$), we have $x$ is strictly less than the last element of $s$ ($x < s.\text{last}$).

CompositionSeries.isMaximal_eraseLast_last theorem

{s : CompositionSeries X} (h : 0 < s.length) : IsMaximal s.eraseLast.last s.last

Full source

theorem isMaximal_eraseLast_last {s : CompositionSeries X} (h : 0 < s.length) :
    IsMaximal s.eraseLast.last s.last := by
  have : s.length - 1 + 1 = s.length := by
    conv_rhs => rw [← Nat.add_one_sub_one s.length]; rw [Nat.succ_sub h]
  rw [last_eraseLast, last]
  convert s.step ⟨s.length - 1, by omega⟩; ext; simp [this]

Maximality of Penultimate Element in Composition Series

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$ with length greater than 0, the last element of the series obtained by removing the actual last element of $s$ (denoted $s.\text{eraseLast}.\text{last}$) is maximal in the original last element of $s$ (denoted $s.\text{last}$). In other words, $\text{IsMaximal}(s.\text{eraseLast}.\text{last}, s.\text{last})$ holds.

CompositionSeries.snoc_eraseLast_last theorem

{s : CompositionSeries X} (h : IsMaximal s.eraseLast.last s.last) : s.eraseLast.snoc s.last h = s

Full source

@[simp]
theorem snoc_eraseLast_last {s : CompositionSeries X} (h : IsMaximal s.eraseLast.last s.last) :
    s.eraseLast.snoc s.last h = s :=
  have h : 0 < s.length :=
    Nat.pos_of_ne_zero (fun hs => ne_of_gt (lt_of_isMaximal h) <| by simp [last, Fin.ext_iff, hs])
  (eq_snoc_eraseLast h).symm

Reconstruction of Composition Series by Appending Last Element

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, if the last element of the series obtained by removing the actual last element of $s$ (denoted $s.\text{eraseLast}.\text{last}$) is maximal in the original last element of $s$ (denoted $s.\text{last}$), then appending $s.\text{last}$ back to $s.\text{eraseLast}$ with the maximality condition $h$ reconstructs the original series $s$.

CompositionSeries.Equivalent definition

(s₁ s₂ : CompositionSeries X) : Prop

Full source

/-- 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))` -/
def Equivalent (s₁ s₂ : CompositionSeries X) : Prop :=
  ∃ f : Fin s₁.length ≃ Fin s₂.length,
    ∀ i : Fin s₁.length, Iso (s₁ (Fin.castSucc i), s₁ i.succ)
      (s₂ (Fin.castSucc (f i)), s₂ (Fin.succ (f i)))

Equivalence of Composition Series in a Jordan-Hölder Lattice

Informal description

Two composition series $ s_1 $ and $ s_2 $ in a Jordan-Hölder lattice $ X $ are *equivalent* if there exists a bijection $ f $ between their indexing sets (as finite types) such that for each index $ i $, the consecutive intervals $ (s_1(i), s_1(i+1)) $ and $ (s_2(f(i)), s_2(f(i)+1)) $ are isomorphic under the lattice's notion of isomorphism `Iso`.

CompositionSeries.Equivalent.refl theorem

(s : CompositionSeries X) : Equivalent s s

Full source

@[refl]
theorem refl (s : CompositionSeries X) : Equivalent s s :=
  ⟨Equiv.refl _, fun _ => (s.step _).iso_refl⟩

Reflexivity of Composition Series Equivalence

Informal description

For any composition series $s$ in a Jordan-Hölder lattice $X$, the series $s$ is equivalent to itself. That is, there exists a bijection (specifically, the identity bijection) between the indexing sets of $s$ and itself such that for each index $i$, the consecutive intervals $(s(i), s(i+1))$ are isomorphic to themselves under the lattice's notion of isomorphism $\text{Iso}$.

CompositionSeries.Equivalent.symm theorem

{s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : Equivalent s₂ s₁

Full source

@[symm]
theorem symm {s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : Equivalent s₂ s₁ :=
  ⟨h.choose.symm, fun i => iso_symm (by simpa using h.choose_spec (h.choose.symm i))⟩

Symmetry of Composition Series Equivalence

Informal description

If two composition series $s_1$ and $s_2$ in a Jordan-Hölder lattice $X$ are equivalent (i.e., there exists a bijection between their indexing sets preserving interval isomorphisms), then $s_2$ and $s_1$ are also equivalent.

CompositionSeries.Equivalent.trans theorem

 {s₁ s₂ s₃ : CompositionSeries X} (h₁ : Equivalent s₁ s₂) (h₂ : Equivalent s₂ s₃) : Equivalent s₁ s₃

Full source

@[trans]
theorem trans {s₁ s₂ s₃ : CompositionSeries X} (h₁ : Equivalent s₁ s₂) (h₂ : Equivalent s₂ s₃) :
    Equivalent s₁ s₃ :=
  ⟨h₁.choose.trans h₂.choose,
    fun i => iso_trans (h₁.choose_spec i) (h₂.choose_spec (h₁.choose i))⟩

Transitivity of Composition Series Equivalence in Jordan-Hölder Lattices

Informal description

For any three composition series $ s_1, s_2, s_3 $ in a Jordan-Hölder lattice $ X $, if $ s_1 $ is equivalent to $ s_2 $ and $ s_2 $ is equivalent to $ s_3 $, then $ s_1 $ is equivalent to $ s_3 $. Here, equivalence means there exist bijections between their indexing sets preserving the isomorphism classes of consecutive intervals.

CompositionSeries.Equivalent.smash theorem

 {s₁ s₂ t₁ t₂ : CompositionSeries X} (hs : s₁.last = s₂.head) (ht : t₁.last = t₂.head) (h₁ : Equivalent s₁ t₁)
  (h₂ : Equivalent s₂ t₂) : Equivalent (smash s₁ s₂ hs) (smash t₁ t₂ ht)

Full source

protected theorem smash {s₁ s₂ t₁ t₂ : CompositionSeries X}
    (hs : s₁.last = s₂.head) (ht : t₁.last = t₂.head)
    (h₁ : Equivalent s₁ t₁) (h₂ : Equivalent s₂ t₂) :
    Equivalent (smash s₁ s₂ hs) (smash t₁ t₂ ht) :=
  let e : FinFin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
    calc
      Fin (s₁.length + s₂.length) ≃ (Fin s₁.length) ⊕ (Fin s₂.length) := finSumFinEquiv.symm
      _ ≃ (Fin t₁.length) ⊕ (Fin t₂.length)calc
      Fin (s₁.length + s₂.length) ≃ (Fin s₁.length) ⊕ (Fin s₂.length) := finSumFinEquiv.symm
      _ ≃ (Fin t₁.length) ⊕ (Fin t₂.length) := Equiv.sumCongr h₁.choose h₂.choose
      _ ≃ Fin (t₁.length + t₂.length) := finSumFinEquiv
  ⟨e, by
    intro i
    refine Fin.addCases ?_ ?_ i
    · intro i
      simpa [e, smash_castAdd, smash_succ_castAdd] using h₁.choose_spec i
    · intro i
      simpa [e, smash_natAdd, smash_succ_natAdd] using h₂.choose_spec i⟩

Equivalence Preservation Under Concatenation of Composition Series

Informal description

Let $s_1, s_2, t_1, t_2$ be composition series in a Jordan-Hölder lattice $X$ such that: 1. The last element of $s_1$ equals the first element of $s_2$ (i.e., $s_1.\text{last} = s_2.\text{head}$) 2. The last element of $t_1$ equals the first element of $t_2$ (i.e., $t_1.\text{last} = t_2.\text{head}$) 3. $s_1$ is equivalent to $t_1$ (denoted $s_1 \sim t_1$) 4. $s_2$ is equivalent to $t_2$ (denoted $s_2 \sim t_2$) Then the concatenated series $\text{smash}(s_1, s_2)$ is equivalent to $\text{smash}(t_1, t_2)$, where $\text{smash}$ denotes the operation of concatenating two composition series along their common endpoint.

CompositionSeries.Equivalent.snoc theorem

 {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X} {hsat₁ : IsMaximal s₁.last x₁} {hsat₂ : IsMaximal s₂.last x₂}
  (hequiv : Equivalent s₁ s₂) (hlast : Iso (s₁.last, x₁) (s₂.last, x₂)) :
  Equivalent (s₁.snoc x₁ hsat₁) (s₂.snoc x₂ hsat₂)

Full source

protected theorem snoc {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X} {hsat₁ : IsMaximal s₁.last x₁}
    {hsat₂ : IsMaximal s₂.last x₂} (hequiv : Equivalent s₁ s₂)
    (hlast : Iso (s₁.last, x₁) (s₂.last, x₂)) : Equivalent (s₁.snoc x₁ hsat₁) (s₂.snoc x₂ hsat₂) :=
  let e : FinFin s₁.length.succ ≃ Fin s₂.length.succ :=
    calc
      Fin (s₁.length + 1) ≃ Option (Fin s₁.length) := finSuccEquivLast
      _ ≃ Option (Fin s₂.length)calc
      Fin (s₁.length + 1) ≃ Option (Fin s₁.length) := finSuccEquivLast
      _ ≃ Option (Fin s₂.length) := Functor.mapEquiv Option hequiv.choose
      _ ≃ Fin (s₂.length + 1) := finSuccEquivLast.symm
  ⟨e, fun i => by
    refine Fin.lastCases ?_ ?_ i
    · simpa [e, apply_last] using hlast
    · intro i
      simpa [e, Fin.succ_castSucc] using hequiv.choose_spec i⟩

Equivalence of Extended Composition Series under Maximal Extensions and Interval Isomorphism

Informal description

Let $s_1$ and $s_2$ be two composition series in a Jordan-Hölder lattice $X$, and let $x_1, x_2 \in X$ be elements such that: 1. $x_1$ is maximal in $s_1$ (i.e., $\text{IsMaximal}(s_1.\text{last}, x_1)$) 2. $x_2$ is maximal in $s_2$ (i.e., $\text{IsMaximal}(s_2.\text{last}, x_2)$) If $s_1$ and $s_2$ are equivalent composition series (denoted $\text{Equivalent}\,s_1\,s_2$) and the intervals $(s_1.\text{last}, x_1)$ and $(s_2.\text{last}, x_2)$ are isomorphic (denoted $\text{Iso}\,(s_1.\text{last}, x_1)\,(s_2.\text{last}, x_2)$), then the extended series $s_1.\text{snoc}\,x_1$ and $s_2.\text{snoc}\,x_2$ are also equivalent. Here, $\text{snoc}$ denotes appending an element to a composition series while preserving the maximality condition between consecutive elements.

CompositionSeries.Equivalent.length_eq theorem

{s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : s₁.length = s₂.length

Full source

theorem length_eq {s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : s₁.length = s₂.length := by
  simpa using Fintype.card_congr h.choose

Length Equality of Equivalent Composition Series

Informal description

For any two equivalent composition series $s_1$ and $s_2$ in a Jordan-Hölder lattice $X$, their lengths are equal, i.e., $\text{length}(s_1) = \text{length}(s_2)$.

CompositionSeries.Equivalent.snoc_snoc_swap theorem

 {s : CompositionSeries X} {x₁ x₂ y₁ y₂ : X} {hsat₁ : IsMaximal s.last x₁} {hsat₂ : IsMaximal s.last x₂}
  {hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁} {hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂}
  (hr₁ : Iso (s.last, x₁) (x₂, y₂)) (hr₂ : Iso (x₁, y₁) (s.last, x₂)) :
  Equivalent (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)

Full source

theorem snoc_snoc_swap {s : CompositionSeries X} {x₁ x₂ y₁ y₂ : X} {hsat₁ : IsMaximal s.last x₁}
    {hsat₂ : IsMaximal s.last x₂} {hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁}
    {hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂} (hr₁ : Iso (s.last, x₁) (x₂, y₂))
    (hr₂ : Iso (x₁, y₁) (s.last, x₂)) :
    Equivalent (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (snoc (snoc s x₂ hsat₂) y₂ hsaty₂) :=
  let e : FinFin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
    Equiv.swap (Fin.last _) (Fin.castSucc (Fin.last _))
  have h1 : ∀ {i : Fin s.length},
      (Fin.castSucc (Fin.castSucc i)) ≠ (Fin.castSucc (Fin.last _)) := by simp
  have h2 : ∀ {i : Fin s.length}, (Fin.castSucc (Fin.castSucc i)) ≠ Fin.last _ := by simp
  ⟨e, by
    intro i
    dsimp only [e]
    refine Fin.lastCases ?_ (fun i => ?_) i
    · erw [Equiv.swap_apply_left, snoc_castSucc,
      show (snoc s x₁ hsat₁).toFun (Fin.last _) = x₁ from last_snoc _ _ _, Fin.succ_last,
      show ((s.snoc x₁ hsat₁).snoc y₁ hsaty₁).toFun (Fin.last _) = y₁ from last_snoc _ _ _,
      snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc, Fin.succ_last,
      show (s.snoc _ hsat₂).toFun (Fin.last _) = x₂ from last_snoc _ _ _]
      exact hr₂
    · refine Fin.lastCases ?_ (fun i => ?_) i
      · erw [Equiv.swap_apply_right, snoc_castSucc, snoc_castSucc, snoc_castSucc,
          Fin.succ_castSucc, snoc_castSucc, Fin.succ_last, last_snoc', last_snoc', last_snoc']
        exact hr₁
      · erw [Equiv.swap_apply_of_ne_of_ne h2 h1, snoc_castSucc, snoc_castSucc,
          snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc,
          Fin.succ_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc]
        exact (s.step i).iso_refl⟩

Equivalence of Doubly Extended Composition Series under Maximal Extensions and Interval Isomorphisms

Informal description

Let $s$ be a composition series in a Jordan-Hölder lattice $X$, and let $x₁, x₂, y₁, y₂ \in X$ be elements such that: 1. $x₁$ is maximal in $s$ (i.e., $\text{IsMaximal}(s.\text{last}, x₁)$) 2. $x₂$ is maximal in $s$ (i.e., $\text{IsMaximal}(s.\text{last}, x₂)$) 3. $y₁$ is maximal in the extended series $s.\text{snoc}\,x₁$ (i.e., $\text{IsMaximal}((s.\text{snoc}\,x₁).\text{last}, y₁)$) 4. $y₂$ is maximal in the extended series $s.\text{snoc}\,x₂$ (i.e., $\text{IsMaximal}((s.\text{snoc}\,x₂).\text{last}, y₂)$) If the intervals $(s.\text{last}, x₁)$ and $(x₂, y₂)$ are isomorphic (i.e., $\text{Iso}(s.\text{last}, x₁)(x₂, y₂)$) and the intervals $(x₁, y₁)$ and $(s.\text{last}, x₂)$ are isomorphic (i.e., $\text{Iso}(x₁, y₁)(s.\text{last}, x₂)$), then the doubly extended series $(s.\text{snoc}\,x₁).\text{snoc}\,y₁$ and $(s.\text{snoc}\,x₂).\text{snoc}\,y₂$ are equivalent. Here, $\text{snoc}$ denotes appending an element to a composition series while preserving the maximality condition between consecutive elements.

CompositionSeries.length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero theorem

 {s₁ s₂ : CompositionSeries X} (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) (hs₁ : s₁.length = 0) : s₂.length = 0

Full source

theorem length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero
    {s₁ s₂ : CompositionSeries X} (hb : s₁.head = s₂.head)
    (ht : s₁.last = s₂.last) (hs₁ : s₁.length = 0) : s₂.length = 0 := by
  have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm
  simpa [Fin.ext_iff]

Length Zero Preservation for Composition Series with Matching Endpoints

Informal description

Let $s_1$ and $s_2$ be two composition series in a Jordan-Hölder lattice $X$ with the same head ($s_1.\text{head} = s_2.\text{head}$) and the same last element ($s_1.\text{last} = s_2.\text{last}$). If $s_1$ has length zero, then $s_2$ must also have length zero.

CompositionSeries.length_pos_of_head_eq_head_of_last_eq_last_of_length_pos theorem

 {s₁ s₂ : CompositionSeries X} (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) : 0 < s₁.length → 0 < s₂.length

Full source

theorem length_pos_of_head_eq_head_of_last_eq_last_of_length_pos {s₁ s₂ : CompositionSeries X}
    (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) : 0 < s₁.length → 0 < s₂.length :=
  not_imp_not.1
    (by
      simpa only [pos_iff_ne_zero, ne_eq, Decidable.not_not] using
        length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb.symm ht.symm)

Positive Length Preservation for Composition Series with Matching Endpoints

Informal description

Let $s_1$ and $s_2$ be two composition series in a Jordan-Hölder lattice $X$ with the same head ($s_1.\text{head} = s_2.\text{head}$) and the same last element ($s_1.\text{last} = s_2.\text{last}$). If $s_1$ has positive length, then $s_2$ must also have positive length.

CompositionSeries.exists_last_eq_snoc_equivalent theorem

 (s : CompositionSeries X) (x : X) (hm : IsMaximal x s.last) (hb : s.head ≤ x) :
  ∃ t : CompositionSeries X,
    t.head = s.head ∧
      t.length + 1 = s.length ∧
        ∃ htx : t.last = x, Equivalent s (snoc t s.last (show IsMaximal t.last _ from htx.symm ▸ hm))

Full source

/-- 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 exists_last_eq_snoc_equivalent (s : CompositionSeries X) (x : X) (hm : IsMaximal x s.last)
    (hb : s.head ≤ x) :
    ∃ t : CompositionSeries X,
      t.head = s.head ∧ t.length + 1 = s.length ∧
      ∃ htx : t.last = x,
        Equivalent s (snoc t s.last (show IsMaximal t.last _ from htx.symm ▸ hm)) := by
  induction' hn : s.length with n ih generalizing s x
  · exact
      (ne_of_gt (lt_of_le_of_lt hb (lt_of_isMaximal hm))
          (subsingleton_of_length_eq_zero hn s.last_mem s.head_mem)).elim
  · have h0s : 0 < s.length := hn.symm ▸ Nat.succ_pos _
    by_cases hetx : s.eraseLast.last = x
    · use s.eraseLast
      simp [← hetx, hn, Equivalent.refl]
    · have imxs : IsMaximal (x ⊓ s.eraseLast.last) s.eraseLast.last :=
        isMaximal_of_eq_inf x s.last rfl (Ne.symm hetx) hm (isMaximal_eraseLast_last h0s)
      have := ih _ _ imxs (le_inf (by simpa) (le_last_of_mem s.eraseLast.head_mem)) (by simp [hn])
      rcases this with ⟨t, htb, htl, htt, hteqv⟩
      have hmtx : IsMaximal t.last x :=
        isMaximal_of_eq_inf s.eraseLast.last s.last (by rw [inf_comm, htt]) hetx
          (isMaximal_eraseLast_last h0s) hm
      use snoc t x hmtx
      refine ⟨by simp [htb], by simp [htl], by simp, ?_⟩
      have : s.Equivalent ((snoc t s.eraseLast.last <| show IsMaximal t.last _ from
        htt.symm ▸ imxs).snoc s.last
          (by simpa using isMaximal_eraseLast_last h0s)) := by
        conv_lhs => rw [eq_snoc_eraseLast h0s]
        exact Equivalent.snoc hteqv (by simpa using (isMaximal_eraseLast_last h0s).iso_refl)
      refine this.trans <| Equivalent.snoc_snoc_swap
        (iso_symm
            (second_iso_of_eq hm
              (sup_eq_of_isMaximal hm (isMaximal_eraseLast_last h0s) (Ne.symm hetx)) htt.symm))
        (second_iso_of_eq (isMaximal_eraseLast_last h0s)
            (sup_eq_of_isMaximal (isMaximal_eraseLast_last h0s) hm hetx) (by rw [inf_comm, htt]))

Existence of Equivalent Truncated Composition Series under Maximal Extension

Informal description

Let $s$ be a composition series in a Jordan-Hölder lattice $X$, and let $x \in X$ be an element such that: 1. $x$ is maximal in $s_{\text{last}}$ (i.e., $\text{IsMaximal}(x, s_{\text{last}})$) 2. $s_{\text{head}} \leq x$ Then there exists another composition series $t$ such that: 1. $t_{\text{head}} = s_{\text{head}}$ 2. The length of $t$ is one less than the length of $s$ (i.e., $t_{\text{length}} + 1 = s_{\text{length}}$) 3. $t_{\text{last}} = x$ 4. The series $s$ is equivalent to the series obtained by appending $s_{\text{last}}$ to $t$ (i.e., $\text{Equivalent}\,s\,(t.\text{snoc}\,s_{\text{last}})$)

CompositionSeries.jordan_holder theorem

(s₁ s₂ : CompositionSeries X) (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) : Equivalent s₁ s₂

Full source

/-- The **Jordan-Hölder** theorem, stated for any `JordanHolderLattice`.
If two composition series start and finish at the same place, they are equivalent. -/
theorem jordan_holder (s₁ s₂ : CompositionSeries X)
    (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) :
    Equivalent s₁ s₂ := by
  induction' hle : s₁.length with n ih generalizing s₁ s₂
  · rw [eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hle]
  · have h0s₂ : 0 < s₂.length :=
      length_pos_of_head_eq_head_of_last_eq_last_of_length_pos hb ht (hle.symm ▸ Nat.succ_pos _)
    rcases exists_last_eq_snoc_equivalent s₁ s₂.eraseLast.last
        (ht.symm ▸ isMaximal_eraseLast_last h0s₂)
        (hb.symm ▸ s₂.head_eraseLast ▸ head_le_of_mem (last_mem _)) with
      ⟨t, htb, htl, htt, hteq⟩
    have := ih t s₂.eraseLast (by simp [htb, ← hb]) htt (Nat.succ_inj.1 (htl.trans hle))
    refine hteq.trans ?_
    conv_rhs => rw [eq_snoc_eraseLast h0s₂]
    simp only [ht]
    exact Equivalent.snoc this (by simpa [htt] using (isMaximal_eraseLast_last h0s₂).iso_refl)

Jordan-Hölder Theorem for Composition Series in a Jordan-Hölder Lattice

Informal description

Let $X$ be a Jordan-Hölder lattice, and let $s_1$ and $s_2$ be two composition series in $X$ with the same head element ($s_1.\text{head} = s_2.\text{head}$) and the same last element ($s_1.\text{last} = s_2.\text{last}$). Then $s_1$ and $s_2$ are equivalent, meaning there exists a bijection between their indexing sets that preserves the isomorphism classes of consecutive intervals.