From f463ad79dfc26c1b3b52de6bbf51d5916b7e955f Mon Sep 17 00:00:00 2001 From: ovi Date: Fri, 15 May 2026 20:28:30 +0200 Subject: [PATCH 1/7] showing an `AffineMap` `isAffineMap` --- .../Convex/ConvexSpace/AffineSpace.lean | 22 +++++++++++++++++++ Mathlib/Geometry/Convex/ConvexSpace/Defs.lean | 4 +--- 2 files changed, 23 insertions(+), 3 deletions(-) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index 4aa7fe0ea4531c..a93400db5cf0f8 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -152,6 +152,28 @@ theorem convexCombPair_eq_lineMap (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) end AddTorsor +open Finset AddTorsor in +variable {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] in +lemma AffineMap.isAffineMap (f : P →ᵃ[R] P2) : IsAffineMap R f where + map_sConvexComb s:= by + classical + simp_rw [sConvexComb_eq_affineCombination, StdSimplex.weights_map, Finsupp.mapDomain, + map_affineCombination _ _ _ s.total, Finsupp.sum, Finsupp.coe_finsetSum] + simp only [affineCombination_apply, weightedVSubOfPoint_apply, map_sum] + congr + ext i + rw [sum_eq_single (f i) fun _ _ hx ↦ by simp [hx.symm]] + · simp + · intro h + simp only [Finsupp.mem_support_iff, Finsupp.coe_finsetSum, sum_apply, + Decidable.not_not, Finsupp.single_apply] at h + have hwi : s.weights i = 0 := by + by_contra hi + convert (sum_eq_zero_iff_of_nonneg (fun _ _ ↦ ?_)).mp h i (Finsupp.mem_support_iff.mpr hi) + · simpa + · split_ifs <;> simp + simp [hwi] + open Finsupp namespace Convexity diff --git a/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean b/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean index 31f09b28713966..3dd6b26c4948ea 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean @@ -259,9 +259,7 @@ abbrev ConvexSpace.mk {M : Type*} (sConvexComb : StdSimplex R M → M) ⟨sConvexComb, single, assoc⟩ variable (R) in -/-- A map between convex spaces is affine if it preserves convex combinations. - -TODO: Show that this generalises affine maps between affine spaces, see `AffineMap`. -/ +/-- A map between convex spaces is affine if it preserves convex combinations. -/ @[fun_prop] structure IsAffineMap (f : M → N) : Prop where map_sConvexComb (s : StdSimplex R M) : f s.sConvexComb = (s.map f).sConvexComb From cbb97dd69774978e1eaae8fe4052ce3d720f972d Mon Sep 17 00:00:00 2001 From: ovi Date: Fri, 15 May 2026 23:46:59 +0200 Subject: [PATCH 2/7] cosmetics --- Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index a93400db5cf0f8..d8691291a012f1 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -153,8 +153,8 @@ theorem convexCombPair_eq_lineMap (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) end AddTorsor open Finset AddTorsor in -variable {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] in -lemma AffineMap.isAffineMap (f : P →ᵃ[R] P2) : IsAffineMap R f where +lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] + (f : P →ᵃ[R] P2) : IsAffineMap R f where map_sConvexComb s:= by classical simp_rw [sConvexComb_eq_affineCombination, StdSimplex.weights_map, Finsupp.mapDomain, @@ -169,8 +169,9 @@ lemma AffineMap.isAffineMap (f : P →ᵃ[R] P2) : IsAffineMap R f where Decidable.not_not, Finsupp.single_apply] at h have hwi : s.weights i = 0 := by by_contra hi - convert (sum_eq_zero_iff_of_nonneg (fun _ _ ↦ ?_)).mp h i (Finsupp.mem_support_iff.mpr hi) - · simpa + have := sum_eq_zero_iff_of_nonneg (fun _ _ ↦ ?_) |>.mp h i (Finsupp.mem_support_iff.mpr hi) + · simp at this + contradiction · split_ifs <;> simp simp [hwi] From 2481dd51cd177941685e85096b4097b2c8643a2d Mon Sep 17 00:00:00 2001 From: ooovi <79147175+ooovi@users.noreply.github.com> Date: Thu, 21 May 2026 15:51:25 +0200 Subject: [PATCH 3/7] nit --- Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index d25ece173792c4..970a675bd607ea 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -182,4 +182,4 @@ lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [Aff · split_ifs <;> simp simp [hwi] -end \ No newline at end of file +end From 665c26e4dfffe8fe98fdb15a0922d4dd523970a7 Mon Sep 17 00:00:00 2001 From: ovi Date: Thu, 21 May 2026 16:16:05 +0200 Subject: [PATCH 4/7] fixing uninstantiation trouble --- Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index 970a675bd607ea..3d9448878a87ef 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -159,6 +159,10 @@ theorem convexCombPair_eq_lineMap (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) end AddTorsor +section + +local instance : ConvexSpace R P := AddTorsor.toConvexSpace + open Finset AddTorsor in lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] (f : P →ᵃ[R] P2) : IsAffineMap R f where @@ -183,3 +187,5 @@ lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [Aff simp [hwi] end + +end From c2d72269cc8690d2e36f84599c288dffbd9ca0d6 Mon Sep 17 00:00:00 2001 From: ovi Date: Fri, 22 May 2026 09:00:54 +0200 Subject: [PATCH 5/7] fix linter --- Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index 3d9448878a87ef..a2b25d6220f273 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -161,10 +161,12 @@ end AddTorsor section -local instance : ConvexSpace R P := AddTorsor.toConvexSpace +namespace AffineMap + +attribute [local instance] AddTorsor.toConvexSpace open Finset AddTorsor in -lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] +lemma isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] (f : P →ᵃ[R] P2) : IsAffineMap R f where map_sConvexComb s:= by classical @@ -186,6 +188,6 @@ lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [Aff · split_ifs <;> simp simp [hwi] -end +end AffineMap end From 9bb82b58ef6063fe17c876fd8981167fb071b9e9 Mon Sep 17 00:00:00 2001 From: ooovi <79147175+ooovi@users.noreply.github.com> Date: Thu, 4 Jun 2026 11:28:46 +0200 Subject: [PATCH 6/7] Update Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean Co-authored-by: Paul Lezeau --- .../Convex/ConvexSpace/AffineSpace.lean | 38 +++++++++---------- 1 file changed, 17 insertions(+), 21 deletions(-) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index a2b25d6220f273..c70ce82986b793 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -166,27 +166,23 @@ namespace AffineMap attribute [local instance] AddTorsor.toConvexSpace open Finset AddTorsor in -lemma isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] - (f : P →ᵃ[R] P2) : IsAffineMap R f where - map_sConvexComb s:= by - classical - simp_rw [sConvexComb_eq_affineCombination, StdSimplex.weights_map, Finsupp.mapDomain, - map_affineCombination _ _ _ s.total, Finsupp.sum, Finsupp.coe_finsetSum] - simp only [affineCombination_apply, weightedVSubOfPoint_apply, map_sum] - congr - ext i - rw [sum_eq_single (f i) fun _ _ hx ↦ by simp [hx.symm]] - · simp - · intro h - simp only [Finsupp.mem_support_iff, Finsupp.coe_finsetSum, sum_apply, - Decidable.not_not, Finsupp.single_apply] at h - have hwi : s.weights i = 0 := by - by_contra hi - have := sum_eq_zero_iff_of_nonneg (fun _ _ ↦ ?_) |>.mp h i (Finsupp.mem_support_iff.mpr hi) - · simp at this - contradiction - · split_ifs <;> simp - simp [hwi] +lemma isAffineMap_of_preserves_convex_combinations + {k : Type u_1} {V P V₂ P₂ : Type*} [PartialOrder k] [Ring k] [IsStrictOrderedRing k] + [AddCommGroup V] [Module k V] [S : AffineSpace V P] + [AddCommGroup V₂] [Module k V₂] [AffineSpace V₂ P₂] (f : P → P₂) + (H : ∀ {ι : Type u_6} (s : Finset ι) (p : ι → P) (w : ι → k), + ∑ i ∈ s, w i = 1 → + f ((affineCombination k s p) w) = (affineCombination k s (f ∘ p)) w) : + IsAffineMap k f where + map_sConvexComb s := by + rw [sConvexComb_eq_affineCombination, H s.weights.support _root_.id s.weights s.total, + ←iConvexComb_eq_affineCombination, Function.comp_id, iConvexComb] + +open Finset AddTorsor in +lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] + (f : P →ᵃ[R] P2) : IsAffineMap R f := by + apply isAffineMap_of_preserves_convex_combinations + grind [map_affineCombination] end AffineMap From 8fb418e8689f0eebfceeb863d864acb0400dd487 Mon Sep 17 00:00:00 2001 From: ovi Date: Thu, 4 Jun 2026 11:34:14 +0200 Subject: [PATCH 7/7] naming --- Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index c70ce82986b793..70560595164605 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -163,10 +163,11 @@ section namespace AffineMap +open Finset AddTorsor + attribute [local instance] AddTorsor.toConvexSpace -open Finset AddTorsor in -lemma isAffineMap_of_preserves_convex_combinations +lemma of_apply_affineCombination {k : Type u_1} {V P V₂ P₂ : Type*} [PartialOrder k] [Ring k] [IsStrictOrderedRing k] [AddCommGroup V] [Module k V] [S : AffineSpace V P] [AddCommGroup V₂] [Module k V₂] [AffineSpace V₂ P₂] (f : P → P₂) @@ -178,10 +179,9 @@ lemma isAffineMap_of_preserves_convex_combinations rw [sConvexComb_eq_affineCombination, H s.weights.support _root_.id s.weights s.total, ←iConvexComb_eq_affineCombination, Function.comp_id, iConvexComb] -open Finset AddTorsor in -lemma AffineMap.isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] +lemma isAffineMap {V2 P2 : Type*} [AddCommGroup V2] [Module R V2] [AffineSpace V2 P2] (f : P →ᵃ[R] P2) : IsAffineMap R f := by - apply isAffineMap_of_preserves_convex_combinations + apply of_apply_affineCombination grind [map_affineCombination] end AffineMap