feat(Order): more API for krull dimensions (#21800)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

Mathlib/Algebra/Order/SuccPred/WithBot.lean

@@ -26,4 +26,8 @@ lemma succ_one : succ (1 : WithBot α) = 2 := by simpa [one_add_one_eq_two] usin
 lemma succ_ofNat (n : ℕ) [n.AtLeastTwo] :
     succ (ofNat(n) : WithBot α) = ofNat(n) + 1 := succ_natCast n
 
+lemma one_le_iff_pos {α : Type*} [PartialOrder α] [AddMonoidWithOne α]
+    [ZeroLEOneClass α] [NeZero (1 : α)] [SuccAddOrder α] (a : WithBot α) : 1 ≤ a ↔ 0 < a := by
+  cases a <;> simp [Order.one_le_iff_pos]
+
 end WithBot

Mathlib/Order/KrullDimension.lean

@@ -605,9 +605,41 @@ lemma krullDim_nonpos_of_subsingleton [Subsingleton α] : krullDim α ≤ 0 := b
   rw [krullDim_nonpos_iff_forall_isMax]
   exact fun x y h ↦ (Subsingleton.elim x y).ge
 
+lemma krullDim_eq_zero [Nonempty α] [Subsingleton α] :
+    krullDim α = 0 :=
+  le_antisymm krullDim_nonpos_of_subsingleton krullDim_nonneg
+
 lemma krullDim_eq_zero_of_unique [Unique α] : krullDim α = 0 :=
   le_antisymm krullDim_nonpos_of_subsingleton krullDim_nonneg
 
+section PartialOrder
+
+variable {α : Type*} [PartialOrder α]
+
+lemma krullDim_eq_zero_iff_of_orderBot [OrderBot α] :
+    krullDim α = 0 ↔ Subsingleton α :=
+  ⟨fun H ↦ subsingleton_of_forall_eq ⊥ fun _ ↦ le_bot_iff.mp
+    (krullDim_nonpos_iff_forall_isMax.mp H.le ⊥ bot_le), fun _ ↦ Order.krullDim_eq_zero⟩
+
+lemma krullDim_pos_iff_of_orderBot [OrderBot α] :
+    0 < krullDim α ↔ Nontrivial α := by
+  rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot,
+    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
+  simp [Order.krullDim_nonneg]
+
+lemma krullDim_eq_zero_iff_of_orderTop [OrderTop α] :
+    krullDim α = 0 ↔ Subsingleton α :=
+  ⟨fun H ↦ subsingleton_of_forall_eq ⊤ fun _ ↦ top_le_iff.mp
+    (krullDim_nonpos_iff_forall_isMin.mp H.le ⊤ le_top), fun _ ↦ Order.krullDim_eq_zero⟩
+
+lemma krullDim_pos_iff_of_orderTop [OrderTop α] :
+    0 < krullDim α ↔ Nontrivial α := by
+  rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderTop,
+    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
+  simp [Order.krullDim_nonneg]
+
+end PartialOrder
+
 lemma krullDim_eq_length_of_finiteDimensionalOrder [FiniteDimensionalOrder α] :
     krullDim α = (LTSeries.longestOf α).length :=
   le_antisymm

Mathlib/Order/RelSeries.lean

@@ -421,6 +421,14 @@ def cons (p : RelSeries r) (newHead : α) (rel : r newHead p.head) : RelSeries r
   delta cons
   rw [last_append]
 
+lemma cons_cast_succ (s : RelSeries r) (a : α) (h : r a s.head) (i : Fin (s.length + 1)) :
+    (s.cons a h) (.cast (by simp) (.succ i)) = s i := by
+  dsimp [cons]
+  convert append_apply_right (singleton r a) s h i
+  ext
+  show i.1 + 1 = _ % _
+  simpa using (Nat.mod_eq_of_lt (by simp)).symm
+
 /--
 Given a series `a₀ -r→ a₁ -r→ ... -r→ aₙ` and an `a` such that `aₙ -r→ a` holds, there is
 a series of length `n+1`: `a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a`.
@@ -436,6 +444,10 @@ def snoc (p : RelSeries r) (newLast : α) (rel : r p.last newLast) : RelSeries r
 @[simp] lemma last_snoc (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
     (p.snoc newLast rel).last = newLast := last_append _ _ _
 
+lemma snoc_cast_castSucc (s : RelSeries r) (a : α) (h : r s.last a) (i : Fin (s.length + 1)) :
+    (s.snoc a h) (.cast (by simp) (.castSucc i)) = s i :=
+  append_apply_left s (singleton r a) h i
+
 -- This lemma is useful because `last_snoc` is about `Fin.last (p.snoc _ _).length`, but we often
 -- see `Fin.last (p.length + 1)` in practice. They are equal by definition, but sometimes simplifier
 -- does not pick up `last_snoc`
@@ -656,6 +668,36 @@ lemma Rel.finiteDimensional_or_infiniteDimensional [Nonempty α] :
   rw [← not_finiteDimensional_iff]
   exact em r.FiniteDimensional
 
+instance Rel.FiniteDimensional.swap [FiniteDimensional r] : FiniteDimensional (Function.swap r) :=
+  ⟨.reverse (.longestOf r), fun s ↦ s.reverse.length_le_length_longestOf⟩
+
+variable {r} in
+@[simp]
+lemma Rel.finiteDimensional_swap_iff :
+    FiniteDimensional (Function.swap r) ↔ FiniteDimensional r :=
+  ⟨fun _ ↦ .swap _, fun _ ↦ .swap _⟩
+
+instance Rel.InfiniteDimensional.swap [InfiniteDimensional r] :
+    InfiniteDimensional (Function.swap r) :=
+  ⟨fun n ↦ ⟨.reverse (.withLength r n), RelSeries.length_withLength r n⟩⟩
+
+variable {r} in
+@[simp]
+lemma Rel.infiniteDimensional_swap_iff :
+    InfiniteDimensional (Function.swap r) ↔ InfiniteDimensional r :=
+  ⟨fun _ ↦ .swap _, fun _ ↦ .swap _⟩
+
+lemma Rel.wellFounded_swap_of_finiteDimensional [Rel.FiniteDimensional r] :
+    WellFounded (Function.swap r) := by
+  rw [WellFounded.wellFounded_iff_no_descending_seq]
+  refine ⟨fun ⟨f, hf⟩ ↦ ?_⟩
+  let s := RelSeries.mk (r := r) ((RelSeries.longestOf r).length + 1) (f ·) (hf ·)
+  exact (RelSeries.longestOf r).length.lt_succ_self.not_le s.length_le_length_longestOf
+
+lemma Rel.wellFounded_of_finiteDimensional [Rel.FiniteDimensional r] : WellFounded r :=
+  have : (Rel.FiniteDimensional (Function.swap r)) := Rel.finiteDimensional_swap_iff.mp ‹_›
+  wellFounded_swap_of_finiteDimensional (Function.swap r)
+
 /-- A type is finite dimensional if its `LTSeries` has bounded length. -/
 abbrev FiniteDimensionalOrder (γ : Type*) [Preorder γ] :=
   Rel.FiniteDimensional ((· < ·) : γ → γ → Prop)