|
| 1 | +/- |
| 2 | +Copyright (c) 2023 Jujian Zhang. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Jujian Zhang |
| 5 | +-/ |
| 6 | +import Mathlib.Logic.Equiv.Fin |
| 7 | +import Mathlib.Data.List.Indexes |
| 8 | +import Mathlib.Data.Rel |
| 9 | + |
| 10 | +/-! |
| 11 | +# Series of a relation |
| 12 | +
|
| 13 | +If `r` is a relation on `α` then a relation series of length `n` is a series |
| 14 | +`a_0, a_1, ..., a_n` such that `r a_i a_{i+1}` for all `i < n` |
| 15 | +
|
| 16 | +-/ |
| 17 | + |
| 18 | +variable {α : Type _} (r : Rel α α) |
| 19 | + |
| 20 | +/-- |
| 21 | +Let `r` be a relation on `α`, a relation series of `r` of length `n` is a series |
| 22 | +`a_0, a_1, ..., a_n` such that `r a_i a_{i+1}` for all `i < n` |
| 23 | +-/ |
| 24 | +structure RelSeries where |
| 25 | + /-- The number of inequalities in the series -/ |
| 26 | + length : ℕ |
| 27 | + /-- The underlying function of a relation series -/ |
| 28 | + toFun : Fin (length + 1) → α |
| 29 | + /-- Adjacent elements are related -/ |
| 30 | + step : ∀ (i : Fin length), r (toFun (Fin.castSucc i)) (toFun i.succ) |
| 31 | + |
| 32 | +namespace RelSeries |
| 33 | + |
| 34 | +instance : CoeFun (RelSeries r) (fun x ↦ Fin (x.length + 1) → α) := |
| 35 | +{ coe := RelSeries.toFun } |
| 36 | + |
| 37 | +/-- |
| 38 | +For any type `α`, each term of `α` gives a relation series with the right most index to be 0. |
| 39 | +-/ |
| 40 | +@[simps!] def singleton (a : α) : RelSeries r where |
| 41 | + length := 0 |
| 42 | + toFun _ := a |
| 43 | + step := Fin.elim0 |
| 44 | + |
| 45 | +instance [IsEmpty α] : IsEmpty (RelSeries r) where |
| 46 | + false x := IsEmpty.false (x 0) |
| 47 | + |
| 48 | +instance [Inhabited α] : Inhabited (RelSeries r) where |
| 49 | + default := singleton r default |
| 50 | + |
| 51 | +instance [Nonempty α] : Nonempty (RelSeries r) := |
| 52 | + Nonempty.map (singleton r) inferInstance |
| 53 | + |
| 54 | +variable {r} |
| 55 | + |
| 56 | +@[ext] |
| 57 | +lemma ext {x y : RelSeries r} (length_eq : x.length = y.length) |
| 58 | + (toFun_eq : x.toFun = y.toFun ∘ Fin.cast (by rw [length_eq])) : x = y := by |
| 59 | + rcases x with ⟨nx, fx⟩ |
| 60 | + dsimp only at length_eq toFun_eq |
| 61 | + subst length_eq toFun_eq |
| 62 | + rfl |
| 63 | + |
| 64 | +lemma rel_of_lt [IsTrans α r] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i < j) : |
| 65 | + r (x i) (x j) := |
| 66 | + (Fin.liftFun_iff_succ r).mpr x.step h |
| 67 | + |
| 68 | +lemma rel_or_eq_of_le [IsTrans α r] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i ≤ j) : |
| 69 | + r (x i) (x j) ∨ x i = x j := |
| 70 | + h.lt_or_eq.imp (x.rel_of_lt ·) (by rw [·]) |
| 71 | + |
| 72 | +/-- |
| 73 | +Given two relations `r, s` on `α` such that `r ≤ s`, any relation series of `r` induces a relation |
| 74 | +series of `s` |
| 75 | +-/ |
| 76 | +@[simps!] |
| 77 | +def ofLE (x : RelSeries r) {s : Rel α α} (h : r ≤ s) : RelSeries s where |
| 78 | + length := x.length |
| 79 | + toFun := x |
| 80 | + step _ := h _ _ <| x.step _ |
| 81 | + |
| 82 | +lemma coe_ofLE (x : RelSeries r) {s : Rel α α} (h : r ≤ s) : |
| 83 | + (x.ofLE h : _ → _) = x := rfl |
| 84 | + |
| 85 | +/-- Every relation series gives a list -/ |
| 86 | +abbrev toList (x : RelSeries r) : List α := List.ofFn x |
| 87 | + |
| 88 | +lemma toList_chain' (x : RelSeries r) : x.toList.Chain' r := by |
| 89 | + rw [List.chain'_iff_get] |
| 90 | + intros i h |
| 91 | + convert x.step ⟨i, by simpa using h⟩ <;> apply List.get_ofFn |
| 92 | + |
| 93 | +lemma toList_ne_empty (x : RelSeries r) : x.toList ≠ [] := fun m => |
| 94 | + List.eq_nil_iff_forall_not_mem.mp m (x 0) <| (List.mem_ofFn _ _).mpr ⟨_, rfl⟩ |
| 95 | + |
| 96 | +/-- Every nonempty list satisfying the chain condition gives a relation series-/ |
| 97 | +@[simps] |
| 98 | +def fromListChain' (x : List α) (x_ne_empty : x ≠ []) (hx : x.Chain' r) : RelSeries r where |
| 99 | + length := x.length.pred |
| 100 | + toFun := x.get ∘ Fin.cast (Nat.succ_pred_eq_of_pos <| List.length_pos.mpr x_ne_empty) |
| 101 | + step i := List.chain'_iff_get.mp hx i i.2 |
| 102 | + |
| 103 | +/-- Relation series of `r` and nonempty list of `α` satisfying `r`-chain condition bijectively |
| 104 | +corresponds to each other.-/ |
| 105 | +protected def Equiv : RelSeries r ≃ {x : List α | x ≠ [] ∧ x.Chain' r} where |
| 106 | + toFun x := ⟨_, x.toList_ne_empty, x.toList_chain'⟩ |
| 107 | + invFun x := fromListChain' _ x.2.1 x.2.2 |
| 108 | + left_inv x := ext (by simp) <| by ext; apply List.get_ofFn |
| 109 | + right_inv x := by |
| 110 | + refine Subtype.ext (List.ext_get ?_ <| fun n hn1 _ => List.get_ofFn _ _) |
| 111 | + simp [Nat.succ_pred_eq_of_pos <| List.length_pos.mpr x.2.1] |
| 112 | + |
| 113 | +-- TODO : build a similar bijection between `RelSeries α` and `Quiver.Path` |
| 114 | + |
| 115 | +end RelSeries |
| 116 | + |
| 117 | +namespace Rel |
| 118 | + |
| 119 | +/-- A relation `r` is said to be finite dimensional iff there is a relation series of `r` with the |
| 120 | + maximum length. -/ |
| 121 | +class FiniteDimensional : Prop where |
| 122 | + /-- A relation `r` is said to be finite dimensional iff there is a relation series of `r` with the |
| 123 | + maximum length. -/ |
| 124 | + exists_longest_relSeries : ∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length ≤ x.length |
| 125 | + |
| 126 | +/-- A relation `r` is said to be infinite dimensional iff there exists relation series of arbitrary |
| 127 | + length. -/ |
| 128 | +class InfiniteDimensional : Prop where |
| 129 | + /-- A relation `r` is said to be infinite dimensional iff there exists relation series of |
| 130 | + arbitrary length. -/ |
| 131 | + exists_relSeries_with_length : ∀ (n : ℕ), ∃ (x : RelSeries r), x.length = n |
| 132 | + |
| 133 | +end Rel |
| 134 | + |
| 135 | +namespace RelSeries |
| 136 | + |
| 137 | +/-- The longest relational series when a relation is finite dimensional -/ |
| 138 | +protected noncomputable def longestOf [r.FiniteDimensional] : RelSeries r := |
| 139 | + Rel.FiniteDimensional.exists_longest_relSeries.choose |
| 140 | + |
| 141 | +lemma length_le_length_longestOf [r.FiniteDimensional] (x : RelSeries r) : |
| 142 | + x.length ≤ (RelSeries.longestOf r).length := |
| 143 | + Rel.FiniteDimensional.exists_longest_relSeries.choose_spec _ |
| 144 | + |
| 145 | +/-- A relation series with length `n` if the relation is infinite dimensional -/ |
| 146 | +protected noncomputable def withLength [r.InfiniteDimensional] (n : ℕ) : RelSeries r := |
| 147 | + (Rel.InfiniteDimensional.exists_relSeries_with_length n).choose |
| 148 | + |
| 149 | +@[simp] lemma length_withLength [r.InfiniteDimensional] (n : ℕ) : |
| 150 | + (RelSeries.withLength r n).length = n := |
| 151 | + (Rel.InfiniteDimensional.exists_relSeries_with_length n).choose_spec |
| 152 | + |
| 153 | +/-- If a relation on `α` is infinite dimensional, then `α` is nonempty. -/ |
| 154 | +lemma nonempty_of_infiniteDimensional [r.InfiniteDimensional] : Nonempty α := |
| 155 | + ⟨RelSeries.withLength r 0 0⟩ |
| 156 | + |
| 157 | +end RelSeries |
| 158 | + |
| 159 | +/-- A type is finite dimensional if its `LTSeries` has bounded length. -/ |
| 160 | +abbrev FiniteDimensionalOrder (γ : Type _) [Preorder γ] := |
| 161 | + Rel.FiniteDimensional ((. < .) : γ → γ → Prop) |
| 162 | + |
| 163 | +/-- A type is infinite dimensional if it has `LTSeries` of at least arbitrary length -/ |
| 164 | +abbrev InfiniteDimensionalOrder (γ : Type _) [Preorder γ] := |
| 165 | + Rel.InfiniteDimensional ((. < .) : γ → γ → Prop) |
| 166 | + |
| 167 | +section LTSeries |
| 168 | + |
| 169 | +variable (α) [Preorder α] |
| 170 | +/-- |
| 171 | +If `α` is a preorder, a LTSeries is a relation series of the less than relation. |
| 172 | +-/ |
| 173 | +abbrev LTSeries := RelSeries ((. < .) : Rel α α) |
| 174 | + |
| 175 | +namespace LTSeries |
| 176 | + |
| 177 | +/-- The longest `<`-series when a type is finite dimensional -/ |
| 178 | +protected noncomputable def longestOf [FiniteDimensionalOrder α] : LTSeries α := |
| 179 | + RelSeries.longestOf _ |
| 180 | + |
| 181 | +/-- A `<`-series with length `n` if the relation is infinite dimensional -/ |
| 182 | +protected noncomputable def withLength [InfiniteDimensionalOrder α] (n : ℕ) : LTSeries α := |
| 183 | + RelSeries.withLength _ n |
| 184 | + |
| 185 | +@[simp] lemma length_withLength [InfiniteDimensionalOrder α] (n : ℕ) : |
| 186 | + (LTSeries.withLength α n).length = n := |
| 187 | + RelSeries.length_withLength _ _ |
| 188 | + |
| 189 | +/-- if `α` is infinite dimensional, then `α` is nonempty. -/ |
| 190 | +lemma nonempty_of_infiniteDimensionalType [InfiniteDimensionalOrder α] : Nonempty α := |
| 191 | + ⟨LTSeries.withLength α 0 0⟩ |
| 192 | + |
| 193 | +variable {α} |
| 194 | + |
| 195 | +lemma longestOf_is_longest [FiniteDimensionalOrder α] (x : LTSeries α) : |
| 196 | + x.length ≤ (LTSeries.longestOf α).length := |
| 197 | + RelSeries.length_le_length_longestOf _ _ |
| 198 | + |
| 199 | +lemma longestOf_len_unique [FiniteDimensionalOrder α] (p : LTSeries α) |
| 200 | + (is_longest : ∀ (q : LTSeries α), q.length ≤ p.length) : |
| 201 | + p.length = (LTSeries.longestOf α).length := |
| 202 | + le_antisymm (longestOf_is_longest _) (is_longest _) |
| 203 | + |
| 204 | + |
| 205 | +lemma strictMono (x : LTSeries α) : StrictMono x := |
| 206 | + fun _ _ h => x.rel_of_lt h |
| 207 | + |
| 208 | +lemma monotone (x : LTSeries α) : Monotone x := |
| 209 | + x.strictMono.monotone |
| 210 | + |
| 211 | +end LTSeries |
| 212 | + |
| 213 | +end LTSeries |
0 commit comments