comm_alg/CommAlg/StrictSeries.lean
2023-06-22 05:30:47 +00:00

583 lines
21 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2021 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the Mathlib file LICENSE.
Authors: Chris Hughes, Grant Barkley
-/
import Mathlib.Order.Lattice
import Mathlib.Data.List.Sort
import Mathlib.Logic.Equiv.Fin
import Mathlib.Logic.Equiv.Functor
import Mathlib.Data.Fintype.Card
import Mathlib.Order.Monotone.Basic
structure StrictSeries (X : Type u) [LT X] : Type u where
length :
toFun : Fin (length + 1) → X
step' : ∀ i : Fin length, (toFun (Fin.castSucc i)) < (toFun (Fin.succ i))
--StrictMono toFun
section List
-- TODO: move this to Mathlib.Data.List.Basic
@[simp]
theorem List.getLast_tail {X : Type _} {l : List X} {h : l.tail ≠ []} :
l.tail.getLast h = l.getLast (fun c => (c ▸ h) List.tail_nil) := by
cases l
. simp
. rw [List.getLast_cons]; simp; assumption
end List
namespace StrictSeries
section FinLemmas
-- TODO: move these to `VecNotation` and rename them to better describe their statement
variable {α : Type _} {m n : } (a : Fin m.succ → α) (b : Fin n.succ → α)
theorem append_castAdd_aux (i : Fin m) :
Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b
(Fin.castSucc <| Fin.castAdd n i) =
a (Fin.castSucc i) := by
cases i
simp [Matrix.vecAppend_eq_ite, *]
#align composition_series.append_cast_add_aux StrictSeries.append_castAdd_aux
theorem append_succ_castAdd_aux (i : Fin m) (h : a (Fin.last _) = b 0) :
Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b (Fin.castAdd n i).succ =
a i.succ := by
cases' i with i hi
simp only [Matrix.vecAppend_eq_ite, hi, Fin.succ_mk, Function.comp_apply, Fin.castSucc_mk,
Fin.val_mk, Fin.castAdd_mk]
split_ifs with h_1
· rfl
· have : i + 1 = m := le_antisymm hi (le_of_not_gt h_1)
calc
b ⟨i + 1 - m, by simp [this]⟩ = b 0 := congr_arg b (by simp [Fin.ext_iff, this])
_ = a (Fin.last _) := h.symm
_ = _ := congr_arg a (by simp [Fin.ext_iff, this])
#align composition_series.append_succ_cast_add_aux StrictSeries.append_succ_castAdd_aux
theorem append_natAdd_aux (i : Fin n) :
Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b
(Fin.castSucc <| Fin.natAdd m i) =
b (Fin.castSucc i) := by
cases i
simp only [Matrix.vecAppend_eq_ite, Nat.not_lt_zero, Fin.natAdd_mk, add_lt_iff_neg_left,
add_tsub_cancel_left, dif_neg, Fin.castSucc_mk, not_false_iff, Fin.val_mk]
#align composition_series.append_nat_add_aux StrictSeries.append_natAdd_aux
theorem append_succ_natAdd_aux (i : Fin n) :
Matrix.vecAppend (Nat.add_succ _ _).symm (a ∘ Fin.castSucc) b (Fin.natAdd m i).succ =
b i.succ := by
cases' i with i hi
simp only [Matrix.vecAppend_eq_ite, add_assoc, Nat.not_lt_zero, Fin.natAdd_mk,
add_lt_iff_neg_left, add_tsub_cancel_left, Fin.succ_mk, dif_neg, not_false_iff, Fin.val_mk]
#align composition_series.append_succ_nat_add_aux StrictSeries.append_succ_natAdd_aux
end FinLemmas
section LT
variable {X : Type u} [LT X]
instance IsEmpty [IsEmpty X] : IsEmpty (StrictSeries X) :=
⟨fun s => IsEmpty.false <| s.toFun 0⟩
instance coeFun : CoeFun (StrictSeries X) fun x => Fin (x.length + 1) → X where
coe := StrictSeries.toFun
instance inhabited [Inhabited X] : Inhabited (StrictSeries X) :=
⟨{ length := 0
toFun := default
step' := fun x => x.elim0 }⟩
instance Nonempty [Nonempty X] : Nonempty (StrictSeries X) :=
⟨{ length := 0
toFun := Nonempty.some inferInstance
step' := fun x => x.elim0 }⟩
theorem step (s : StrictSeries X) :
∀ i : Fin s.length, (s (Fin.castSucc i)) < (s (Fin.succ i)) :=
s.step'
theorem coeFn_mk (length : ) (toFun step) :
(@StrictSeries.mk X _ length toFun step : Fin length.succ → X) = toFun :=
rfl
theorem lt_succ (s : StrictSeries X) (i : Fin s.length) :
s (Fin.castSucc i) < s (Fin.succ i) :=
(s.step _)
instance membership : Membership X (StrictSeries X) :=
⟨fun x s => x ∈ Set.range s⟩
theorem mem_def {x : X} {s : StrictSeries X} : x ∈ s ↔ x ∈ Set.range s :=
Iff.rfl
/-- The ordered `List X` of elements of a `StrictSeries X`. -/
def toList (s : StrictSeries X) : List X :=
List.ofFn s
/-- Two `StrictSeries` are equal if they are the same length and
have the same `i`th element for every `i` -/
theorem ext_fun {s₁ s₂ : StrictSeries X} (hl : s₁.length = s₂.length)
(h : ∀ i, s₁ i = s₂ (Fin.cast (congr_arg Nat.succ hl) i)) : s₁ = s₂ := by
cases s₁; cases s₂
-- Porting note: `dsimp at *` doesn't work. Why?
dsimp at hl h
subst hl
simpa [Function.funext_iff] using h
@[simp]
theorem length_toList (s : StrictSeries X) : s.toList.length = s.length + 1 := by
rw [toList, List.length_ofFn]
theorem toList_ne_nil (s : StrictSeries X) : s.toList ≠ [] := by
rw [← List.length_pos_iff_ne_nil, length_toList]; exact Nat.succ_pos _
theorem chain'_toList (s : StrictSeries X) : List.Chain' (· < ·) s.toList :=
List.chain'_iff_get.2
(by
intro i hi
simp only [toList, List.get_ofFn]
rw [length_toList] at hi
exact s.step ⟨i, hi⟩)
@[simp]
theorem mem_toList {s : StrictSeries X} {x : X} : x ∈ s.toList ↔ x ∈ s := by
rw [toList, List.mem_ofFn, mem_def]
/-- Make a `StrictSeries X` from the ordered list of its elements. -/
def ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' (· < ·) l) : StrictSeries X
where
length := l.length - 1
toFun i :=
l.nthLe i
(by
conv_rhs => rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
exact i.2)
step' := fun ⟨i, hi⟩ => List.chain'_iff_get.1 hc i hi
theorem length_ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' (· < ·) l) :
(ofList l hl hc).length = l.length - 1 :=
rfl
theorem ofList_toList (s : StrictSeries X) :
ofList s.toList s.toList_ne_nil s.chain'_toList = s := by
refine' ext_fun _ _
· rw [length_ofList, length_toList, Nat.succ_sub_one]
· rintro ⟨i, hi⟩
simp [ofList, toList, -List.ofFn_succ]
@[simp]
theorem ofList_toList' (s : StrictSeries X) :
ofList s.toList s.toList_ne_nil s.chain'_toList = s :=
ofList_toList s
@[simp]
theorem toList_ofList (l : List X) (hl : l ≠ []) (hc : List.Chain' (· < ·) l) :
toList (ofList l hl hc) = l := by
refine' List.ext_get _ _
· rw [length_toList, length_ofList,
tsub_add_cancel_of_le (Nat.succ_le_of_lt <| List.length_pos_of_ne_nil hl)]
· intro i hi hi'
dsimp [ofList, toList]
rw [List.get_ofFn]
rfl
theorem toList_injective : Function.Injective (@StrictSeries.toList X _) :=
fun s₁ s₂ (h : List.ofFn s₁ = List.ofFn s₂) => by
have h₁ : s₁.length = s₂.length :=
Nat.succ_injective
((List.length_ofFn s₁).symm.trans <| (congr_arg List.length h).trans <| List.length_ofFn s₂)
have h₂ : ∀ i : Fin s₁.length.succ, s₁ i = s₂ (Fin.cast (congr_arg Nat.succ h₁) i) :=
congr_fun <| List.ofFn_injective <| h.trans <| List.ofFn_congr (congr_arg Nat.succ h₁).symm _
cases s₁
cases s₂
dsimp at h h₁ h₂
subst h₁
simp only [mk.injEq, heq_eq_eq, true_and]
simp only [Fin.cast_refl] at h₂
exact funext h₂
theorem ext_list {s₁ s₂ : StrictSeries X} (h : toList s₁ = toList s₂) : s₁ = s₂ :=
toList_injective h
def ofElement (x : X) : StrictSeries X where
length := 0
toFun _ := x
step' := by simp
@[simp]
theorem length_ofElement (x : X) :
(ofElement x).length = 0 := rfl
@[simp]
theorem toList_ofElement (x : X) : toList (ofElement x) = [x] := by
obtain ⟨a, ha⟩ := List.length_eq_one.mp (length_ofElement x ▸ length_toList <| ofElement x)
have := List.eq_of_mem_singleton <| ha ▸ (mem_toList.mpr ⟨0, rfl⟩ : x ∈ toList (ofElement x))
rw [(ha : toList (ofElement x) = _), this]
@[simp]
theorem mem_ofElement (x : X) {y : X} : y ∈ (ofElement x) ↔ y = x := by
rw [←mem_toList, toList_ofElement, List.mem_singleton]
@[simp]
theorem ofList_singleton {x : X} {hne} {hch} : ofList [x] hne hch = ofElement x := by
apply ext_list
rw [toList_ofList, toList_ofElement]
theorem length_eq_zero {s : StrictSeries X} :
s.length = 0 ↔ ∃ x, s = ofElement x :=
⟨fun h =>
have ⟨a, ha⟩ := List.length_eq_one.mp (h ▸ (length_toList s))
⟨a, by apply ext_list; rw [ha, toList_ofElement]⟩,
fun ⟨x, h⟩ => h.symm ▸ length_ofElement x⟩
theorem ofElement_of_length_zero {s : StrictSeries X} (h : s.length = 0) (hx : x ∈ s) :
s = ofElement x := by
have ⟨y, hy⟩ := length_eq_zero.mp h
-- bug? can't inline this
have := mem_ofElement y |>.mp <| hy ▸ hx
rwa [this]
/-- The last element of a `StrictSeries` -/
def top (s : StrictSeries X) : X :=
s (Fin.last _)
theorem top_mem (s : StrictSeries X) : s.top ∈ s :=
mem_def.2 (Set.mem_range.2 ⟨Fin.last _, rfl⟩)
@[simp]
theorem ofElement_top {x : X} : (ofElement x).top = x := rfl
@[simp]
theorem getLast_toList_eq_top (s : StrictSeries X) : s.toList.getLast s.toList_ne_nil = s.top := by
erw [List.last_ofFn]; rfl
@[simp]
theorem top_ofList {l : List X} {hnn} {hcn} : (ofList l hnn hcn).top = l.getLast hnn := by
rw [←getLast_toList_eq_top]; simp
theorem length_eq_zero_top {s : StrictSeries X} : s.length = 0 ↔ s = ofElement s.top :=
⟨fun h => ofElement_of_length_zero h (top_mem s), fun h => h.symm ▸ length_ofElement _⟩
/-- The first element of a `StrictSeries` -/
def bot (s : StrictSeries X) : X :=
s 0
theorem bot_mem (s : StrictSeries X) : s.bot ∈ s :=
mem_def.2 (Set.mem_range.2 ⟨0, rfl⟩)
@[simp]
theorem ofElement_bot {x : X} : (ofElement x).bot = x := rfl
theorem length_eq_zero_bot {s : StrictSeries X} : s.length = 0 ↔ s = ofElement s.bot :=
⟨fun h => ofElement_of_length_zero h (bot_mem s), fun h => h.symm ▸ length_ofElement _⟩
/-- Remove the largest element from a `StrictSeries`. If the toFun `s`
has length zero, then `s.eraseTop = s` -/
@[simps]
def eraseTop (s : StrictSeries X) : StrictSeries X
where
length := s.length - 1
toFun i := s ⟨i, lt_of_lt_of_le i.2 (Nat.succ_le_succ tsub_le_self)⟩
step' i := by
have := s.step ⟨i, lt_of_lt_of_le i.2 tsub_le_self⟩
cases i
exact this
theorem top_eraseTop (s : StrictSeries X) :
s.eraseTop.top = s ⟨s.length - 1, lt_of_le_of_lt tsub_le_self (Nat.lt_succ_self _)⟩ :=
show s _ = s _ from
congr_arg s
(by
ext
simp only [eraseTop_length, Fin.val_last, Fin.coe_castSucc, Fin.coe_ofNat_eq_mod,
Fin.val_mk])
@[simp]
theorem bot_eraseTop (s : StrictSeries X) : s.eraseTop.bot = s.bot :=
rfl
def eraseBot (s : StrictSeries X) : StrictSeries X :=
if h : s.length = 0 then s
else
ofList (s.toList.tail)
(fun hc => h <| s.length_toList ▸ hc ▸ s.toList.length_tail |>.symm) s.chain'_toList.tail
#check Function.invFun
theorem top_eraseBot (s : StrictSeries X) : s.eraseBot.top = s.top :=
if h : s.length = 0 then by rw [eraseBot, dif_pos h]
else by rw [eraseBot, dif_neg h]; simp
/-- Append two composition toFun `s₁` and `s₂` such that
the least element of `s₁` is the maximum element of `s₂`. -/
@[simps length]
def append (s₁ s₂ : StrictSeries X) (h : s₁.top = s₂.bot) : StrictSeries X where
length := s₁.length + s₂.length
toFun := Matrix.vecAppend (Nat.add_succ s₁.length s₂.length).symm (s₁ ∘ Fin.castSucc) s₂
step' i := by
refine' Fin.addCases _ _ i
· intro i
rw [append_succ_castAdd_aux _ _ _ h, append_castAdd_aux]
exact s₁.step i
· intro i
rw [append_natAdd_aux, append_succ_natAdd_aux]
exact s₂.step i
theorem coe_append (s₁ s₂ : StrictSeries X) (h) :
⇑(s₁.append s₂ h) = Matrix.vecAppend (Nat.add_succ _ _).symm (s₁ ∘ Fin.castSucc) s₂ :=
rfl
@[simp]
theorem append_castAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot) (i : Fin s₁.length) :
append s₁ s₂ h (Fin.castSucc <| Fin.castAdd s₂.length i) = s₁ (Fin.castSucc i) := by
rw [coe_append, append_castAdd_aux _ _ i]
@[simp]
theorem append_succ_castAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot)
(i : Fin s₁.length) : append s₁ s₂ h (Fin.castAdd s₂.length i).succ = s₁ i.succ := by
rw [coe_append, append_succ_castAdd_aux _ _ _ h]
@[simp]
theorem append_natAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot) (i : Fin s₂.length) :
append s₁ s₂ h (Fin.castSucc <| Fin.natAdd s₁.length i) = s₂ (Fin.castSucc i) := by
rw [coe_append, append_natAdd_aux _ _ i]
@[simp]
theorem append_succ_natAdd {s₁ s₂ : StrictSeries X} (h : s₁.top = s₂.bot) (i : Fin s₂.length) :
append s₁ s₂ h (Fin.natAdd s₁.length i).succ = s₂ i.succ := by
rw [coe_append, append_succ_natAdd_aux _ _ i]
/-- Add an element to the top of a `StrictSeries` -/
@[simps length]
def snoc (s : StrictSeries X) (x : X) (hsat : s.top < x) : StrictSeries X where
length := s.length + 1
toFun := Fin.snoc s x
step' i := by
refine' Fin.lastCases _ _ i
· rwa [Fin.snoc_castSucc, Fin.succ_last, Fin.snoc_last, ← top]
· intro i
rw [Fin.snoc_castSucc, ← Fin.castSucc_fin_succ, Fin.snoc_castSucc]
exact s.step _
#align composition_series.snoc StrictSeries.snoc
@[simp]
theorem top_snoc (s : StrictSeries X) (x : X) (hsat : s.top < x) :
(snoc s x hsat).top = x :=
Fin.snoc_last (α := fun _ => X) _ _
#align composition_series.top_snoc StrictSeries.top_snoc
@[simp]
theorem snoc_last (s : StrictSeries X) (x : X) (hsat : s.top < x) :
snoc s x hsat (Fin.last (s.length + 1)) = x :=
Fin.snoc_last (α := fun _ => X) _ _
#align composition_series.snoc_last StrictSeries.snoc_last
@[simp]
theorem snoc_castSucc (s : StrictSeries X) (x : X) (hsat : s.top < x)
(i : Fin (s.length + 1)) : snoc s x hsat (Fin.castSucc i) = s i :=
Fin.snoc_castSucc (α := fun _ => X) _ _ _
#align composition_series.snoc_cast_succ StrictSeries.snoc_castSucc
@[simp]
theorem bot_snoc (s : StrictSeries X) (x : X) (hsat : s.top < x) :
(snoc s x hsat).bot = s.bot := by rw [bot, bot, ← snoc_castSucc s _ _ 0, Fin.castSucc_zero]
#align composition_series.bot_snoc StrictSeries.bot_snoc
theorem mem_snoc {s : StrictSeries X} {x y : X} {hsat : s.top < x} :
y ∈ snoc s x hsat ↔ y ∈ s y = x := by
simp only [snoc, mem_def]
constructor
· rintro ⟨i, rfl⟩
refine' Fin.lastCases _ (fun i => _) i
· right
simp
· left
simp
· intro h
rcases h with (⟨i, rfl⟩ | rfl)
· use Fin.castSucc i
simp
· use Fin.last _
simp
#align composition_series.mem_snoc StrictSeries.mem_snoc
end LT
section Preorder
variable {X : Type _} [Preorder X]
protected theorem strictMono (s : StrictSeries X) : StrictMono s :=
Fin.strictMono_iff_lt_succ.2 s.lt_succ
protected theorem injective (s : StrictSeries X) : Function.Injective s :=
s.strictMono.injective
@[simp]
protected theorem inj (s : StrictSeries X) {i j : Fin s.length.succ} : s i = s j ↔ i = j :=
s.injective.eq_iff
theorem total {s : StrictSeries 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
theorem toList_sorted (s : StrictSeries X) : s.toList.Sorted (· < ·) :=
List.pairwise_iff_get.2 fun i j h => by
dsimp [toList]
rw [List.get_ofFn, List.get_ofFn]
exact s.strictMono h
theorem toList_nodup (s : StrictSeries X) : s.toList.Nodup :=
s.toList_sorted.nodup
/-- Two `StrictSeries` on a preorder are equal if they have the same elements.
See also `ext_fun` and `ext_list`. -/
@[ext]
theorem ext {s₁ s₂ : StrictSeries X} (h : ∀ x, 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 simp [*]))
s₁.toList_sorted s₂.toList_sorted
@[simp]
theorem le_top {s : StrictSeries X} (i : Fin (s.length + 1)) : s i ≤ s.top :=
s.strictMono.monotone (Fin.le_last _)
theorem le_top_of_mem {s : StrictSeries X} {x : X} (hx : x ∈ s) : x ≤ s.top :=
let ⟨_i, hi⟩ := Set.mem_range.2 hx
hi ▸ le_top _
@[simp]
theorem bot_le {s : StrictSeries X} (i : Fin (s.length + 1)) : s.bot ≤ s i :=
s.strictMono.monotone (Fin.zero_le _)
theorem bot_le_of_mem {s : StrictSeries X} {x : X} (hx : x ∈ s) : s.bot ≤ x :=
let ⟨_i, hi⟩ := Set.mem_range.2 hx
hi ▸ bot_le _
-- TODO this should be in section LT
theorem length_pos_of_mem_ne {s : StrictSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s)
(hxy : x ≠ y) : 0 < s.length :=
let ⟨i, hi⟩ := hx
let ⟨j, hj⟩ := hy
have hij : i ≠ j := mt s.inj.2 fun h => hxy (hi ▸ hj ▸ h)
hij.lt_or_lt.elim
(fun hij => lt_of_le_of_lt (zero_le (i : )) (lt_of_lt_of_le hij (Nat.le_of_lt_succ j.2)))
fun hji => lt_of_le_of_lt (zero_le (j : )) (lt_of_lt_of_le hji (Nat.le_of_lt_succ i.2))
-- TODO this should be in section LT
theorem forall_mem_eq_of_length_eq_zero {s : StrictSeries X} (hs : s.length = 0) {x y}
(hx : x ∈ s) (hy : y ∈ s) : x = y :=
by_contradiction fun hxy => pos_iff_ne_zero.1 (length_pos_of_mem_ne hx hy hxy) hs
theorem eraseTop_top_le (s : StrictSeries X) : s.eraseTop.top ≤ s.top := by
simp [eraseTop, top, s.strictMono.le_iff_le, Fin.le_iff_val_le_val, tsub_le_self]
-- TODO this should be in section LT
theorem mem_eraseTop_of_ne_of_mem {s : StrictSeries X} {x : X} (hx : x ≠ s.top) (hxs : x ∈ s) :
x ∈ s.eraseTop := by
rcases hxs with ⟨i, rfl⟩
have hi : (i : ) < (s.length - 1).succ := by
conv_rhs => rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [top, s.inj, Fin.ext_iff] using hx)
refine' ⟨Fin.castSucc i, _⟩
simp [Fin.ext_iff, Nat.mod_eq_of_lt hi]
theorem mem_eraseTop {s : StrictSeries X} {x : X} (h : 0 < s.length) :
x ∈ s.eraseTop ↔ x ≠ s.top ∧ x ∈ s := by
simp only [mem_def]
dsimp only [eraseTop]
constructor
· rintro ⟨i, rfl⟩
have hi : (i : ) < s.length := by
conv_rhs => rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
exact i.2
simp [top, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
· intro h
exact mem_eraseTop_of_ne_of_mem h.1 h.2
theorem lt_top_of_mem_eraseTop {s : StrictSeries X} {x : X} (h : 0 < s.length)
(hx : x ∈ s.eraseTop) : x < s.top := by
rw [mem_eraseTop h] at hx
let ⟨i, hi⟩ := Set.mem_range.2 hx.2
rw [←hi]
apply s.strictMono
apply lt_of_le_of_ne i.le_last
intro hc
exact ((hc ▸ hi).symm ▸ hx).1 rfl
--hi ▸ le_top _
-- lt_of_le_of_ne (le_top_of_mem ((mem_eraseTop h).1 hx).2) ((mem_eraseTop h).1 hx).1
-- #align composition_series.lt_top_of_mem_erase_top StrictSeries.lt_top_of_mem_eraseTop
theorem isMaximal_eraseTop_top {s : StrictSeries X} (h : 0 < s.length) :
s.eraseTop.top < s.top := lt_top_of_mem_eraseTop h (top_mem _)
-- have : s.length - 1 + 1 = s.length := by
-- conv_rhs => rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
-- rw [top_eraseTop, top]
-- convert s.step ⟨s.length - 1, Nat.sub_lt h zero_lt_one⟩; ext; simp [this]
-- #align composition_series.is_maximal_erase_top_top StrictSeries.isMaximal_eraseTop_top
-- TODO should be in LT
theorem eq_snoc_eraseTop {s : StrictSeries X} (h : 0 < s.length) :
s = snoc (eraseTop s) s.top (isMaximal_eraseTop_top h) := by
ext x
simp [mem_snoc, mem_eraseTop h]
by_cases h : x = s.top <;> simp [*, s.top_mem]
-- TODO should be in LT
@[simp]
theorem snoc_eraseTop_top {s : StrictSeries X} (h : s.eraseTop.top < s.top) :
s.eraseTop.snoc s.top h = s :=
have h : 0 < s.length :=
Nat.pos_of_ne_zero
(by
intro hs
refine' ne_of_gt h _
simp [top, Fin.ext_iff, hs])
(eq_snoc_eraseTop h).symm
-- section `Equivalent` doesn't apply here
theorem length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {s₁ s₂ : StrictSeries X}
(hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) (hs₁ : s₁.length = 0) : s₂.length = 0 := by
have : s₁.bot = s₁.top := congr_arg s₁ (Fin.ext (by simp [hs₁]))
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
s₂.injective (hb.symm.trans (this.trans ht)).symm
-- Porting note: Was `simpa [Fin.ext_iff]`.
rw [Fin.ext_iff] at this
simpa
theorem length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos {s₁ s₂ : StrictSeries X}
(hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) : 0 < s₁.length → 0 < s₂.length :=
not_imp_not.1
(by
simp only [pos_iff_ne_zero, Ne.def, not_iff_not, Classical.not_not]
exact length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb.symm ht.symm)
theorem eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero {s₁ s₂ : StrictSeries X}
(hb : s₁.bot = s₂.bot) (ht : s₁.top = s₂.top) (hs₁0 : s₁.length = 0) : s₁ = s₂ := by
have : ∀ x, x ∈ s₁ ↔ x = s₁.top := fun x =>
⟨fun hx => forall_mem_eq_of_length_eq_zero hs₁0 hx s₁.top_mem, fun hx => hx.symm ▸ s₁.top_mem⟩
have : ∀ x, x ∈ s₂ ↔ x = s₂.top := fun x =>
⟨fun hx =>
forall_mem_eq_of_length_eq_zero
(length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb ht hs₁0) hx s₂.top_mem,
fun hx => hx.symm ▸ s₂.top_mem⟩
ext
simp [*]
end Preorder
end StrictSeries