CompositionSeries.exists_top_eq_snoc_equivalant
theorem CompositionSeries.exists_top_eq_snoc_equivalant :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X) (x : X)
(hm : JordanHolderLattice.IsMaximal x s.top),
s.bot ≤ x → ∃ t, t.bot = s.bot ∧ t.length + 1 = s.length ∧ ∃ (htx : t.top = x), s.Equivalent (t.snoc s.top ⋯)
The theorem `CompositionSeries.exists_top_eq_snoc_equivalant` asserts the following: Given a lattice `X` and a composition series `s` in this lattice, and an element `x` of the lattice such that `x` is maximal inside `s.top`, if `s.bot` is less than or equal to `x`, then there exists another composition series `t` such that the bottom of `t` is the same as the bottom of `s`, the length of `t` is one less than the length of `s`, and the top of `t` is `x`. Furthermore, adding `s.top` to the end of `t` (denoted `t.snoc s.top`) results in a series equivalent to `s`. This theorem is an important step in the Jordan-Holder theory, which deals with the unique decomposition of series in a Jordan-Holder lattice.
More concisely: Given a lattice with a composition series and an element maximal in the series, if the series top contains the element and intersects the series bottom, then there exists a shorter composition series ending at that element, whose concatenation with the original series is series-equivalent.
|
CompositionSeries.strictMono
theorem CompositionSeries.strictMono :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X), StrictMono s.series
The theorem `CompositionSeries.strictMono` states that for any type `X` for which a lattice and a Jordan-Hölder lattice can be defined, and for any composition series `s` of type `X`, the function `s.series` is strictly monotone. This means that if `a` and `b` are any two elements in the composition series `s` such that `a < b`, then `s.series a` is strictly less than `s.series b`. This establishes an order-preserving relationship for elements in the composition series.
More concisely: For any composition series `s` of a type `X` with defined lattice and Jordan-Hölder lattice, the function `s.series` is strictly increasing on the elements of the series.
|
CompositionSeries.ext
theorem CompositionSeries.ext :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
(∀ (x : X), x ∈ s₁ ↔ x ∈ s₂) → s₁ = s₂
The theorem `CompositionSeries.ext` states that two `CompositionSeries` in a Jordan-Hölder Lattice are equal if they contain the same elements. The comparison is made for all elements of a given type `X`, where `X` is a type forming a lattice structure. This is a generalization of the principle of set equality, which states that two sets are equal if and only if they have the same elements.
More concisely: Given two `CompositionSeries` of a lattice `X`, they are equal if they contain the same elements.
|
CompositionSeries.mem_def
theorem CompositionSeries.mem_def :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x : X} {s : CompositionSeries X},
x ∈ s ↔ x ∈ Set.range s.series
This theorem states that for any type `X` with a lattice structure and a Jordan-Hölder lattice structure, any element `x` of type `X`, and any composition series `s` of type `X`, `x` is an element of the composition series `s` if and only if `x` is in the range of the series function `s.series`. This range is defined as the set of all outputs of the function `s.series`.
More concisely: For any lattice type `X` with a Jordan-Hölder structure, an element `x` lies in a composition series `s` if and only if `x` is in the image of the series function `s.series`.
|
CompositionSeries.ext_fun
theorem CompositionSeries.ext_fun :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X}
(hl : s₁.length = s₂.length), (∀ (i : Fin (s₁.length + 1)), s₁.series i = s₂.series (Fin.cast ⋯ i)) → s₁ = s₂
The theorem `CompositionSeries.ext_fun` states that for any type `X` with a `Lattice` and `JordanHolderLattice` structures, two `CompositionSeries` of `X`, say `s₁` and `s₂`, are equal if they satisfy two conditions: they have the same length and for every index `i` within the inclusive range from 0 to the length of the series, the `i`th elements of the two series are the same. Here `Fin (s₁.length + 1)` represents the set of natural numbers less than or equal to `s₁.length`, and `Fin.cast` is a function that embeds `i` into an equal `Fin` type.
More concisely: For any type `X` with lattice and Jordan-Holder lattice structures, two composition series `s₁` and `s₂` of length `n` over `X` are equal if and only if for all `i` in `[0, n]`, the `i`-th elements of `s₁` and `s₂` are equal.
|
CompositionSeries.coe_append
theorem CompositionSeries.coe_append :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s₁ s₂ : CompositionSeries X)
(h : s₁.top = s₂.bot), (s₁.append s₂ h).series = Matrix.vecAppend ⋯ (s₁.series ∘ Fin.castSucc) s₂.series
This theorem states that for any type `X` that has a lattice structure and a Jordan-Holder lattice structure, given two composition series `s₁` and `s₂` of type `X` such that the largest element of `s₁` is the smallest element of `s₂` (denoted by `h`), the series of the composition series formed by appending `s₁` and `s₂` is equal to the vector formed by appending the series of `s₁` (after embedding its indices in a larger finite set using `Fin.castSucc`) and the series of `s₂`. The function `Matrix.vecAppend` is used to perform the appending of the two series.
More concisely: For any type `X` with lattice and Jordan-Holder lattice structures, if `s₁` and `s₂` are composition series of `X` with `s₁` a subseries of `s₂` and first element `h`, then `[h :: s₁.toList] ++ s₂.toList` is the composition series obtained by appending `s₁` and `s₂`.
|
CompositionSeries.jordan_holder
theorem CompositionSeries.jordan_holder :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s₁ s₂ : CompositionSeries X),
s₁.bot = s₂.bot → s₁.top = s₂.top → s₁.Equivalent s₂
The **Jordan-Hölder Theorem**, as stated for any `JordanHolderLattice`, asserts that if two composition series, `s₁` and `s₂`, start (`s₁.bot = s₂.bot`) and finish (`s₁.top = s₂.top`) at the same place, then they are equivalent (`s₁.Equivalent s₂`). Here, `X` is any type that forms a lattice and also satisfies the properties of a `JordanHolderLattice`.
More concisely: In a Jordan-Hölder lattice `X`, two composition series with the same bottom and top elements are equivalent.
|
CompositionSeries.step
theorem CompositionSeries.step :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X) (i : Fin s.length),
JordanHolderLattice.IsMaximal (s.series i.castSucc) (s.series i.succ)
The theorem `CompositionSeries.step` states that for any type `X` that forms a Lattice and a Jordan-Hölder Lattice, and for any composition series `s` of `X`, at every index `i` of the series (represented as a `Fin` type), the element at the index `i` cast to `Fin (n + 1)` (denoted by `Fin.castSucc i`) and the successor of the index `i` (denoted by `Fin.succ i`) in the series form a maximal pair as per the definition of maximality in Jordan-Hölder Lattice. In simpler terms, for each consecutive pair of elements in the composition series, the first element is less than the second, and there are no elements between them in the lattice structure.
More concisely: For any composition series `s` of a type `X` that forms a Lattice and a Jordan-Hölder Lattice, the consecutive pairs of elements `(X.n i) (Fin.castSucc i)` in `s` satisfy `X.n i < X.n (Fin.succ i)` and there are no elements between them in the lattice structure.
|
CompositionSeries.length_toList
theorem CompositionSeries.length_toList :
∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X),
s.toList.length = s.length + 1
The theorem `CompositionSeries.length_toList` states that for any type `X` that is a Lattice and a Jordan-Hölder Lattice, and for any `s` which is a CompositionSeries of `X`, the length of the list obtained by converting `s` using the `CompositionSeries.toList` function is equal to the length of the CompositionSeries `s` plus one.
More concisely: For any CompositionSeries `s` of a Jordan-Hölder Lattice `X`, the length of the list obtained by converting `s` to a list is one more than the length of `s`.
|