From c74008f351231736d78017bebef9b835bf89d554 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Tue, 8 Sep 2026 16:09:46 +0200 Subject: [PATCH 1/3] feat(AffineSpace): `toAffineSubspace` lemmas --- .../AffineSpace/AffineSubspace/Defs.lean | 20 +++++++++++++++---- .../LinearAlgebra/AffineSpace/Dimension.lean | 9 +++++++++ 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean index 80ba951c1264c2..e88e1ba17381c5 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean @@ -220,6 +220,10 @@ variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V] instance : Coe (Submodule k V) (AffineSubspace k V) := ⟨toAffineSubspace⟩ +@[simp] +theorem coe_toAffineSubspace (p : Submodule k V) : (p.toAffineSubspace : Set V) = (p : Set V) := + rfl + @[simp] theorem mem_toAffineSubspace {p : Submodule k V} {x : V} : x ∈ (p : AffineSubspace k V) ↔ x ∈ p := Iff.rfl @@ -793,6 +797,10 @@ theorem eq_bot_or_nonempty (Q : AffineSubspace k P) : Q = ⊥ ∨ (Q : Set P).No rw [nonempty_iff_ne_bot] apply eq_or_ne +@[simp] +theorem toAffineSubspace_ne_bot (p : Submodule k V) : p.toAffineSubspace ≠ ⊥ := + (AffineSubspace.nonempty_iff_ne_bot _).mp ⟨0, p.zero_mem⟩ + instance [Subsingleton P] : IsSimpleOrder (AffineSubspace k P) where eq_bot_or_eq_top (s : AffineSubspace k P) := by rw [← coe_eq_bot_iff, ← coe_eq_univ_iff] @@ -1149,15 +1157,19 @@ lemma affineSpan_subset_span {s : Set V} : (affineSpan k s : Set V) ⊆ Submodule.span k s := affineSpan_le_toAffineSubspace_span --- TODO: We want this to be simp, but `affineSpan` gets simp-ed away to `spanPoints`! --- Let's delete `spanPoints` +@[simp] lemma affineSpan_insert_zero (s : Set V) : - (affineSpan k (insert 0 s) : Set V) = Submodule.span k s := by - rw [← Submodule.span_insert_zero] + affineSpan k (insert 0 s) = Submodule.span k s := by + rw [AffineSubspace.ext_iff, ← Submodule.span_insert_zero] refine affineSpan_subset_span.antisymm ?_ rw [← vectorSpan_add_self, vectorSpan_def] refine Subset.trans ?_ <| subset_add_left _ <| mem_insert .. gcongr exact subset_sub_left <| mem_insert .. +theorem affineSpan_eq_span_iff_zero_mem {s : Set V} : + affineSpan k s = (Submodule.span k s).toAffineSubspace ↔ 0 ∈ affineSpan k s := by + refine ⟨by simp +contextual, fun h ↦ ?_⟩ + rw [← affineSpan_insert_eq_affineSpan _ h, affineSpan_insert_zero] + end AffineSpace' diff --git a/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean b/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean index d97aa2403c7a6c..d0829089ec9ab2 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean @@ -92,6 +92,15 @@ theorem finDim_eq_finrank (h : s ≠ ⊥) : finDim s = Module.finrank R s.direct simp [finDim, dim_eq_rank h] norm_cast +@[simp] +theorem dim_toAffineSubspace (s : Submodule R V) : s.toAffineSubspace.dim = Module.rank R s := by + rw [dim_eq_rank (toAffineSubspace_ne_bot _), Submodule.toAffineSubspace_direction] + +@[simp] +theorem finDim_toAffineSubspace (s : Submodule R V) : + s.toAffineSubspace.finDim = Module.finrank R s := by + rw [finDim_eq_finrank (toAffineSubspace_ne_bot _), Submodule.toAffineSubspace_direction] + @[simp] theorem finDim_eq_finrank_of_not_finite [Module.Free R s.direction] [StrongRankCondition R] (h : ¬Module.Finite R s.direction) : finDim s = 0 := by From d540bb39cbb83344120fef1ec07993a9b9e86d5c Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Tue, 8 Sep 2026 16:13:53 +0200 Subject: [PATCH 2/3] clearer --- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean index e88e1ba17381c5..0bf9f90eaa60a3 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean @@ -1168,7 +1168,7 @@ lemma affineSpan_insert_zero (s : Set V) : exact subset_sub_left <| mem_insert .. theorem affineSpan_eq_span_iff_zero_mem {s : Set V} : - affineSpan k s = (Submodule.span k s).toAffineSubspace ↔ 0 ∈ affineSpan k s := by + affineSpan k s = Submodule.span k s ↔ 0 ∈ affineSpan k s := by refine ⟨by simp +contextual, fun h ↦ ?_⟩ rw [← affineSpan_insert_eq_affineSpan _ h, affineSpan_insert_zero] From d218829e523d8433ecec47c500b25cde98b08cac Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Tue, 8 Sep 2026 21:06:35 +0200 Subject: [PATCH 3/3] add back TODO --- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean index 0bf9f90eaa60a3..9ad3473db37e7e 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean @@ -44,6 +44,10 @@ topology are defined elsewhere; see `Analysis.Normed.Affine.AddTorsor` and * https://en.wikipedia.org/wiki/Affine_space * https://en.wikipedia.org/wiki/Principal_homogeneous_space + +## TODO + +* Delete `spanPoints` -/ @[expose] public section