From d747656848508888859be80d60b95cff8c9b9984 Mon Sep 17 00:00:00 2001 From: Martin Winter Date: Thu, 1 Oct 2026 20:57:52 +0200 Subject: [PATCH 1/6] Add `FiniteDimensional` for affine subspaces --- Polyhedral.lean | 1 + .../AffineSubspace/FiniteDimensional.lean | 222 ++++++++++++++++++ 2 files changed, 223 insertions(+) create mode 100644 Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean diff --git a/Polyhedral.lean b/Polyhedral.lean index 53d06d22..e71743fa 100644 --- a/Polyhedral.lean +++ b/Polyhedral.lean @@ -70,6 +70,7 @@ public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.No public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineMap public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean new file mode 100644 index 00000000..31d6ef80 --- /dev/null +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean @@ -0,0 +1,222 @@ +/- +Copyright (c) 2026 Martin Winter. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Martin Winter +-/ +module + +public import Mathlib.LinearAlgebra.AffineSpace.Dimension +public import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional + +/-! +# Finite-dimensional affine subspaces + +`AffineSubspace.FiniteDimensional s` means that the direction of `s` is finite-dimensional. +It is an abbreviation, just as `FiniteDimensional` is an abbreviation for `Module.Finite`. +Thus `[s.FiniteDimensional]` works directly with the existing API for `s.direction`, `s.dim`, +and `s.finDim`, without conversion instances. + +The empty subspace is finite-dimensional, although its affine dimension is `⊥`. +Infinite-dimensional subspaces have the junk value `finDim = 0`; use `dim < ℵ₀` to +characterize finite-dimensionality instead. + +Mathlib already supplies instances for singletons, affine spans of finite families, binary +suprema, affine images, and adjoining a point. This file adds instances for subspaces of a +finite-dimensional ambient space, intersections, finite suprema, and affine spans of finsets. +It also provides descent along injective affine maps, finite generating sets, and dimension +criteria for equality and strict inclusion. +-/ + +@[expose] public section + +namespace AffineSubspace + +variable {K V P : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V P] + +/-- An affine subspace is finite-dimensional if its direction is finite-dimensional. +In particular, the empty affine subspace is finite-dimensional. -/ +abbrev FiniteDimensional (s : AffineSubspace K P) : Prop := + _root_.FiniteDimensional K s.direction + +variable {s t : AffineSubspace K P} + +theorem finiteDimensional_iff_direction : + s.FiniteDimensional ↔ _root_.FiniteDimensional K s.direction := Iff.rfl + +@[simp] +theorem finiteDimensional_top_iff : + (⊤ : AffineSubspace K P).FiniteDimensional ↔ _root_.FiniteDimensional K V := by + unfold FiniteDimensional + rw [direction_top] + exact ⟨fun h ↦ by + let := h + exact Submodule.topEquiv.finiteDimensional, fun h ↦ by + let := h + infer_instance⟩ + +@[simp] +theorem finiteDimensional_toAffineSubspace_iff (S : Submodule K V) : + S.toAffineSubspace.FiniteDimensional ↔ _root_.FiniteDimensional K S := by + unfold FiniteDimensional + rw [Submodule.toAffineSubspace_direction] + +instance finiteDimensional_toAffineSubspace (S : Submodule K V) + [_root_.FiniteDimensional K S] : S.toAffineSubspace.FiniteDimensional := + (finiteDimensional_toAffineSubspace_iff S).mpr inferInstance + +instance finiteDimensional_mk' (p : P) (S : Submodule K V) + [_root_.FiniteDimensional K S] : (mk' p S).FiniteDimensional := by + unfold FiniteDimensional + rw [direction_mk'] + infer_instance + +/-- Every affine subspace of a finite-dimensional ambient space is finite-dimensional. -/ +instance (priority := low) finiteDimensional_of_finiteDimensional + [_root_.FiniteDimensional K V] (s : AffineSubspace K P) : s.FiniteDimensional := + inferInstanceAs (_root_.FiniteDimensional K s.direction) + +instance finiteDimensional_bot : (⊥ : AffineSubspace K P).FiniteDimensional := by + unfold FiniteDimensional + rw [direction_bot] + infer_instance + +/-- Finite-dimensionality descends to affine subspaces. -/ +theorem finiteDimensional_of_le [t.FiniteDimensional] (h : s ≤ t) : s.FiniteDimensional := + Submodule.finiteDimensional_of_le (direction_le h) + +instance finiteDimensional_inf_left (s t : AffineSubspace K P) [s.FiniteDimensional] : + (s ⊓ t).FiniteDimensional := + finiteDimensional_of_le inf_le_left + +instance finiteDimensional_inf_right (s t : AffineSubspace K P) [t.FiniteDimensional] : + (s ⊓ t).FiniteDimensional := + finiteDimensional_of_le inf_le_right + +/-- An indexed intersection is finite-dimensional if one of its members is. -/ +theorem finiteDimensional_iInf {ι : Sort*} (S : ι → AffineSubspace K P) (i : ι) + [(S i).FiniteDimensional] : (⨅ j, S j).FiniteDimensional := + finiteDimensional_of_le (iInf_le S i) + +instance finiteDimensional_finset_sup {ι : Type*} (I : Finset ι) + (S : ι → AffineSubspace K P) [∀ i, (S i).FiniteDimensional] : + (I.sup S).FiniteDimensional := by + classical + induction I using Finset.induction_on with + | empty => simpa using (inferInstance : (⊥ : AffineSubspace K P).FiniteDimensional) + | @insert i I hi hI => + let := hI + rw [Finset.sup_insert] + infer_instance + +instance finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P) + [∀ i, (S i).FiniteDimensional] : (⨆ i, S i).FiniteDimensional := by + classical + let := Fintype.ofFinite (PLift ι) + simpa only [Finset.sup_univ_eq_iSup, iSup_plift_down] using + (inferInstance : (Finset.univ.sup (fun i : PLift ι ↦ S i.down)).FiniteDimensional) + +/-- The affine span of a finite set is finite-dimensional. -/ +theorem finiteDimensional_affineSpan_of_finite {S : Set P} (hS : S.Finite) : + (affineSpan K S).FiniteDimensional := + finiteDimensional_direction_affineSpan_of_finite K hS + +instance finiteDimensional_affineSpan_finset (S : Finset P) : + (affineSpan K (S : Set P)).FiniteDimensional := + finiteDimensional_affineSpan_of_finite S.finite_toSet + +/-- The affine span of a subset of a finite-dimensional subspace is finite-dimensional. -/ +theorem finiteDimensional_affineSpan_of_subset [s.FiniteDimensional] {S : Set P} + (hS : S ⊆ s) : (affineSpan K S).FiniteDimensional := + finiteDimensional_of_le (affineSpan_le.mpr hS) + +section Map + +variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q] + +/-- Finite-dimensionality descends along an injective affine map. -/ +theorem finiteDimensional_of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) + [(s.map f).FiniteDimensional] : s.FiniteDimensional := by + have : _root_.FiniteDimensional K (s.direction.map f.linear) := by + rw [← map_direction] + exact (inferInstance : (s.map f).FiniteDimensional) + exact (Submodule.equivMapOfInjective f.linear + (f.linear_injective_iff.mpr hf) s.direction).symm.finiteDimensional + +theorem finiteDimensional_map_iff {f : P →ᵃ[K] Q} (hf : Function.Injective f) : + (s.map f).FiniteDimensional ↔ s.FiniteDimensional := by + constructor + · intro h + let := h + exact finiteDimensional_of_map hf + · intro h + let := h + infer_instance + +/-- An injective affine preimage of a finite-dimensional subspace is finite-dimensional. -/ +theorem finiteDimensional_comap_of_injective {f : P →ᵃ[K] Q} (hf : Function.Injective f) + (t : AffineSubspace K Q) [t.FiniteDimensional] : (t.comap f).FiniteDimensional := by + have : ((t.comap f).map f).FiniteDimensional := + finiteDimensional_of_le (map_comap_le f t) + exact finiteDimensional_of_map hf + +@[simp] +theorem finiteDimensional_map_equiv_iff (e : P ≃ᵃ[K] Q) : + (s.map e.toAffineMap).FiniteDimensional ↔ s.FiniteDimensional := + finiteDimensional_map_iff e.injective + +end Map + +/-- Finite-dimensional affine subspaces are precisely the affine spans of finite sets. -/ +theorem finiteDimensional_iff_exists_finite_affineSpan : + s.FiniteDimensional ↔ ∃ S : Set P, S.Finite ∧ affineSpan K S = s := by + constructor + · intro hs + let := hs + obtain ⟨S, -, hS, hI⟩ := exists_affineIndependent K V (s : Set P) + have hspan : affineSpan K S = s := hS.trans (affineSpan_coe s) + have : (affineSpan K S).FiniteDimensional := hspan ▸ hs + have : _root_.FiniteDimensional K (vectorSpan K (Set.range ((↑) : S → P))) := by + rw [Subtype.range_coe, ← direction_affineSpan] + exact (inferInstance : (affineSpan K S).FiniteDimensional) + exact ⟨S, (finiteDimensional_iff_setFinite K hI).mp inferInstance, hspan⟩ + · rintro ⟨S, hS, rfl⟩ + exact finiteDimensional_affineSpan_of_finite hS + +theorem finiteDimensional_iff_exists_finset_affineSpan : + s.FiniteDimensional ↔ ∃ S : Finset P, affineSpan K (S : Set P) = s := by + classical + rw [finiteDimensional_iff_exists_finite_affineSpan] + exact ⟨fun ⟨S, hS, hspan⟩ ↦ ⟨hS.toFinset, by simpa using hspan⟩, + fun ⟨S, hspan⟩ ↦ ⟨S, S.finite_toSet, hspan⟩⟩ + +/-- The cardinal-valued dimension detects finite-dimensionality, including for `⊥`. -/ +theorem finiteDimensional_iff_dim_lt_aleph0 : + s.FiniteDimensional ↔ s.dim < (Cardinal.aleph0 : WithBot Cardinal) := + finite_iff_dim_lt_aleph0 s + +/-- In finite dimension, the cardinal dimension is the natural dimension cast to cardinals. +This formulation also applies to the empty subspace. -/ +theorem dim_eq_map_finDim [s.FiniteDimensional] : + s.dim = s.finDim.map (fun n : ℕ ↦ (n : Cardinal)) := by + rcases eq_or_ne s ⊥ with rfl | hs + · simp + rw [dim_eq_rank hs, finDim_eq_finrank hs, WithBot.map_natCast, WithBot.coe_inj] + exact (Module.finrank_eq_rank' (K := K) (V := s.direction)).symm + +/-- A finite-dimensional affine subspace is determined by inclusion and finite dimension. -/ +theorem eq_of_le_of_finDim_eq [t.FiniteDimensional] (h : s ≤ t) + (hd : s.finDim = t.finDim) : s = t := by + by_contra hne + exact (ne_of_lt (finDim_strictMono (lt_of_le_of_ne h hne))) hd + +theorem finDim_eq_iff_eq_of_le [t.FiniteDimensional] (h : s ≤ t) : + s.finDim = t.finDim ↔ s = t := + ⟨eq_of_le_of_finDim_eq h, fun h ↦ congrArg finDim h⟩ + +theorem lt_iff_finDim_lt_of_le [t.FiniteDimensional] (h : s ≤ t) : + s < t ↔ s.finDim < t.finDim := by + refine ⟨finDim_strictMono, fun hd ↦ lt_of_le_of_ne h ?_⟩ + intro heq + exact (ne_of_lt hd) (congrArg finDim heq) + +end AffineSubspace From 960e98f83fb72922980a5517ad1b8c2e2bc5daa2 Mon Sep 17 00:00:00 2001 From: Martin Winter Date: Thu, 1 Oct 2026 21:34:34 +0200 Subject: [PATCH 2/6] Add `AffineSpace.FiniteDimensional` --- Polyhedral.lean | 1 + .../AffineSubspace/FiniteDimensional.lean | 146 ++++++++------- .../AffineSpace/FiniteDimensional.lean | 172 ++++++++++++++++++ 3 files changed, 258 insertions(+), 61 deletions(-) create mode 100644 Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean diff --git a/Polyhedral.lean b/Polyhedral.lean index e71743fa..2b27d790 100644 --- a/Polyhedral.lean +++ b/Polyhedral.lean @@ -73,6 +73,7 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean index 31d6ef80..393afb47 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean @@ -5,26 +5,24 @@ Authors: Martin Winter -/ module -public import Mathlib.LinearAlgebra.AffineSpace.Dimension -public import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional /-! # Finite-dimensional affine subspaces `AffineSubspace.FiniteDimensional s` means that the direction of `s` is finite-dimensional. It is an abbreviation, just as `FiniteDimensional` is an abbreviation for `Module.Finite`. -Thus `[s.FiniteDimensional]` works directly with the existing API for `s.direction`, `s.dim`, -and `s.finDim`, without conversion instances. +The closure lemmas in this file take explicit proofs of this predicate and register no +additional instances. A proof can still be installed locally with `let := hs` to use +Mathlib's API for `s.direction`, `s.dim`, and `s.finDim`. The empty subspace is finite-dimensional, although its affine dimension is `⊥`. Infinite-dimensional subspaces have the junk value `finDim = 0`; use `dim < ℵ₀` to characterize finite-dimensionality instead. -Mathlib already supplies instances for singletons, affine spans of finite families, binary -suprema, affine images, and adjoining a point. This file adds instances for subspaces of a -finite-dimensional ambient space, intersections, finite suprema, and affine spans of finsets. -It also provides descent along injective affine maps, finite generating sets, and dimension -criteria for equality and strict inclusion. +Finite-dimensionality of an affine space is expressed separately by +`AffineSpace.FiniteDimensional K P`. For a nonempty subspace `s`, the two notions agree when +`s` is viewed as an affine space modeled on `s.direction`. -/ @[expose] public section @@ -43,6 +41,19 @@ variable {s t : AffineSubspace K P} theorem finiteDimensional_iff_direction : s.FiniteDimensional ↔ _root_.FiniteDimensional K s.direction := Iff.rfl +/-- A nonempty affine subspace has the same finite-dimensionality as its underlying affine +space. This comparison is a theorem, not an instance. -/ +theorem finiteDimensional_iff_affineSpace (s : AffineSubspace K P) [Nonempty s] : + s.FiniteDimensional ↔ AffineSpace.FiniteDimensional K s := Iff.rfl + +theorem dim_eq_affine_dim (s : AffineSubspace K P) [Nonempty s] : + s.dim = (AffineSpace.dim K s : WithBot Cardinal) := + dim_eq_rank (nonempty_iff_ne_bot s |>.mp (Set.nonempty_coe_sort.mp inferInstance)) + +theorem finDim_eq_affine_finDim (s : AffineSubspace K P) [Nonempty s] : + s.finDim = (AffineSpace.finDim K s : WithBot ℕ) := + finDim_eq_finrank (nonempty_iff_ne_bot s |>.mp (Set.nonempty_coe_sort.mp inferInstance)) + @[simp] theorem finiteDimensional_top_iff : (⊤ : AffineSubspace K P).FiniteDimensional ↔ _root_.FiniteDimensional K V := by @@ -60,104 +71,114 @@ theorem finiteDimensional_toAffineSubspace_iff (S : Submodule K V) : unfold FiniteDimensional rw [Submodule.toAffineSubspace_direction] -instance finiteDimensional_toAffineSubspace (S : Submodule K V) - [_root_.FiniteDimensional K S] : S.toAffineSubspace.FiniteDimensional := - (finiteDimensional_toAffineSubspace_iff S).mpr inferInstance +theorem finiteDimensional_toAffineSubspace (S : Submodule K V) + (hS : _root_.FiniteDimensional K S) : S.toAffineSubspace.FiniteDimensional := + (finiteDimensional_toAffineSubspace_iff S).mpr hS -instance finiteDimensional_mk' (p : P) (S : Submodule K V) - [_root_.FiniteDimensional K S] : (mk' p S).FiniteDimensional := by +theorem finiteDimensional_mk' (p : P) (S : Submodule K V) + (hS : _root_.FiniteDimensional K S) : (mk' p S).FiniteDimensional := by unfold FiniteDimensional rw [direction_mk'] - infer_instance + exact hS /-- Every affine subspace of a finite-dimensional ambient space is finite-dimensional. -/ -instance (priority := low) finiteDimensional_of_finiteDimensional - [_root_.FiniteDimensional K V] (s : AffineSubspace K P) : s.FiniteDimensional := +theorem finiteDimensional_of_finiteDimensional + [AffineSpace.FiniteDimensional K P] (s : AffineSubspace K P) : s.FiniteDimensional := inferInstanceAs (_root_.FiniteDimensional K s.direction) -instance finiteDimensional_bot : (⊥ : AffineSubspace K P).FiniteDimensional := by +theorem finiteDimensional_bot : (⊥ : AffineSubspace K P).FiniteDimensional := by unfold FiniteDimensional rw [direction_bot] infer_instance /-- Finite-dimensionality descends to affine subspaces. -/ -theorem finiteDimensional_of_le [t.FiniteDimensional] (h : s ≤ t) : s.FiniteDimensional := - Submodule.finiteDimensional_of_le (direction_le h) +theorem finiteDimensional_of_le (ht : t.FiniteDimensional) (h : s ≤ t) : + s.FiniteDimensional := by + let := ht + exact Submodule.finiteDimensional_of_le (direction_le h) -instance finiteDimensional_inf_left (s t : AffineSubspace K P) [s.FiniteDimensional] : +theorem finiteDimensional_inf_left (s t : AffineSubspace K P) (hs : s.FiniteDimensional) : (s ⊓ t).FiniteDimensional := - finiteDimensional_of_le inf_le_left + finiteDimensional_of_le hs inf_le_left -instance finiteDimensional_inf_right (s t : AffineSubspace K P) [t.FiniteDimensional] : +theorem finiteDimensional_inf_right (s t : AffineSubspace K P) (ht : t.FiniteDimensional) : (s ⊓ t).FiniteDimensional := - finiteDimensional_of_le inf_le_right + finiteDimensional_of_le ht inf_le_right /-- An indexed intersection is finite-dimensional if one of its members is. -/ theorem finiteDimensional_iInf {ι : Sort*} (S : ι → AffineSubspace K P) (i : ι) - [(S i).FiniteDimensional] : (⨅ j, S j).FiniteDimensional := - finiteDimensional_of_le (iInf_le S i) + (hi : (S i).FiniteDimensional) : (⨅ j, S j).FiniteDimensional := + finiteDimensional_of_le hi (iInf_le S i) -instance finiteDimensional_finset_sup {ι : Type*} (I : Finset ι) - (S : ι → AffineSubspace K P) [∀ i, (S i).FiniteDimensional] : +theorem finiteDimensional_finset_sup {ι : Type*} (I : Finset ι) + (S : ι → AffineSubspace K P) (hS : ∀ i ∈ I, (S i).FiniteDimensional) : (I.sup S).FiniteDimensional := by - classical - induction I using Finset.induction_on with - | empty => simpa using (inferInstance : (⊥ : AffineSubspace K P).FiniteDimensional) - | @insert i I hi hI => - let := hI - rw [Finset.sup_insert] - infer_instance - -instance finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P) - [∀ i, (S i).FiniteDimensional] : (⨆ i, S i).FiniteDimensional := by + refine Finset.sup_induction finiteDimensional_bot ?_ hS + intro s hs t ht + let := hs + let := ht + infer_instance + +theorem finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P) + (hS : ∀ i, (S i).FiniteDimensional) : (⨆ i, S i).FiniteDimensional := by classical let := Fintype.ofFinite (PLift ι) simpa only [Finset.sup_univ_eq_iSup, iSup_plift_down] using - (inferInstance : (Finset.univ.sup (fun i : PLift ι ↦ S i.down)).FiniteDimensional) + finiteDimensional_finset_sup Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down) + +/-- A singleton is finite-dimensional, even in an infinite-dimensional ambient space. -/ +theorem finiteDimensional_singleton (p : P) : ({p} : AffineSubspace K P).FiniteDimensional := + inferInstance + +/-- Binary joins preserve finite-dimensionality. -/ +theorem finiteDimensional_sup_of_finiteDimensional (hs : s.FiniteDimensional) + (ht : t.FiniteDimensional) : (s ⊔ t).FiniteDimensional := by + let := hs + let := ht + infer_instance /-- The affine span of a finite set is finite-dimensional. -/ theorem finiteDimensional_affineSpan_of_finite {S : Set P} (hS : S.Finite) : (affineSpan K S).FiniteDimensional := finiteDimensional_direction_affineSpan_of_finite K hS -instance finiteDimensional_affineSpan_finset (S : Finset P) : +theorem finiteDimensional_affineSpan_finset (S : Finset P) : (affineSpan K (S : Set P)).FiniteDimensional := finiteDimensional_affineSpan_of_finite S.finite_toSet /-- The affine span of a subset of a finite-dimensional subspace is finite-dimensional. -/ -theorem finiteDimensional_affineSpan_of_subset [s.FiniteDimensional] {S : Set P} +theorem finiteDimensional_affineSpan_of_subset (hs : s.FiniteDimensional) {S : Set P} (hS : S ⊆ s) : (affineSpan K S).FiniteDimensional := - finiteDimensional_of_le (affineSpan_le.mpr hS) + finiteDimensional_of_le hs (affineSpan_le.mpr hS) section Map variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q] +theorem finiteDimensional_map (hs : s.FiniteDimensional) (f : P →ᵃ[K] Q) : + (s.map f).FiniteDimensional := by + let := hs + infer_instance + /-- Finite-dimensionality descends along an injective affine map. -/ theorem finiteDimensional_of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) - [(s.map f).FiniteDimensional] : s.FiniteDimensional := by + (hs : (s.map f).FiniteDimensional) : s.FiniteDimensional := by have : _root_.FiniteDimensional K (s.direction.map f.linear) := by rw [← map_direction] - exact (inferInstance : (s.map f).FiniteDimensional) + exact hs exact (Submodule.equivMapOfInjective f.linear (f.linear_injective_iff.mpr hf) s.direction).symm.finiteDimensional theorem finiteDimensional_map_iff {f : P →ᵃ[K] Q} (hf : Function.Injective f) : (s.map f).FiniteDimensional ↔ s.FiniteDimensional := by constructor - · intro h - let := h - exact finiteDimensional_of_map hf - · intro h - let := h - infer_instance + · exact finiteDimensional_of_map hf + · exact fun h ↦ finiteDimensional_map h f /-- An injective affine preimage of a finite-dimensional subspace is finite-dimensional. -/ theorem finiteDimensional_comap_of_injective {f : P →ᵃ[K] Q} (hf : Function.Injective f) - (t : AffineSubspace K Q) [t.FiniteDimensional] : (t.comap f).FiniteDimensional := by - have : ((t.comap f).map f).FiniteDimensional := - finiteDimensional_of_le (map_comap_le f t) - exact finiteDimensional_of_map hf + (t : AffineSubspace K Q) (ht : t.FiniteDimensional) : (t.comap f).FiniteDimensional := + finiteDimensional_of_map hf (finiteDimensional_of_le ht (map_comap_le f t)) @[simp] theorem finiteDimensional_map_equiv_iff (e : P ≃ᵃ[K] Q) : @@ -196,25 +217,28 @@ theorem finiteDimensional_iff_dim_lt_aleph0 : /-- In finite dimension, the cardinal dimension is the natural dimension cast to cardinals. This formulation also applies to the empty subspace. -/ -theorem dim_eq_map_finDim [s.FiniteDimensional] : +theorem dim_eq_map_finDim (hs : s.FiniteDimensional) : s.dim = s.finDim.map (fun n : ℕ ↦ (n : Cardinal)) := by - rcases eq_or_ne s ⊥ with rfl | hs + let := hs + rcases eq_or_ne s ⊥ with rfl | hbot · simp - rw [dim_eq_rank hs, finDim_eq_finrank hs, WithBot.map_natCast, WithBot.coe_inj] + rw [dim_eq_rank hbot, finDim_eq_finrank hbot, WithBot.map_natCast, WithBot.coe_inj] exact (Module.finrank_eq_rank' (K := K) (V := s.direction)).symm /-- A finite-dimensional affine subspace is determined by inclusion and finite dimension. -/ -theorem eq_of_le_of_finDim_eq [t.FiniteDimensional] (h : s ≤ t) +theorem eq_of_le_of_finDim_eq (ht : t.FiniteDimensional) (h : s ≤ t) (hd : s.finDim = t.finDim) : s = t := by + let := ht by_contra hne exact (ne_of_lt (finDim_strictMono (lt_of_le_of_ne h hne))) hd -theorem finDim_eq_iff_eq_of_le [t.FiniteDimensional] (h : s ≤ t) : +theorem finDim_eq_iff_eq_of_le (ht : t.FiniteDimensional) (h : s ≤ t) : s.finDim = t.finDim ↔ s = t := - ⟨eq_of_le_of_finDim_eq h, fun h ↦ congrArg finDim h⟩ + ⟨eq_of_le_of_finDim_eq ht h, fun h ↦ congrArg finDim h⟩ -theorem lt_iff_finDim_lt_of_le [t.FiniteDimensional] (h : s ≤ t) : +theorem lt_iff_finDim_lt_of_le (ht : t.FiniteDimensional) (h : s ≤ t) : s < t ↔ s.finDim < t.finDim := by + let := ht refine ⟨finDim_strictMono, fun hd ↦ lt_of_le_of_ne h ?_⟩ intro heq exact (ne_of_lt hd) (congrArg finDim heq) diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean new file mode 100644 index 00000000..04cd4ffa --- /dev/null +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2026 Martin Winter. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Martin Winter +-/ +module + +public import Mathlib.LinearAlgebra.AffineSpace.Dimension +public import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional +public import Mathlib.Data.Fintype.Card + +/-! +# Finite-dimensional affine spaces + +`AffineSpace.FiniteDimensional K P` expresses finite-dimensionality of an affine space `P` +over `K`. Its model vector space `V` is inferred from `[AddTorsor V P]`. +The definition abbreviates `FiniteDimensional K V`, so the two typeclass assumptions +are interchangeable and all of Mathlib's instances on model vector spaces apply directly. +In particular, vector spaces, products, and nonempty affine subspaces inherit finite dimension. +No conversion instances are needed in either direction. + +`AffineSpace.dim K P` and `AffineSpace.finDim K P` are the dimensions of the model vector space. +An affine space is nonempty, so these do not need the bottom value used by +`AffineSubspace.dim` and `AffineSubspace.finDim`. As with `Module.finrank`, `finDim` has +the junk value zero in infinite dimension. + +The predicate on affine subspaces is kept separately in +`AffineSpace/AffineSubspace/FiniteDimensional.lean`; that file provides explicit closure +lemmas and a comparison for a nonempty subspace viewed as an affine space. +-/ + +@[expose] public section + +namespace AffineSpace + +/-- An affine space is finite-dimensional when its model vector space is finite-dimensional. -/ +abbrev FiniteDimensional (K P : Type*) {V : Type*} [DivisionRing K] [AddCommGroup V] + [Module K V] [AddTorsor V P] : Prop := + _root_.FiniteDimensional K V + +/-- The cardinal dimension of an affine space is the rank of its model vector space. -/ +noncomputable def dim (K P : Type*) {V : Type*} [DivisionRing K] [AddCommGroup V] + [Module K V] [AddTorsor V P] : Cardinal := + Module.rank K V + +/-- The finite dimension of an affine space, with the junk value zero in infinite dimension. -/ +noncomputable def finDim (K P : Type*) {V : Type*} [DivisionRing K] [AddCommGroup V] + [Module K V] [AddTorsor V P] : ℕ := + Module.finrank K V + +variable {K V P : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V P] + +theorem finiteDimensional_iff_model : + FiniteDimensional K P ↔ _root_.FiniteDimensional K V := Iff.rfl + +theorem dim_eq_rank : dim K P = Module.rank K V := rfl + +theorem finDim_eq_finrank : finDim K P = Module.finrank K V := rfl + +@[simp] +theorem dim_eq_zero_iff : dim K P = 0 ↔ Subsingleton P := + (rank_zero_iff (R := K) (M := V)).trans (AddTorsor.subsingleton_iff V P) + +@[simp] +theorem dim_top : (⊤ : AffineSubspace K P).dim = (dim K P : WithBot Cardinal) := + by rw [AffineSubspace.dim_eq_rank (by simp), AffineSubspace.direction_top, + _root_.rank_top]; rfl + +@[simp] +theorem finDim_top : (⊤ : AffineSubspace K P).finDim = (finDim K P : WithBot ℕ) := by + rw [AffineSubspace.finDim_eq_finrank (by simp), AffineSubspace.direction_top, + _root_.finrank_top] + rfl + +theorem finiteDimensional_iff_dim_lt_aleph0 : + FiniteDimensional K P ↔ dim K P < Cardinal.aleph0 := + Module.rank_lt_aleph0_iff.symm + +theorem finDim_eq_zero_of_not_finiteDimensional (h : ¬FiniteDimensional K P) : + finDim K P = 0 := + Module.finrank_of_not_finite h + +namespace FiniteDimensional + +variable [FiniteDimensional K P] + +theorem dim_lt_aleph0 : dim K P < Cardinal.aleph0 := Module.rank_lt_aleph0 K V + +theorem finDim_eq_dim : (finDim K P : Cardinal) = dim K P := + Module.finrank_eq_rank' K V + +@[simp] +theorem finDim_eq_zero_iff : finDim K P = 0 ↔ Subsingleton P := + (Module.finrank_zero_iff (R := K) (M := V)).trans (AddTorsor.subsingleton_iff V P) + +/-- A finite-dimensional affine space admits a finite affine basis. -/ +theorem exists_affineBasis : Nonempty (AffineBasis (Fin (finDim K P + 1)) K P) := + AffineBasis.exists_affineBasis_of_finiteDimensional (Fintype.card_fin _) + +/-- A finite-dimensional affine space is generated by finitely many points. -/ +theorem exists_finset_affineSpan : ∃ S : Finset P, affineSpan K (S : Set P) = ⊤ := by + classical + obtain ⟨b⟩ := exists_affineBasis (K := K) (P := P) + exact ⟨Finset.univ.image b, by simpa only [Finset.coe_image, Finset.coe_univ, + Set.image_univ] using b.tot⟩ + +section Map + +variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q] + +omit [FiniteDimensional K P] in +/-- An affine space injecting into a finite-dimensional affine space is finite-dimensional. -/ +theorem of_injective [FiniteDimensional K Q] (f : P →ᵃ[K] Q) + (hf : Function.Injective f) : FiniteDimensional K P := + _root_.FiniteDimensional.of_injective f.linear (f.linear_injective_iff.mpr hf) + +/-- A surjective affine image of a finite-dimensional affine space is finite-dimensional. -/ +theorem of_surjective (f : P →ᵃ[K] Q) (hf : Function.Surjective f) : + FiniteDimensional K Q := + _root_.FiniteDimensional.of_surjective f.linear (f.linear_surjective_iff.mpr hf) + +/-- Finite-dimensionality is preserved by an affine equivalence. -/ +theorem of_equiv (e : P ≃ᵃ[K] Q) : FiniteDimensional K Q := + e.linear.finiteDimensional + +omit [FiniteDimensional K P] in +theorem finDim_le_of_injective [FiniteDimensional K Q] (f : P →ᵃ[K] Q) + (hf : Function.Injective f) : finDim K P ≤ finDim K Q := + LinearMap.finrank_le_finrank_of_injective (f.linear_injective_iff.mpr hf) + +theorem finDim_le_of_surjective (f : P →ᵃ[K] Q) (hf : Function.Surjective f) : + finDim K Q ≤ finDim K P := + LinearMap.finrank_le_finrank_of_surjective (f.linear_surjective_iff.mpr hf) + +end Map + +end FiniteDimensional + +/-- An affine space is finite-dimensional exactly when a finite set of points spans it. -/ +theorem finiteDimensional_iff_exists_finset_affineSpan : + FiniteDimensional K P ↔ ∃ S : Finset P, affineSpan K (S : Set P) = ⊤ := by + constructor + · intro h + let := h + exact FiniteDimensional.exists_finset_affineSpan + · rintro ⟨S, hS⟩ + have h : _root_.FiniteDimensional K (affineSpan K (S : Set P)).direction := + finiteDimensional_direction_affineSpan_of_finite K S.finite_toSet + rw [hS, AffineSubspace.direction_top] at h + let := h + exact Submodule.topEquiv.finiteDimensional + +section Equiv + +variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q] + +theorem finiteDimensional_iff_of_equiv (e : P ≃ᵃ[K] Q) : + FiniteDimensional K P ↔ FiniteDimensional K Q := by + constructor + · intro h + let := h + exact FiniteDimensional.of_equiv e + · intro h + let := h + exact FiniteDimensional.of_equiv e.symm + +theorem finDim_eq_of_equiv (e : P ≃ᵃ[K] Q) : finDim K P = finDim K Q := + e.linear.finrank_eq + +end Equiv + +end AffineSpace From 4b1032b4acd5a4511eff4da59e4dae1fb62e1d42 Mon Sep 17 00:00:00 2001 From: Martin Winter Date: Thu, 1 Oct 2026 22:12:01 +0200 Subject: [PATCH 3/6] Add FinDim for sets --- Polyhedral.lean | 1 + .../Convex/ConvexSpace/Polytope/Basic.lean | 14 + .../Geometry/Convex/ConvexSpace/Set/Hull.lean | 12 + .../AffineSubspace/FiniteDimensional.lean | 100 +++--- .../LinearAlgebra/AffineSpace/FinDim.lean | 314 ++++++++++++++++++ 5 files changed, 392 insertions(+), 49 deletions(-) create mode 100644 Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean diff --git a/Polyhedral.lean b/Polyhedral.lean index 2b27d790..4a6a1279 100644 --- a/Polyhedral.lean +++ b/Polyhedral.lean @@ -73,6 +73,7 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FinDim public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean index 3d3fbf9f..9ca7bf49 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean @@ -97,6 +97,20 @@ protected lemma prod {P₂ : Set Y} (hP₁ : IsPolytope R P₁) (hP₂ : IsPolyt end Semiring +section Ring + +variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] +variable [ConvexSpace R X] +variable [AddCommGroup V] [Module R V] [AddTorsor V X] [IsAffineConvexSpace R V X] + +/-- Every polytope has finite-dimensional affine span, even in an infinite-dimensional +ambient space. -/ +theorem finDim {P : Set X} (hP : IsPolytope R P) : Affine.FinDim R P := by + obtain ⟨t, rfl⟩ := hP + exact (Affine.FinDim.finset t).convexHull + +end Ring + section Field variable [Field R] [PartialOrder R] [IsStrictOrderedRing R] diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean index cfa2a745..3f1fa72b 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean @@ -3,6 +3,7 @@ module public import Polyhedral.Mathlib.Geometry.Convex.AffineMap.Module public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace public import Polyhedral.Mathlib.Geometry.Convex.Hull +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FinDim public section @@ -28,6 +29,17 @@ theorem vectorSpan_convexHull (s : Set A) : vectorSpan R (convexHull R s : Set A) = vectorSpan R s := by rw [← direction_affineSpan, affineSpan_convexHull, direction_affineSpan] +/-- Taking the convex hull preserves finite-dimensionality of a set. -/ +@[simp] +theorem finDim_convexHull_iff (s : Set A) : + Affine.FinDim R (convexHull R s : Set A) ↔ Affine.FinDim R s := by + unfold Affine.FinDim + rw [vectorSpan_convexHull] + +theorem _root_.Affine.FinDim.convexHull {s : Set A} (hs : Affine.FinDim R s) : + Affine.FinDim R (convexHull R s : Set A) := + (finDim_convexHull_iff s).mpr hs + variable [ConvexSpace R V] [IsModuleConvexSpace R V] @[simp] diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean index 393afb47..d136e40a 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean @@ -10,8 +10,9 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional /-! # Finite-dimensional affine subspaces -`AffineSubspace.FiniteDimensional s` means that the direction of `s` is finite-dimensional. -It is an abbreviation, just as `FiniteDimensional` is an abbreviation for `Module.Finite`. +`AffineSubspace.FinDim s` means that the direction of `s` is a finite module. +Over a division ring this is finite-dimensionality; over a general ring it is finite generation. +It abbreviates `Module.Finite`, as does `FiniteDimensional` for vector spaces. The closure lemmas in this file take explicit proofs of this predicate and register no additional instances. A proof can still be installed locally with `let := hs` to use Mathlib's API for `s.direction`, `s.dim`, and `s.finDim`. @@ -31,20 +32,21 @@ namespace AffineSubspace variable {K V P : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V P] -/-- An affine subspace is finite-dimensional if its direction is finite-dimensional. +/-- An affine subspace is finite-dimensional if its direction is a finite module. In particular, the empty affine subspace is finite-dimensional. -/ -abbrev FiniteDimensional (s : AffineSubspace K P) : Prop := - _root_.FiniteDimensional K s.direction +abbrev FinDim {R V A : Type*} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V A] + (s : AffineSubspace R A) : Prop := + Module.Finite R s.direction variable {s t : AffineSubspace K P} theorem finiteDimensional_iff_direction : - s.FiniteDimensional ↔ _root_.FiniteDimensional K s.direction := Iff.rfl + s.FinDim ↔ _root_.FiniteDimensional K s.direction := Iff.rfl /-- A nonempty affine subspace has the same finite-dimensionality as its underlying affine space. This comparison is a theorem, not an instance. -/ theorem finiteDimensional_iff_affineSpace (s : AffineSubspace K P) [Nonempty s] : - s.FiniteDimensional ↔ AffineSpace.FiniteDimensional K s := Iff.rfl + s.FinDim ↔ AffineSpace.FiniteDimensional K s := Iff.rfl theorem dim_eq_affine_dim (s : AffineSubspace K P) [Nonempty s] : s.dim = (AffineSpace.dim K s : WithBot Cardinal) := @@ -56,8 +58,8 @@ theorem finDim_eq_affine_finDim (s : AffineSubspace K P) [Nonempty s] : @[simp] theorem finiteDimensional_top_iff : - (⊤ : AffineSubspace K P).FiniteDimensional ↔ _root_.FiniteDimensional K V := by - unfold FiniteDimensional + (⊤ : AffineSubspace K P).FinDim ↔ _root_.FiniteDimensional K V := by + unfold FinDim rw [direction_top] exact ⟨fun h ↦ by let := h @@ -67,52 +69,52 @@ theorem finiteDimensional_top_iff : @[simp] theorem finiteDimensional_toAffineSubspace_iff (S : Submodule K V) : - S.toAffineSubspace.FiniteDimensional ↔ _root_.FiniteDimensional K S := by - unfold FiniteDimensional + S.toAffineSubspace.FinDim ↔ _root_.FiniteDimensional K S := by + unfold FinDim rw [Submodule.toAffineSubspace_direction] theorem finiteDimensional_toAffineSubspace (S : Submodule K V) - (hS : _root_.FiniteDimensional K S) : S.toAffineSubspace.FiniteDimensional := + (hS : _root_.FiniteDimensional K S) : S.toAffineSubspace.FinDim := (finiteDimensional_toAffineSubspace_iff S).mpr hS theorem finiteDimensional_mk' (p : P) (S : Submodule K V) - (hS : _root_.FiniteDimensional K S) : (mk' p S).FiniteDimensional := by - unfold FiniteDimensional + (hS : _root_.FiniteDimensional K S) : (mk' p S).FinDim := by + unfold FinDim rw [direction_mk'] exact hS /-- Every affine subspace of a finite-dimensional ambient space is finite-dimensional. -/ theorem finiteDimensional_of_finiteDimensional - [AffineSpace.FiniteDimensional K P] (s : AffineSubspace K P) : s.FiniteDimensional := + [AffineSpace.FiniteDimensional K P] (s : AffineSubspace K P) : s.FinDim := inferInstanceAs (_root_.FiniteDimensional K s.direction) -theorem finiteDimensional_bot : (⊥ : AffineSubspace K P).FiniteDimensional := by - unfold FiniteDimensional +theorem finiteDimensional_bot : (⊥ : AffineSubspace K P).FinDim := by + unfold FinDim rw [direction_bot] infer_instance /-- Finite-dimensionality descends to affine subspaces. -/ -theorem finiteDimensional_of_le (ht : t.FiniteDimensional) (h : s ≤ t) : - s.FiniteDimensional := by +theorem finiteDimensional_of_le (ht : t.FinDim) (h : s ≤ t) : + s.FinDim := by let := ht exact Submodule.finiteDimensional_of_le (direction_le h) -theorem finiteDimensional_inf_left (s t : AffineSubspace K P) (hs : s.FiniteDimensional) : - (s ⊓ t).FiniteDimensional := +theorem finiteDimensional_inf_left (s t : AffineSubspace K P) (hs : s.FinDim) : + (s ⊓ t).FinDim := finiteDimensional_of_le hs inf_le_left -theorem finiteDimensional_inf_right (s t : AffineSubspace K P) (ht : t.FiniteDimensional) : - (s ⊓ t).FiniteDimensional := +theorem finiteDimensional_inf_right (s t : AffineSubspace K P) (ht : t.FinDim) : + (s ⊓ t).FinDim := finiteDimensional_of_le ht inf_le_right /-- An indexed intersection is finite-dimensional if one of its members is. -/ theorem finiteDimensional_iInf {ι : Sort*} (S : ι → AffineSubspace K P) (i : ι) - (hi : (S i).FiniteDimensional) : (⨅ j, S j).FiniteDimensional := + (hi : (S i).FinDim) : (⨅ j, S j).FinDim := finiteDimensional_of_le hi (iInf_le S i) theorem finiteDimensional_finset_sup {ι : Type*} (I : Finset ι) - (S : ι → AffineSubspace K P) (hS : ∀ i ∈ I, (S i).FiniteDimensional) : - (I.sup S).FiniteDimensional := by + (S : ι → AffineSubspace K P) (hS : ∀ i ∈ I, (S i).FinDim) : + (I.sup S).FinDim := by refine Finset.sup_induction finiteDimensional_bot ?_ hS intro s hs t ht let := hs @@ -120,49 +122,49 @@ theorem finiteDimensional_finset_sup {ι : Type*} (I : Finset ι) infer_instance theorem finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P) - (hS : ∀ i, (S i).FiniteDimensional) : (⨆ i, S i).FiniteDimensional := by + (hS : ∀ i, (S i).FinDim) : (⨆ i, S i).FinDim := by classical let := Fintype.ofFinite (PLift ι) simpa only [Finset.sup_univ_eq_iSup, iSup_plift_down] using finiteDimensional_finset_sup Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down) /-- A singleton is finite-dimensional, even in an infinite-dimensional ambient space. -/ -theorem finiteDimensional_singleton (p : P) : ({p} : AffineSubspace K P).FiniteDimensional := +theorem finiteDimensional_singleton (p : P) : ({p} : AffineSubspace K P).FinDim := inferInstance /-- Binary joins preserve finite-dimensionality. -/ -theorem finiteDimensional_sup_of_finiteDimensional (hs : s.FiniteDimensional) - (ht : t.FiniteDimensional) : (s ⊔ t).FiniteDimensional := by +theorem finiteDimensional_sup_of_finiteDimensional (hs : s.FinDim) + (ht : t.FinDim) : (s ⊔ t).FinDim := by let := hs let := ht infer_instance /-- The affine span of a finite set is finite-dimensional. -/ theorem finiteDimensional_affineSpan_of_finite {S : Set P} (hS : S.Finite) : - (affineSpan K S).FiniteDimensional := + (affineSpan K S).FinDim := finiteDimensional_direction_affineSpan_of_finite K hS theorem finiteDimensional_affineSpan_finset (S : Finset P) : - (affineSpan K (S : Set P)).FiniteDimensional := + (affineSpan K (S : Set P)).FinDim := finiteDimensional_affineSpan_of_finite S.finite_toSet /-- The affine span of a subset of a finite-dimensional subspace is finite-dimensional. -/ -theorem finiteDimensional_affineSpan_of_subset (hs : s.FiniteDimensional) {S : Set P} - (hS : S ⊆ s) : (affineSpan K S).FiniteDimensional := +theorem finiteDimensional_affineSpan_of_subset (hs : s.FinDim) {S : Set P} + (hS : S ⊆ s) : (affineSpan K S).FinDim := finiteDimensional_of_le hs (affineSpan_le.mpr hS) section Map variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q] -theorem finiteDimensional_map (hs : s.FiniteDimensional) (f : P →ᵃ[K] Q) : - (s.map f).FiniteDimensional := by +theorem finiteDimensional_map (hs : s.FinDim) (f : P →ᵃ[K] Q) : + (s.map f).FinDim := by let := hs infer_instance /-- Finite-dimensionality descends along an injective affine map. -/ theorem finiteDimensional_of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) - (hs : (s.map f).FiniteDimensional) : s.FiniteDimensional := by + (hs : (s.map f).FinDim) : s.FinDim := by have : _root_.FiniteDimensional K (s.direction.map f.linear) := by rw [← map_direction] exact hs @@ -170,41 +172,41 @@ theorem finiteDimensional_of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) (f.linear_injective_iff.mpr hf) s.direction).symm.finiteDimensional theorem finiteDimensional_map_iff {f : P →ᵃ[K] Q} (hf : Function.Injective f) : - (s.map f).FiniteDimensional ↔ s.FiniteDimensional := by + (s.map f).FinDim ↔ s.FinDim := by constructor · exact finiteDimensional_of_map hf · exact fun h ↦ finiteDimensional_map h f /-- An injective affine preimage of a finite-dimensional subspace is finite-dimensional. -/ theorem finiteDimensional_comap_of_injective {f : P →ᵃ[K] Q} (hf : Function.Injective f) - (t : AffineSubspace K Q) (ht : t.FiniteDimensional) : (t.comap f).FiniteDimensional := + (t : AffineSubspace K Q) (ht : t.FinDim) : (t.comap f).FinDim := finiteDimensional_of_map hf (finiteDimensional_of_le ht (map_comap_le f t)) @[simp] theorem finiteDimensional_map_equiv_iff (e : P ≃ᵃ[K] Q) : - (s.map e.toAffineMap).FiniteDimensional ↔ s.FiniteDimensional := + (s.map e.toAffineMap).FinDim ↔ s.FinDim := finiteDimensional_map_iff e.injective end Map /-- Finite-dimensional affine subspaces are precisely the affine spans of finite sets. -/ theorem finiteDimensional_iff_exists_finite_affineSpan : - s.FiniteDimensional ↔ ∃ S : Set P, S.Finite ∧ affineSpan K S = s := by + s.FinDim ↔ ∃ S : Set P, S.Finite ∧ affineSpan K S = s := by constructor · intro hs let := hs obtain ⟨S, -, hS, hI⟩ := exists_affineIndependent K V (s : Set P) have hspan : affineSpan K S = s := hS.trans (affineSpan_coe s) - have : (affineSpan K S).FiniteDimensional := hspan ▸ hs + have : (affineSpan K S).FinDim := hspan ▸ hs have : _root_.FiniteDimensional K (vectorSpan K (Set.range ((↑) : S → P))) := by rw [Subtype.range_coe, ← direction_affineSpan] - exact (inferInstance : (affineSpan K S).FiniteDimensional) + exact (inferInstance : (affineSpan K S).FinDim) exact ⟨S, (finiteDimensional_iff_setFinite K hI).mp inferInstance, hspan⟩ · rintro ⟨S, hS, rfl⟩ exact finiteDimensional_affineSpan_of_finite hS theorem finiteDimensional_iff_exists_finset_affineSpan : - s.FiniteDimensional ↔ ∃ S : Finset P, affineSpan K (S : Set P) = s := by + s.FinDim ↔ ∃ S : Finset P, affineSpan K (S : Set P) = s := by classical rw [finiteDimensional_iff_exists_finite_affineSpan] exact ⟨fun ⟨S, hS, hspan⟩ ↦ ⟨hS.toFinset, by simpa using hspan⟩, @@ -212,12 +214,12 @@ theorem finiteDimensional_iff_exists_finset_affineSpan : /-- The cardinal-valued dimension detects finite-dimensionality, including for `⊥`. -/ theorem finiteDimensional_iff_dim_lt_aleph0 : - s.FiniteDimensional ↔ s.dim < (Cardinal.aleph0 : WithBot Cardinal) := + s.FinDim ↔ s.dim < (Cardinal.aleph0 : WithBot Cardinal) := finite_iff_dim_lt_aleph0 s /-- In finite dimension, the cardinal dimension is the natural dimension cast to cardinals. This formulation also applies to the empty subspace. -/ -theorem dim_eq_map_finDim (hs : s.FiniteDimensional) : +theorem dim_eq_map_finDim (hs : s.FinDim) : s.dim = s.finDim.map (fun n : ℕ ↦ (n : Cardinal)) := by let := hs rcases eq_or_ne s ⊥ with rfl | hbot @@ -226,17 +228,17 @@ theorem dim_eq_map_finDim (hs : s.FiniteDimensional) : exact (Module.finrank_eq_rank' (K := K) (V := s.direction)).symm /-- A finite-dimensional affine subspace is determined by inclusion and finite dimension. -/ -theorem eq_of_le_of_finDim_eq (ht : t.FiniteDimensional) (h : s ≤ t) +theorem eq_of_le_of_finDim_eq (ht : t.FinDim) (h : s ≤ t) (hd : s.finDim = t.finDim) : s = t := by let := ht by_contra hne exact (ne_of_lt (finDim_strictMono (lt_of_le_of_ne h hne))) hd -theorem finDim_eq_iff_eq_of_le (ht : t.FiniteDimensional) (h : s ≤ t) : +theorem finDim_eq_iff_eq_of_le (ht : t.FinDim) (h : s ≤ t) : s.finDim = t.finDim ↔ s = t := ⟨eq_of_le_of_finDim_eq ht h, fun h ↦ congrArg finDim h⟩ -theorem lt_iff_finDim_lt_of_le (ht : t.FiniteDimensional) (h : s ≤ t) : +theorem lt_iff_finDim_lt_of_le (ht : t.FinDim) (h : s ≤ t) : s < t ↔ s.finDim < t.finDim := by let := ht refine ⟨finDim_strictMono, fun hd ↦ lt_of_le_of_ne h ?_⟩ diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean new file mode 100644 index 00000000..c362d4b2 --- /dev/null +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean @@ -0,0 +1,314 @@ +/- +Copyright (c) 2026 Martin Winter. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Martin Winter +-/ +module + +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs +public import Mathlib.Algebra.Group.Pointwise.Set.Finite +public import Mathlib.Algebra.Order.SuccPred.WithBot + +/-! +# Finite-dimensional subsets of affine spaces + +`Affine.FinDim R s` means that the affine span of a set `s` has finitely generated +direction. Over a division ring this is finite-dimensionality. The abbreviation is +definitionally `Module.Finite R (vectorSpan R s)`, so existing assumptions on the vector +span can be written `[Affine.FinDim R s]` without conversion instances. + +This is a predicate, distinct from the numerical dimension `Affine.finrank R s` and +`(affineSpan R s).finDim`. The empty set satisfies the predicate and its affine span has +dimension `⊥`. Closure lemmas take explicit proofs and register no additional instances. + +The API includes affine-span and image invariance, finite unions, descent to subsets over +a division ring, dimension comparisons, and finite independent spanning subsets with +cardinality `(affineSpan R s).finDim.succ`. The last formulation also covers the empty set +and is suited to homogenization and grading of polytope faces. +-/ + +@[expose] public section + +namespace Affine + +/-- A subset of an affine space is finite-dimensional when its vector span is a finite module. +The definition also applies over rings, where it expresses finite generation. -/ +abbrev FinDim (R : Type*) {V A : Type*} [Ring R] [AddCommGroup V] [Module R V] + [AddTorsor V A] (s : Set A) : Prop := + Module.Finite R (vectorSpan R s) + +section Ring + +variable {R V A : Type*} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V A] +variable {s t : Set A} + +theorem finDim_iff_vectorSpan : FinDim R s ↔ Module.Finite R (vectorSpan R s) := Iff.rfl + +@[simp] +theorem finDim_coe_iff (S : AffineSubspace R A) : FinDim R (S : Set A) ↔ S.FinDim := + Iff.rfl + +/-- View a finite-dimensional affine subspace as a finite-dimensional subset. -/ +theorem _root_.AffineSubspace.FinDim.coe {S : AffineSubspace R A} (hS : S.FinDim) : + FinDim R (S : Set A) := + (finDim_coe_iff S).mpr hS + +/-- Finite-dimensionality is exactly finite-dimensionality of the affine span. -/ +theorem finDim_iff_affineSpan : FinDim R s ↔ (_root_.affineSpan R s).FinDim := by + unfold FinDim AffineSubspace.FinDim + rw [direction_affineSpan] + +@[simp] +theorem finDim_affineSpan_iff : FinDim R (_root_.affineSpan R s : Set A) ↔ FinDim R s := by + rw [finDim_coe_iff, ← finDim_iff_affineSpan] + +theorem finDim_congr (h : _root_.affineSpan R s = _root_.affineSpan R t) : + FinDim R s ↔ FinDim R t := by + rw [finDim_iff_affineSpan, h, ← finDim_iff_affineSpan] + +namespace FinDim + +theorem affineSpan (hs : FinDim R s) : (_root_.affineSpan R s).FinDim := + finDim_iff_affineSpan.mp hs + +theorem of_affineSpan_eq (hs : FinDim R s) (h : _root_.affineSpan R t = _root_.affineSpan R s) : + FinDim R t := + (finDim_congr h).mpr hs + +/-- Every finite set of points is finite-dimensional, over any ring. -/ +theorem of_finite (hs : s.Finite) : FinDim R s := by + unfold FinDim + rw [vectorSpan_def] + exact Module.Finite.span_of_finite R (hs.vsub hs) + +theorem finset (S : Finset A) : FinDim R (S : Set A) := of_finite S.finite_toSet + +@[simp] +theorem empty : FinDim R (∅ : Set A) := of_finite Set.finite_empty + +@[simp] +theorem singleton (p : A) : FinDim R ({p} : Set A) := of_finite (Set.finite_singleton p) + +theorem of_subsingleton (hs : s.Subsingleton) : FinDim R s := of_finite hs.finite + +theorem range {ι : Sort*} [Finite ι] (p : ι → A) : FinDim R (Set.range p) := + of_finite (Set.finite_range p) + +/-- A finite union of finite-dimensional sets is finite-dimensional. The joining direction +between two disjoint affine spans is included in the proof. -/ +theorem union (hs : FinDim R s) (ht : FinDim R t) : FinDim R (s ∪ t) := by + rcases s.eq_empty_or_nonempty with rfl | ⟨p, hp⟩ + · simpa using ht + rcases t.eq_empty_or_nonempty with rfl | ⟨q, hq⟩ + · simpa using hs + have : Module.Finite R (_root_.affineSpan R s).direction := hs.affineSpan + have : Module.Finite R (_root_.affineSpan R t).direction := ht.affineSpan + unfold FinDim + rw [← direction_affineSpan, AffineSubspace.span_union, + AffineSubspace.direction_sup (mem_affineSpan R hp) (mem_affineSpan R hq)] + infer_instance + +theorem insert (hs : FinDim R s) (p : A) : FinDim R (insert p s) := by + simpa only [Set.singleton_union] using (singleton p).union hs + +theorem biUnion {ι : Type*} (I : Finset ι) (S : ι → Set A) + (hS : ∀ i ∈ I, FinDim R (S i)) : FinDim R (⋃ i ∈ I, S i) := by + classical + induction I using Finset.induction_on with + | empty => simp + | @insert i I hi ih => + rw [Finset.set_biUnion_insert] + exact (hS i (Finset.mem_insert_self _ _)).union + (ih (fun j hj ↦ hS j (Finset.mem_insert_of_mem hj))) + +theorem iUnion {ι : Sort*} [Finite ι] (S : ι → Set A) (hS : ∀ i, FinDim R (S i)) : + FinDim R (⋃ i, S i) := by + classical + let := Fintype.ofFinite (PLift ι) + simpa only [Finset.mem_univ, Set.iUnion_true, Set.iUnion_plift_down] using + biUnion Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down) + +section Image + +variable {W B : Type*} [AddCommGroup W] [Module R W] [AddTorsor W B] + +theorem image (hs : FinDim R s) (f : A →ᵃ[R] B) : FinDim R (f '' s) := by + let := hs + unfold FinDim + rw [← f.map_vectorSpan] + infer_instance + +theorem of_image {f : A →ᵃ[R] B} (hs : FinDim R (f '' s)) (hf : Function.Injective f) : + FinDim R s := by + have : Module.Finite R ((vectorSpan R s).map f.linear) := by + rw [f.map_vectorSpan] + exact hs + exact Module.Finite.equiv + (Submodule.equivMapOfInjective f.linear (f.linear_injective_iff.mpr hf) _).symm + +end Image + +end FinDim + +section Image + +variable {W B : Type*} [AddCommGroup W] [Module R W] [AddTorsor W B] + +theorem finDim_image_iff {f : A →ᵃ[R] B} (hf : Function.Injective f) : + FinDim R (f '' s) ↔ FinDim R s := + ⟨fun h ↦ h.of_image hf, fun h ↦ h.image f⟩ + +@[simp] +theorem finDim_image_equiv_iff (e : A ≃ᵃ[R] B) : FinDim R (e '' s) ↔ FinDim R s := + finDim_image_iff (f := e.toAffineMap) e.injective + +end Image + +end Ring + +section DivisionRing + +variable {K V A : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V A] +variable {s t : Set A} + +@[simp] +theorem finDim_univ_iff : + FinDim K (Set.univ : Set A) ↔ AffineSpace.FiniteDimensional K A := by + rw [finDim_iff_affineSpan, AffineSubspace.span_univ, + AffineSubspace.finiteDimensional_top_iff] + +@[simp] +theorem finDim_union_iff : FinDim K (s ∪ t) ↔ FinDim K s ∧ FinDim K t := by + constructor + · intro h + let := h + exact ⟨Submodule.finiteDimensional_of_le + (vectorSpan_mono K (Set.subset_union_left : s ⊆ s ∪ t)), + Submodule.finiteDimensional_of_le + (vectorSpan_mono K (Set.subset_union_right : t ⊆ s ∪ t))⟩ + · exact fun ⟨hs, ht⟩ ↦ hs.union ht + +theorem finDim_iff_dim_lt_aleph0 : + FinDim K s ↔ (_root_.affineSpan K s).dim < (Cardinal.aleph0 : WithBot Cardinal) := by + rw [finDim_iff_affineSpan] + exact AffineSubspace.finiteDimensional_iff_dim_lt_aleph0 + +theorem finDim_iff_rank_lt_aleph0 : FinDim K s ↔ rank K s < Cardinal.aleph0 := by + unfold FinDim rank + rw [direction_affineSpan] + exact Module.rank_lt_aleph0_iff.symm + +theorem finDim_iff_exists_finite_affineSpan : + FinDim K s ↔ ∃ t : Set A, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s := by + rw [finDim_iff_affineSpan, AffineSubspace.finiteDimensional_iff_exists_finite_affineSpan] + +theorem finDim_iff_exists_finset_affineSpan : + FinDim K s ↔ ∃ t : Finset A, _root_.affineSpan K (t : Set A) = _root_.affineSpan K s := by + rw [finDim_iff_affineSpan, AffineSubspace.finiteDimensional_iff_exists_finset_affineSpan] + +namespace FinDim + +/-- Finite-dimensionality descends to every subset over a division ring. -/ +theorem mono (ht : FinDim K t) (h : s ⊆ t) : FinDim K s := by + let := ht + exact Submodule.finiteDimensional_of_le (vectorSpan_mono K h) + +theorem of_finiteDimensional [AffineSpace.FiniteDimensional K A] (s : Set A) : FinDim K s := + inferInstanceAs (Module.Finite K (vectorSpan K s)) + +theorem inter_left (hs : FinDim K s) (t : Set A) : FinDim K (s ∩ t) := + hs.mono Set.inter_subset_left + +theorem inter_right (ht : FinDim K t) (s : Set A) : FinDim K (s ∩ t) := + ht.mono Set.inter_subset_right + +theorem diff (hs : FinDim K s) (t : Set A) : FinDim K (s \ t) := hs.mono Set.sdiff_subset + +theorem finrank_mono (ht : FinDim K t) (h : s ⊆ t) : finrank K s ≤ finrank K t := by + let := ht + unfold finrank + rw [direction_affineSpan, direction_affineSpan] + exact Submodule.finrank_mono (vectorSpan_mono K h) + +theorem finDim_mono (ht : FinDim K t) (h : s ⊆ t) : + (_root_.affineSpan K s).finDim ≤ (_root_.affineSpan K t).finDim := by + have := ht.affineSpan + exact AffineSubspace.finDim_mono (affineSpan_mono K h) + +theorem finrank_eq_rank (hs : FinDim K s) : (finrank K s : Cardinal) = rank K s := by + have := hs.affineSpan + exact Module.finrank_eq_rank' K (_root_.affineSpan K s).direction + +/-- Equal dimensions and inclusion imply equality of the affine spans, not necessarily of +the original sets. -/ +theorem affineSpan_eq_of_subset_of_finDim_eq (ht : FinDim K t) (h : s ⊆ t) + (hd : (_root_.affineSpan K s).finDim = (_root_.affineSpan K t).finDim) : + _root_.affineSpan K s = _root_.affineSpan K t := + AffineSubspace.eq_of_le_of_finDim_eq ht.affineSpan (affineSpan_mono K h) hd + +end FinDim + +end DivisionRing + +end Affine + +section AffineIndependent + +variable {K V A : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V A] +variable {s : Set A} + +/-- An independent set in a finite-dimensional affine span is finite. -/ +theorem AffineIndepOn.finite_of_finDim (hi : AffineIndepOn K id s) + (hs : Affine.FinDim K s) : s.Finite := by + have h : FiniteDimensional K (vectorSpan K (Set.range ((↑) : s → A))) := by + rw [Subtype.range_coe] + exact hs + exact (finiteDimensional_iff_setFinite K hi).mp h + +/-- An independent set has one more point than its affine dimension. Using `WithBot.succ` +also covers the empty set: the successor of its dimension `⊥` is zero. -/ +theorem AffineIndepOn.ncard_eq_succ_finDim_affineSpan (hi : AffineIndepOn K id s) + [hs : Affine.FinDim K s] : s.ncard = (_root_.affineSpan K s).finDim.succ := by + have hfinite := hi.finite_of_finDim hs + rcases s.eq_empty_or_nonempty with rfl | hnonempty + · simp + rw [AffineSubspace.finDim_eq_finrank + (by simpa [← Set.nonempty_iff_ne_empty] using hnonempty), direction_affineSpan, + WithBot.succ_natCast, hi.finrank_vectorSpan hfinite hnonempty] + exact (Nat.sub_add_cancel (Nat.succ_le_of_lt ((Set.ncard_pos hfinite).mpr hnonempty))).symm + +theorem AffineIndependent.ncard_eq_succ_finDim_affineSpan + (hi : AffineIndependent K ((↑) : s → A)) [Affine.FinDim K s] : + s.ncard = (_root_.affineSpan K s).finDim.succ := + (show AffineIndepOn K id s from hi).ncard_eq_succ_finDim_affineSpan + +namespace Affine.FinDim + +/-- A finite-dimensional set contains a finite independent subset spanning the same affine +subspace. Its cardinality is already expressed in terms of the original set's dimension. -/ +theorem exists_affineIndependent (hs : Affine.FinDim K s) : + ∃ t ⊆ s, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s ∧ + AffineIndependent K ((↑) : t → A) ∧ t.ncard = (_root_.affineSpan K s).finDim.succ := by + obtain ⟨t, ht, hspan, hi⟩ := _root_.exists_affineIndependent K V s + have htDim : Affine.FinDim K t := hs.of_affineSpan_eq hspan + have hai : AffineIndepOn K id t := hi + let := htDim + refine ⟨t, ht, hai.finite_of_finDim htDim, hspan, hi, ?_⟩ + rw [← hspan] + exact hai.ncard_eq_succ_finDim_affineSpan + +theorem exists_affineIndepOn (hs : Affine.FinDim K s) : + ∃ t ⊆ s, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s ∧ + AffineIndepOn K id t ∧ t.ncard = (_root_.affineSpan K s).finDim.succ := + hs.exists_affineIndependent + +theorem exists_finset_subset_affineSpan (hs : Affine.FinDim K s) : + ∃ t : Finset A, (t : Set A) ⊆ s ∧ _root_.affineSpan K (t : Set A) = _root_.affineSpan K s := by + classical + obtain ⟨t, ht, hfinite, hspan, -, -⟩ := hs.exists_affineIndependent + exact ⟨hfinite.toFinset, by simpa using ht, by simpa using hspan⟩ + +end Affine.FinDim + +end AffineIndependent From 747006891dc27d78b8a532b94f8a226b037432a7 Mon Sep 17 00:00:00 2001 From: Martin Winter Date: Thu, 1 Oct 2026 23:14:08 +0200 Subject: [PATCH 4/6] Renames and moved --- Polyhedral.lean | 2 +- .../AffineSpace/{FinDim.lean => Set/FiniteDimensional.lean} | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename Polyhedral/Mathlib/LinearAlgebra/AffineSpace/{FinDim.lean => Set/FiniteDimensional.lean} (99%) diff --git a/Polyhedral.lean b/Polyhedral.lean index 4a6a1279..0fe8921c 100644 --- a/Polyhedral.lean +++ b/Polyhedral.lean @@ -73,11 +73,11 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FinDim public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Set.FiniteDimensional public import Polyhedral.Mathlib.LinearAlgebra.BilinearMap public import Polyhedral.Mathlib.LinearAlgebra.Dual.Basis public import Polyhedral.Mathlib.RingTheory.Finiteness.Cofinite diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean similarity index 99% rename from Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean rename to Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean index c362d4b2..0adeda8f 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FinDim.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean @@ -195,7 +195,7 @@ theorem finDim_iff_dim_lt_aleph0 : exact AffineSubspace.finiteDimensional_iff_dim_lt_aleph0 theorem finDim_iff_rank_lt_aleph0 : FinDim K s ↔ rank K s < Cardinal.aleph0 := by - unfold FinDim rank + unfold rank rw [direction_affineSpan] exact Module.rank_lt_aleph0_iff.symm From 836f2194734a234f9e52ec1a841dcd5f374355b5 Mon Sep 17 00:00:00 2001 From: Martin Winter Date: Fri, 2 Oct 2026 01:19:56 +0200 Subject: [PATCH 5/6] Naming fix --- .../AffineSubspace/FiniteDimensional.lean | 82 +++++++++---------- .../AffineSpace/Set/FiniteDimensional.lean | 8 +- 2 files changed, 45 insertions(+), 45 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean index d136e40a..0b91a8ed 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean @@ -40,12 +40,12 @@ abbrev FinDim {R V A : Type*} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor variable {s t : AffineSubspace K P} -theorem finiteDimensional_iff_direction : +theorem finDim_iff_direction : s.FinDim ↔ _root_.FiniteDimensional K s.direction := Iff.rfl /-- A nonempty affine subspace has the same finite-dimensionality as its underlying affine space. This comparison is a theorem, not an instance. -/ -theorem finiteDimensional_iff_affineSpace (s : AffineSubspace K P) [Nonempty s] : +theorem finDim_iff_affineSpace (s : AffineSubspace K P) [Nonempty s] : s.FinDim ↔ AffineSpace.FiniteDimensional K s := Iff.rfl theorem dim_eq_affine_dim (s : AffineSubspace K P) [Nonempty s] : @@ -57,7 +57,7 @@ theorem finDim_eq_affine_finDim (s : AffineSubspace K P) [Nonempty s] : finDim_eq_finrank (nonempty_iff_ne_bot s |>.mp (Set.nonempty_coe_sort.mp inferInstance)) @[simp] -theorem finiteDimensional_top_iff : +theorem finDim_top_iff : (⊤ : AffineSubspace K P).FinDim ↔ _root_.FiniteDimensional K V := by unfold FinDim rw [direction_top] @@ -68,102 +68,102 @@ theorem finiteDimensional_top_iff : infer_instance⟩ @[simp] -theorem finiteDimensional_toAffineSubspace_iff (S : Submodule K V) : +theorem finDim_toAffineSubspace_iff (S : Submodule K V) : S.toAffineSubspace.FinDim ↔ _root_.FiniteDimensional K S := by unfold FinDim rw [Submodule.toAffineSubspace_direction] -theorem finiteDimensional_toAffineSubspace (S : Submodule K V) +theorem FinDim.toAffineSubspace (S : Submodule K V) (hS : _root_.FiniteDimensional K S) : S.toAffineSubspace.FinDim := - (finiteDimensional_toAffineSubspace_iff S).mpr hS + (finDim_toAffineSubspace_iff S).mpr hS -theorem finiteDimensional_mk' (p : P) (S : Submodule K V) +theorem FinDim.mk' (p : P) (S : Submodule K V) (hS : _root_.FiniteDimensional K S) : (mk' p S).FinDim := by unfold FinDim rw [direction_mk'] exact hS /-- Every affine subspace of a finite-dimensional ambient space is finite-dimensional. -/ -theorem finiteDimensional_of_finiteDimensional +theorem FinDim.of_finiteDimensional [AffineSpace.FiniteDimensional K P] (s : AffineSubspace K P) : s.FinDim := inferInstanceAs (_root_.FiniteDimensional K s.direction) -theorem finiteDimensional_bot : (⊥ : AffineSubspace K P).FinDim := by +theorem FinDim.bot : (⊥ : AffineSubspace K P).FinDim := by unfold FinDim rw [direction_bot] infer_instance /-- Finite-dimensionality descends to affine subspaces. -/ -theorem finiteDimensional_of_le (ht : t.FinDim) (h : s ≤ t) : +theorem FinDim.mono (ht : t.FinDim) (h : s ≤ t) : s.FinDim := by let := ht exact Submodule.finiteDimensional_of_le (direction_le h) -theorem finiteDimensional_inf_left (s t : AffineSubspace K P) (hs : s.FinDim) : +theorem FinDim.inf_left (s t : AffineSubspace K P) (hs : s.FinDim) : (s ⊓ t).FinDim := - finiteDimensional_of_le hs inf_le_left + FinDim.mono hs inf_le_left -theorem finiteDimensional_inf_right (s t : AffineSubspace K P) (ht : t.FinDim) : +theorem FinDim.inf_right (s t : AffineSubspace K P) (ht : t.FinDim) : (s ⊓ t).FinDim := - finiteDimensional_of_le ht inf_le_right + FinDim.mono ht inf_le_right /-- An indexed intersection is finite-dimensional if one of its members is. -/ -theorem finiteDimensional_iInf {ι : Sort*} (S : ι → AffineSubspace K P) (i : ι) +theorem FinDim.iInf {ι : Sort*} (S : ι → AffineSubspace K P) (i : ι) (hi : (S i).FinDim) : (⨅ j, S j).FinDim := - finiteDimensional_of_le hi (iInf_le S i) + FinDim.mono hi (iInf_le S i) -theorem finiteDimensional_finset_sup {ι : Type*} (I : Finset ι) +theorem FinDim.finset_sup {ι : Type*} (I : Finset ι) (S : ι → AffineSubspace K P) (hS : ∀ i ∈ I, (S i).FinDim) : (I.sup S).FinDim := by - refine Finset.sup_induction finiteDimensional_bot ?_ hS + refine Finset.sup_induction FinDim.bot ?_ hS intro s hs t ht let := hs let := ht infer_instance -theorem finiteDimensional_iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P) +theorem FinDim.iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P) (hS : ∀ i, (S i).FinDim) : (⨆ i, S i).FinDim := by classical let := Fintype.ofFinite (PLift ι) simpa only [Finset.sup_univ_eq_iSup, iSup_plift_down] using - finiteDimensional_finset_sup Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down) + FinDim.finset_sup Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down) /-- A singleton is finite-dimensional, even in an infinite-dimensional ambient space. -/ -theorem finiteDimensional_singleton (p : P) : ({p} : AffineSubspace K P).FinDim := +theorem FinDim.singleton (p : P) : ({p} : AffineSubspace K P).FinDim := inferInstance /-- Binary joins preserve finite-dimensionality. -/ -theorem finiteDimensional_sup_of_finiteDimensional (hs : s.FinDim) +theorem FinDim.sup (hs : s.FinDim) (ht : t.FinDim) : (s ⊔ t).FinDim := by let := hs let := ht infer_instance /-- The affine span of a finite set is finite-dimensional. -/ -theorem finiteDimensional_affineSpan_of_finite {S : Set P} (hS : S.Finite) : +theorem FinDim.affineSpan_of_finite {S : Set P} (hS : S.Finite) : (affineSpan K S).FinDim := finiteDimensional_direction_affineSpan_of_finite K hS -theorem finiteDimensional_affineSpan_finset (S : Finset P) : +theorem FinDim.affineSpan_finset (S : Finset P) : (affineSpan K (S : Set P)).FinDim := - finiteDimensional_affineSpan_of_finite S.finite_toSet + FinDim.affineSpan_of_finite S.finite_toSet /-- The affine span of a subset of a finite-dimensional subspace is finite-dimensional. -/ -theorem finiteDimensional_affineSpan_of_subset (hs : s.FinDim) {S : Set P} +theorem FinDim.affineSpan_of_subset (hs : s.FinDim) {S : Set P} (hS : S ⊆ s) : (affineSpan K S).FinDim := - finiteDimensional_of_le hs (affineSpan_le.mpr hS) + FinDim.mono hs (affineSpan_le.mpr hS) section Map variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q] -theorem finiteDimensional_map (hs : s.FinDim) (f : P →ᵃ[K] Q) : +theorem FinDim.map (hs : s.FinDim) (f : P →ᵃ[K] Q) : (s.map f).FinDim := by let := hs infer_instance /-- Finite-dimensionality descends along an injective affine map. -/ -theorem finiteDimensional_of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) +theorem FinDim.of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) (hs : (s.map f).FinDim) : s.FinDim := by have : _root_.FiniteDimensional K (s.direction.map f.linear) := by rw [← map_direction] @@ -171,26 +171,26 @@ theorem finiteDimensional_of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f) exact (Submodule.equivMapOfInjective f.linear (f.linear_injective_iff.mpr hf) s.direction).symm.finiteDimensional -theorem finiteDimensional_map_iff {f : P →ᵃ[K] Q} (hf : Function.Injective f) : +theorem finDim_map_iff {f : P →ᵃ[K] Q} (hf : Function.Injective f) : (s.map f).FinDim ↔ s.FinDim := by constructor - · exact finiteDimensional_of_map hf - · exact fun h ↦ finiteDimensional_map h f + · exact FinDim.of_map hf + · exact fun h ↦ FinDim.map h f /-- An injective affine preimage of a finite-dimensional subspace is finite-dimensional. -/ -theorem finiteDimensional_comap_of_injective {f : P →ᵃ[K] Q} (hf : Function.Injective f) +theorem FinDim.comap_of_injective {f : P →ᵃ[K] Q} (hf : Function.Injective f) (t : AffineSubspace K Q) (ht : t.FinDim) : (t.comap f).FinDim := - finiteDimensional_of_map hf (finiteDimensional_of_le ht (map_comap_le f t)) + FinDim.of_map hf (FinDim.mono ht (map_comap_le f t)) @[simp] -theorem finiteDimensional_map_equiv_iff (e : P ≃ᵃ[K] Q) : +theorem finDim_map_equiv_iff (e : P ≃ᵃ[K] Q) : (s.map e.toAffineMap).FinDim ↔ s.FinDim := - finiteDimensional_map_iff e.injective + finDim_map_iff e.injective end Map /-- Finite-dimensional affine subspaces are precisely the affine spans of finite sets. -/ -theorem finiteDimensional_iff_exists_finite_affineSpan : +theorem finDim_iff_exists_finite_affineSpan : s.FinDim ↔ ∃ S : Set P, S.Finite ∧ affineSpan K S = s := by constructor · intro hs @@ -203,17 +203,17 @@ theorem finiteDimensional_iff_exists_finite_affineSpan : exact (inferInstance : (affineSpan K S).FinDim) exact ⟨S, (finiteDimensional_iff_setFinite K hI).mp inferInstance, hspan⟩ · rintro ⟨S, hS, rfl⟩ - exact finiteDimensional_affineSpan_of_finite hS + exact FinDim.affineSpan_of_finite hS -theorem finiteDimensional_iff_exists_finset_affineSpan : +theorem finDim_iff_exists_finset_affineSpan : s.FinDim ↔ ∃ S : Finset P, affineSpan K (S : Set P) = s := by classical - rw [finiteDimensional_iff_exists_finite_affineSpan] + rw [finDim_iff_exists_finite_affineSpan] exact ⟨fun ⟨S, hS, hspan⟩ ↦ ⟨hS.toFinset, by simpa using hspan⟩, fun ⟨S, hspan⟩ ↦ ⟨S, S.finite_toSet, hspan⟩⟩ /-- The cardinal-valued dimension detects finite-dimensionality, including for `⊥`. -/ -theorem finiteDimensional_iff_dim_lt_aleph0 : +theorem finDim_iff_dim_lt_aleph0 : s.FinDim ↔ s.dim < (Cardinal.aleph0 : WithBot Cardinal) := finite_iff_dim_lt_aleph0 s diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean index 0adeda8f..215cc972 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean @@ -176,7 +176,7 @@ variable {s t : Set A} theorem finDim_univ_iff : FinDim K (Set.univ : Set A) ↔ AffineSpace.FiniteDimensional K A := by rw [finDim_iff_affineSpan, AffineSubspace.span_univ, - AffineSubspace.finiteDimensional_top_iff] + AffineSubspace.finDim_top_iff] @[simp] theorem finDim_union_iff : FinDim K (s ∪ t) ↔ FinDim K s ∧ FinDim K t := by @@ -192,7 +192,7 @@ theorem finDim_union_iff : FinDim K (s ∪ t) ↔ FinDim K s ∧ FinDim K t := b theorem finDim_iff_dim_lt_aleph0 : FinDim K s ↔ (_root_.affineSpan K s).dim < (Cardinal.aleph0 : WithBot Cardinal) := by rw [finDim_iff_affineSpan] - exact AffineSubspace.finiteDimensional_iff_dim_lt_aleph0 + exact AffineSubspace.finDim_iff_dim_lt_aleph0 theorem finDim_iff_rank_lt_aleph0 : FinDim K s ↔ rank K s < Cardinal.aleph0 := by unfold rank @@ -201,11 +201,11 @@ theorem finDim_iff_rank_lt_aleph0 : FinDim K s ↔ rank K s < Cardinal.aleph0 := theorem finDim_iff_exists_finite_affineSpan : FinDim K s ↔ ∃ t : Set A, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s := by - rw [finDim_iff_affineSpan, AffineSubspace.finiteDimensional_iff_exists_finite_affineSpan] + rw [finDim_iff_affineSpan, AffineSubspace.finDim_iff_exists_finite_affineSpan] theorem finDim_iff_exists_finset_affineSpan : FinDim K s ↔ ∃ t : Finset A, _root_.affineSpan K (t : Set A) = _root_.affineSpan K s := by - rw [finDim_iff_affineSpan, AffineSubspace.finiteDimensional_iff_exists_finset_affineSpan] + rw [finDim_iff_affineSpan, AffineSubspace.finDim_iff_exists_finset_affineSpan] namespace FinDim From 52dcf5f2d6220cbb18d791192f88d8d243fbcf28 Mon Sep 17 00:00:00 2001 From: Martin Winter Date: Fri, 2 Oct 2026 12:02:07 +0200 Subject: [PATCH 6/6] Fix --- Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean index 3f1fa72b..32cd9f6a 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean @@ -3,7 +3,7 @@ module public import Polyhedral.Mathlib.Geometry.Convex.AffineMap.Module public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace public import Polyhedral.Mathlib.Geometry.Convex.Hull -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FinDim +public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Set.FiniteDimensional public section