feat(LinearAlgebra/Basis): flag defined by a basis (#6269)

Also add supporting lemmas and golf some proofs.

Based on a file from the Sphere Eversion Project.

Author: urkud

Mathlib.lean

@@ -1358,6 +1358,7 @@ import Mathlib.Data.Erased
 import Mathlib.Data.FP.Basic
 import Mathlib.Data.Fin.Basic
 import Mathlib.Data.Fin.Fin2
+import Mathlib.Data.Fin.FlagRange
 import Mathlib.Data.Fin.Interval
 import Mathlib.Data.Fin.SuccPred
 import Mathlib.Data.Fin.Tuple.Basic
@@ -2152,6 +2153,7 @@ import Mathlib.LinearAlgebra.AnnihilatingPolynomial
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.LinearAlgebra.Basis
 import Mathlib.LinearAlgebra.Basis.Bilinear
+import Mathlib.LinearAlgebra.Basis.Flag
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.LinearAlgebra.BilinearForm
 import Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Mathlib/Data/Fin/FlagRange.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Order.Cover
+import Mathlib.Order.Chain
+import Mathlib.Data.Fin.Basic
+
+/-!
+# Range of `f : Fin (n + 1) → α` as a `Flag`
+
+Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
+- `f₀ = ⊥` and `fₙ = ⊤`;
+- `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
+  this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.
+Then the range of `f` is a maximal chain.
+
+We formulate this result in terms of `IsMaxChain` and `Flag`.
+-/
+
+open Set
+
+variable {α : Type _} [PartialOrder α] [BoundedOrder α] {n : ℕ} {f : Fin (n + 1) → α}
+
+/-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
+- `f₀ = ⊥` and `fₙ = ⊤`;
+- `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
+  this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.
+Then the range of `f` is a maximal chain. -/
+theorem IsMaxChain.range_fin_of_covby (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤)
+    (hcovby : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) :
+    IsMaxChain (· ≤ ·) (range f) := by
+  have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovby k).1
+  refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
+  rw [mem_range]; by_contra' h
+  suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
+  intro k
+  induction k using Fin.induction with
+  | zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
+  | succ k ihk =>
+    rw [range_subset_iff] at hbt
+    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovby k).2 ihk)
+
+/-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
+- `f₀ = ⊥` and `fₙ = ⊤`;
+- `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
+  this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.
+Then the range of `f` is a `Flag α`. -/
+@[simps]
+def Flag.rangeFin (f : Fin (n + 1) → α) (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤)
+    (hcovby : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) : Flag α where
+  carrier := range f
+  Chain' := (IsMaxChain.range_fin_of_covby h0 hlast hcovby).1
+  max_chain' := (IsMaxChain.range_fin_of_covby h0 hlast hcovby).2
+
+@[simp] theorem Flag.mem_rangeFin {x h0 hlast hcovby} :
+    x ∈ rangeFin f h0 hlast hcovby ↔ ∃ k, f k = x :=
+  Iff.rfl

Mathlib/LinearAlgebra/Basis/Flag.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Patrick Massot
+-/
+import Mathlib.LinearAlgebra.Basis
+import Mathlib.Data.Fin.FlagRange
+
+/-!
+# Flag of submodules defined by a basis
+
+In this file we define `Basis.flag b k`, where `b : Basis (Fin n) R M`, `k : Fin (n + 1)`,
+to be the subspace spanned by the first `k` vectors of the basis `b`.
+
+We also prove some lemmas about this definition.
+-/
+
+open Set Submodule
+
+namespace Basis
+
+section Semiring
+
+variable {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ}
+
+/-- The subspace spanned by the first `k` vectors of the basis `b`. -/
+def flag (b : Basis (Fin n) R M) (k : Fin (n + 1)) : Submodule R M :=
+  .span R <| b '' {i | i.castSucc < k}
+
+@[simp]
+theorem flag_zero (b : Basis (Fin n) R M) : b.flag 0 = ⊥ := by simp [flag]
+
+@[simp]
+theorem flag_last (b : Basis (Fin n) R M) : b.flag (.last n) = ⊤ := by
+  simp [flag, Fin.castSucc_lt_last]
+
+theorem flag_le_iff (b : Basis (Fin n) R M) {k p} :
+    b.flag k ≤ p ↔ ∀ i : Fin n, i.castSucc < k → b i ∈ p :=
+  span_le.trans ball_image_iff
+
+theorem flag_succ (b : Basis (Fin n) R M) (k : Fin n) :
+    b.flag k.succ = (R ∙ b k) ⊔ b.flag k.castSucc := by
+  simp only [flag, Fin.castSucc_lt_castSucc_iff]
+  simp [Fin.castSucc_lt_iff_succ_le, le_iff_eq_or_lt, setOf_or, image_insert_eq, span_insert]
+
+theorem self_mem_flag (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} (h : i.castSucc < k) :
+    b i ∈ b.flag k :=
+  subset_span <| mem_image_of_mem _ h
+
+@[simp]
+theorem self_mem_flag_iff [Nontrivial R] (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} :
+    b i ∈ b.flag k ↔ i.castSucc < k :=
+  b.self_mem_span_image
+
+@[mono]
+theorem flag_mono (b : Basis (Fin n) R M) : Monotone b.flag :=
+  Fin.monotone_iff_le_succ.2 fun k ↦ by rw [flag_succ]; exact le_sup_right
+
+theorem isChain_range_flag (b : Basis (Fin n) R M) : IsChain (· ≤ ·) (range b.flag) :=
+  b.flag_mono.isChain_range
+
+@[mono]
+theorem flag_strictMono [Nontrivial R] (b : Basis (Fin n) R M) : StrictMono b.flag :=
+  Fin.strictMono_iff_lt_succ.2 fun _ ↦ by simp [flag_succ]
+
+end Semiring
+
+section CommRing
+
+variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ}
+
+@[simp]
+theorem flag_le_ker_coord_iff [Nontrivial R] (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} :
+    b.flag k ≤ LinearMap.ker (b.coord l) ↔ k ≤ l.castSucc := by
+  simp [flag_le_iff, Finsupp.single_apply_eq_zero, imp_false, imp_not_comm]
+
+theorem flag_le_ker_coord (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n}
+    (h : k ≤ l.castSucc) : b.flag k ≤ LinearMap.ker (b.coord l) := by
+  nontriviality R
+  exact b.flag_le_ker_coord_iff.2 h
+
+end CommRing
+
+section DivisionRing
+
+variable {K V : Type _} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ}
+
+theorem flag_covby (b : Basis (Fin n) K V) (i : Fin n) :
+    b.flag i.castSucc ⋖ b.flag i.succ := by
+  rw [flag_succ]
+  apply covby_span_singleton_sup
+  simp
+
+theorem flag_wcovby (b : Basis (Fin n) K V) (i : Fin n) :
+    b.flag i.castSucc ⩿ b.flag i.succ :=
+  (b.flag_covby i).wcovby
+
+/-- Range of `Basis.flag` as a `Flag`. -/
+@[simps!]
+def toFlag (b : Basis (Fin n) K V) : Flag (Submodule K V) :=
+  .rangeFin b.flag b.flag_zero b.flag_last b.flag_wcovby
+
+@[simp]
+theorem mem_toFlag (b : Basis (Fin n) K V) {p : Submodule K V} : p ∈ b.toFlag ↔ ∃ k, b.flag k = p :=
+  Iff.rfl
+
+theorem isMaxChain_range_flag (b : Basis (Fin n) K V) : IsMaxChain (· ≤ ·) (range b.flag) :=
+  b.toFlag.maxChain
+
+end DivisionRing

Mathlib/LinearAlgebra/Span.lean

@@ -484,20 +484,7 @@ theorem mem_span_singleton_trans {x y z : M} (hxy : x ∈ R ∙ y) (hyz : y ∈
   exact Submodule.subset_span_trans hxy hyz
 #align submodule.mem_span_singleton_trans Submodule.mem_span_singleton_trans
 
-theorem mem_span_insert {y} :
-    x ∈ span R (insert y s) ↔ ∃ a : R, ∃ z ∈ span R s, x = a • y + z := by
-  simp only [← union_singleton, span_union, mem_sup, mem_span_singleton, exists_prop,
-    exists_exists_eq_and]
-  rw [exists_comm]
-  simp only [eq_comm, add_comm, exists_and_left]
-#align submodule.mem_span_insert Submodule.mem_span_insert
-
-theorem mem_span_pair {x y z : M} :
-    z ∈ span R ({x, y} : Set M) ↔ ∃ a b : R, a • x + b • y = z := by
-  simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
-#align submodule.mem_span_pair Submodule.mem_span_pair
-
-theorem span_insert (x) (s : Set M) : span R (insert x s) = span R ({x} : Set M) ⊔ span R s := by
+theorem span_insert (x) (s : Set M) : span R (insert x s) = (R ∙ x) ⊔ span R s := by
   rw [insert_eq, span_union]
 #align submodule.span_insert Submodule.span_insert
 
@@ -509,6 +496,16 @@ theorem span_span : span R (span R s : Set M) = span R s :=
   span_eq _
 #align submodule.span_span Submodule.span_span
 
+theorem mem_span_insert {y} :
+    x ∈ span R (insert y s) ↔ ∃ a : R, ∃ z ∈ span R s, x = a • y + z := by
+  simp [span_insert, mem_sup, mem_span_singleton, eq_comm (a := x)]
+#align submodule.mem_span_insert Submodule.mem_span_insert
+
+theorem mem_span_pair {x y z : M} :
+    z ∈ span R ({x, y} : Set M) ↔ ∃ a b : R, a • x + b • y = z := by
+  simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
+#align submodule.mem_span_pair Submodule.mem_span_pair
+
 variable (R S s)
 
 /-- If `R` is "smaller" ring than `S` then the span by `R` is smaller than the span by `S`. -/
@@ -548,37 +545,25 @@ theorem span_singleton_eq_bot : (R ∙ x) = ⊥ ↔ x = 0 :=
 theorem span_zero : span R (0 : Set M) = ⊥ := by rw [← singleton_zero, span_singleton_eq_bot]
 #align submodule.span_zero Submodule.span_zero
 
+@[simp]
+theorem span_singleton_le_iff_mem (m : M) (p : Submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p := by
+  rw [span_le, singleton_subset_iff, SetLike.mem_coe]
+#align submodule.span_singleton_le_iff_mem Submodule.span_singleton_le_iff_mem
+
 theorem span_singleton_eq_span_singleton {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
     [NoZeroSMulDivisors R M] {x y : M} : ((R ∙ x) = R ∙ y) ↔ ∃ z : Rˣ, z • x = y := by
-  by_cases hx : x = 0
-  · rw [hx, span_zero_singleton, eq_comm, span_singleton_eq_bot]
-    exact ⟨fun hy => ⟨1, by rw [hy, smul_zero]⟩, fun ⟨_, hz⟩ => by rw [← hz, smul_zero]⟩
-  by_cases hy : y = 0
-  · rw [hy, span_zero_singleton, span_singleton_eq_bot]
-    exact ⟨fun hx => ⟨1, by rw [hx, smul_zero]⟩, fun ⟨z, hz⟩ => (smul_eq_zero_iff_eq z).mp hz⟩
   constructor
-  · intro hxy
-    cases'
-      mem_span_singleton.mp
-        (by
-          rw [hxy]
-          apply mem_span_singleton_self) with
-      v hv
-    cases'
-      mem_span_singleton.mp
-        (by
-          rw [← hxy]
-          apply mem_span_singleton_self) with
-      i hi
-    have vi : v * i = 1 := by
-      rw [← one_smul R y, ← hi, smul_smul] at hv
-      exact smul_left_injective R hy hv
-    have iv : i * v = 1 := by
-      rw [← one_smul R x, ← hv, smul_smul] at hi
-      exact smul_left_injective R hx hi
-    exact ⟨⟨v, i, vi, iv⟩, hv⟩
-  · rintro ⟨v, rfl⟩
-    rw [span_singleton_group_smul_eq]
+  · simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
+    rintro ⟨⟨a, rfl⟩, b, hb⟩
+    rcases eq_or_ne y 0 with rfl | hy; · simp
+    refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
+    · apply smul_left_injective R hy
+      simpa only [mul_smul, one_smul]
+    · rw [← hb] at hy
+      apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
+      simp only [mul_smul, one_smul, hb]
+  · rintro ⟨u, rfl⟩
+    exact (span_singleton_group_smul_eq _ _ _).symm
 #align submodule.span_singleton_eq_span_singleton Submodule.span_singleton_eq_span_singleton
 
 @[simp]
@@ -664,11 +649,6 @@ theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {C : ∀ x, (x 
     refine' ⟨_, hadd _ _ _ _ Cx Cy⟩
 #align submodule.supr_induction' Submodule.iSup_induction'
 
-@[simp]
-theorem span_singleton_le_iff_mem (m : M) (p : Submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p := by
-  rw [span_le, singleton_subset_iff, SetLike.mem_coe]
-#align submodule.span_singleton_le_iff_mem Submodule.span_singleton_le_iff_mem
-
 theorem singleton_span_isCompactElement (x : M) :
     CompleteLattice.IsCompactElement (span R {x} : Submodule R M) := by
   rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
@@ -717,27 +697,7 @@ theorem submodule_eq_sSup_le_nonzero_spans (p : Submodule R M) :
     rwa [span_singleton_le_iff_mem]
 #align submodule.submodule_eq_Sup_le_nonzero_spans Submodule.submodule_eq_sSup_le_nonzero_spans
 
-theorem lt_sup_iff_not_mem {I : Submodule R M} {a : M} : (I < I ⊔ R ∙ a) ↔ a ∉ I := by
-  constructor
-  · intro h
-    by_contra akey
-    have h1 : (I ⊔ R ∙ a) ≤ I := by
-      simp only [sup_le_iff]
-      constructor
-      · exact le_refl I
-      · exact (span_singleton_le_iff_mem a I).mpr akey
-    have h2 := gt_of_ge_of_gt h1 h
-    exact lt_irrefl I h2
-  · intro h
-    apply SetLike.lt_iff_le_and_exists.mpr
-    constructor
-    simp only [le_sup_left]
-    use a
-    constructor
-    swap
-    · assumption
-    · have : (R ∙ a) ≤ I ⊔ R ∙ a := le_sup_right
-      exact this (mem_span_singleton_self a)
+theorem lt_sup_iff_not_mem {I : Submodule R M} {a : M} : (I < I ⊔ R ∙ a) ↔ a ∉ I := by simp
 #align submodule.lt_sup_iff_not_mem Submodule.lt_sup_iff_not_mem
 
 theorem mem_iSup {ι : Sort*} (p : ι → Submodule R M) {m : M} :
@@ -881,6 +841,28 @@ theorem comap_map_eq_self {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p
 
 end AddCommGroup
 
+section DivisionRing
+
+variable [DivisionRing K] [AddCommGroup V] [Module K V]
+
+/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `Wcovby` version. -/
+theorem wcovby_span_singleton_sup (x : V) (p : Submodule K V) : Wcovby p ((K ∙ x) ⊔ p) := by
+  refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_le ?_⟩
+  rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩
+  obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ p, c • x + z = y := by
+    simpa [mem_sup, mem_span_singleton] using hqp.le hyq
+  rcases eq_or_ne c 0 with rfl | hc
+  · simp [hz] at hyp
+  · have : x ∈ q
+    · rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq
+    simp [hpq.le, this]
+
+/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `Covby` version. -/
+theorem covby_span_singleton_sup {x : V} {p : Submodule K V} (h : x ∉ p) : Covby p ((K ∙ x) ⊔ p) :=
+  ⟨by simpa, (wcovby_span_singleton_sup _ _).2⟩
+
+end DivisionRing
+
 end Submodule
 
 namespace LinearMap
@@ -1010,13 +992,10 @@ variable [Field K] [AddCommGroup V] [Module K V]
 
 theorem span_singleton_sup_ker_eq_top (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) :
     (K ∙ x) ⊔ ker f = ⊤ :=
-  eq_top_iff.2 fun y _ =>
+  top_unique fun y _ =>
     Submodule.mem_sup.2
       ⟨(f y * (f x)⁻¹) • x, Submodule.mem_span_singleton.2 ⟨f y * (f x)⁻¹, rfl⟩,
-        ⟨y - (f y * (f x)⁻¹) • x, by
-          rw [LinearMap.mem_ker, f.map_sub, f.map_smul, smul_eq_mul, mul_assoc, inv_mul_cancel hx,
-            mul_one, sub_self],
-          by simp only [add_sub_cancel'_right]⟩⟩
+        ⟨y - (f y * (f x)⁻¹) • x, by simp [hx]⟩⟩
 #align linear_map.span_singleton_sup_ker_eq_top LinearMap.span_singleton_sup_ker_eq_top
 
 end Field