making IsHomogenization a struct

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean

@@ -24,7 +24,7 @@ variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
 variable {V : Type*} [AddCommGroup V] [Module R V]
 variable {A : Type*} [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 variable {W : Type*} [AddCommGroup W] [Module R W] [ConvexSpace R W]
-variable [hom : Affine.IsHomogenization R A W]
+variable {ℋ : Affine.IsHomogenization R A W}
 
 section Module
 
@@ -33,54 +33,55 @@ variable [IsModuleConvexSpace R W]
 /-- If the homogenization of a point lies in the conic hull of a subset `s` of the homogenization
 plane, the point can be written as a convex combination of points in the preimage of `s` under the
 homogenization embedding. -/
-theorem exists_sConvexComb_preimage_of_mem_hull {x} {s : Set W} (hs : s ⊆ Set.range hom.ofPoint)
-    (hx : hom.ofPoint x ∈ hull R s) : ∃ c' : StdSimplex R A,
-      sConvexComb c' = x ∧ (c'.weights.support : Set A) ⊆ (hom.ofPoint ⁻¹' s) := by
+theorem exists_sConvexComb_preimage_of_mem_hull {x} {s : Set W} (hs : s ⊆ Set.range ℋ.ofPoint)
+    (hx : ℋ.ofPoint x ∈ hull R s) : ∃ c' : StdSimplex R A,
+      sConvexComb c' = x ∧ (c'.weights.support : Set A) ⊆ (ℋ.ofPoint ⁻¹' s) := by
   obtain ⟨c, ha, hb, hc⟩ := mem_hull_set.mp hx
   -- use the same weights, just un-embed the domain
-  use StdSimplex.mk (c.comapDomain hom.ofPoint hom.ofPoint_injective.injOn) ?_ ?_
+  use StdSimplex.mk (c.comapDomain ℋ.ofPoint ℋ.ofPoint_injective.injOn) ?_ ?_
   constructor
   · -- the convex combo yields x
-    apply hom.ofPoint_injective
-    rw [hom.ofPoint.isAffineMap.map_sConvexComb, sConvexComb_eq_sum,
-      StdSimplex.weights_map, ← hc, Finsupp.mapDomain_comapDomain _ hom.ofPoint_injective]
+    apply ℋ.ofPoint_injective
+    rw [ℋ.ofPoint.isAffineMap.map_sConvexComb, sConvexComb_eq_sum,
+      StdSimplex.weights_map, ← hc, Finsupp.mapDomain_comapDomain _ ℋ.ofPoint_injective]
     exact ha.trans hs
   · -- the weights are a subset of the preimage of s
     simpa using (Set.preimage_mono ha)
   · -- they're always nonneg
     intro y
-    simpa using hb (hom.ofPoint y)
+    simpa using hb (ℋ.ofPoint y)
   · -- its actually a convex combo, i.e. weights sum to 1
-    have hsum : c.sum (fun a b => b * hom.weight a) = c.sum (fun a b => b) := by
+    have hsum : c.sum (fun a b => b * ℋ.weight a) = c.sum (fun a b => b) := by
         refine Finsupp.sum_congr (fun a h => ?_)
         obtain ⟨_, _, rfl⟩ := (ha.trans hs) h
-        simp [hom.weight_one]
+        simp [ℋ.weight_one]
     -- apply weights map to both sides
-    have := congrArg hom.weight hc
-    simp only [map_finsuppSum, map_smul, smul_eq_mul, hsum, hom.weight_one] at this
+    have := congrArg ℋ.weight hc
+    simp only [map_finsuppSum, map_smul, smul_eq_mul, hsum, ℋ.weight_one] at this
     rw [← this]
     simp only [Finsupp.sum, Finsupp.comapDomain_support, Finsupp.comapDomain_apply]
-    rw [Finset.sum_preimage hom.ofPoint _ (hom.ofPoint_injective.injOn)]
+    rw [Finset.sum_preimage ℋ.ofPoint _ (ℋ.ofPoint_injective.injOn)]
     exact fun _ hx hnx ↦ Finsupp.notMem_support_iff.mp fun _ ↦ hnx (hs (ha hx))
 
 /-- The preimage of the conic hull of a set in the homogenization plane is the convex hull of the
 preimage of the set. -/
-theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range hom.ofPoint) :
-    hom.ofPoint ⁻¹' hull R s = Convexity.convexHull R (hom.ofPoint ⁻¹' s) := by
+theorem preimage_hull_eq_convexHull_preimage {s : Set W} (hs : s ⊆ Set.range ℋ.ofPoint) :
+    ℋ.ofPoint ⁻¹' hull R s = Convexity.convexHull R (ℋ.ofPoint ⁻¹' s) := by
   refine subset_antisymm ?_ ?_
   · intro x hx
     obtain ⟨c', rfl, hs⟩ := exists_sConvexComb_preimage_of_mem_hull hs hx
     exact IsConvexSet.convexHull.sConvexComb_mem (le_trans hs subset_convexHull_self)
   · apply Set.image_subset_iff.mp
-    rw [hom.ofPoint.isAffineMap.image_convexHull, Set.image_preimage_eq_iff.mpr hs]
+    rw [ℋ.ofPoint.isAffineMap.image_convexHull, Set.image_preimage_eq_iff.mpr hs]
     exact (hull R s).isConvexSet.convexHull_subset_iff.mpr subset_hull
 
+variable (hom) in
 /-- The homogenization embedding of the convex hull of a set is contained in the hull of the
 embedding of the set. -/
-theorem preimage_hull_eq_convexHull_preimagke {s : Set A} :
-    hom.ofPoint '' Convexity.convexHull R s ⊆ hull R (hom.ofPoint '' s) := by
+theorem image_hull_eq_convexHull_image {s : Set A} :
+    ℋ.ofPoint '' Convexity.convexHull R s ⊆ hull R (ℋ.ofPoint '' s) := by
   apply Set.image_subset_iff.mp
-  rw [hom.ofPoint.isAffineMap.image_convexHull]
+  rw [ℋ.ofPoint.isAffineMap.image_convexHull]
   simpa using (hull R _).isConvexSet.convexHull_subset_iff.mpr subset_hull
 
 end Module

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean

@@ -32,11 +32,9 @@ include V in
 /-- Faces of polytopes are polytopes. -/
 theorem IsPolytope.face_isPolytope (hC : IsPolytope R (C : Set A)) (hF : IsFaceOf F C) :
     IsPolytope R (F : Set A) := by
-  let W := Homogenization R A
-  let : ConvexSpace R W := ConvexSpace.ofModule
-  have homC := IsPolytope.homogenize_fg (W := W) hC
-  have homF := IsHomogenization.homogenize_isFaceOf (W := W) hF
-  have := PointedCone.IsFaceOf.fg homC homF
+  let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
+  have homF := (IsHomogenization.canonical R A).homogenize_isFaceOf hF
+  have := PointedCone.IsFaceOf.fg (IsPolytope.homogenize_fg _ hC) homF
   convert FG.dehomogenize_isPolytope this (fun _ a b ↦ weight_pos_of_mem_homogenize a b)
   simp [dehomogenize_homogenize]
 
@@ -52,13 +50,12 @@ This is private since it does not yet have the correct grading (off-by-one).
 -/
 private noncomputable instance Polytope.faceHomogenizationGradeOrder (P : Polytope R A) :
     GradeOrder ℕ (Face (P : ConvexSet R A)) := by
-  let W := Homogenization R A
-  letI : ConvexSpace R W := ConvexSpace.ofModule
-  have : PointedCone.FG (homogenize W (P : ConvexSet R A)) :=
-    IsPolytope.homogenize_fg (W := W) P.isPolytope
+  let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
+  have : PointedCone.FG (homogenize _ (P : ConvexSet R A)) :=
+    IsPolytope.homogenize_fg (IsHomogenization.canonical R A) P.isPolytope
   let := PointedCone.FG.gradeOrder_finrank this
-  refine GradeOrder.liftRight (β := (homogenize W (P : ConvexSet R A)).Face) _
-    IsHomogenization.Face.homogenizeIso.strictMono ?_
+  refine GradeOrder.liftRight _
+    (IsHomogenization.Face.homogenizeIso (IsHomogenization.canonical R A) _).strictMono ?_
   exact fun x y ↦ (apply_covBy_apply_iff _).mpr
 
 end Field

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Homogenization.lean

@@ -28,46 +28,46 @@ variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
 variable [IsModuleConvexSpace R W]
 
-variable [hom : IsHomogenization R A W]
+variable (ℋ : IsHomogenization R A W)
 
 open PointedCone
 
 /-- The homogenization of a polytope is a finitely generated cone. -/
 theorem IsPolytope.homogenize_fg {C : ConvexSet R A} (hCfg : IsPolytope R (C : Set A)) :
-    (homogenize W C).FG := by
+    (homogenize ℋ C).FG := by
   obtain ⟨t, ht⟩ := hCfg
   have : C = ⟨convexHull R t, IsConvexSet.convexHull⟩ := SetLike.ext' ht
-  have := congrArg (ConvexSet.homogenize W) this
+  have := congrArg (ConvexSet.homogenize ℋ) this
   rw [this]
-  use t.map ⟨_, hom.ofPoint_injective⟩
+  use t.map ⟨_, ℋ.ofPoint_injective⟩
   simp only [Finset.coe_map, Function.Embedding.coeFn_mk, homogenize,
     PointedCone.hull, ConvexSet.mk_eq]
-  rw [hom.ofPoint.isAffineMap.image_convexHull t]
-  exact (PointedCone.hull_convexHull (hom.ofPoint '' t)).symm
+  rw [ℋ.ofPoint.isAffineMap.image_convexHull t]
+  exact (PointedCone.hull_convexHull (ℋ.ofPoint '' t)).symm
 
 /-- A convex set is a polytope iff its homogenization is a finitely generated cone. -/
 theorem IsPolytope.iff_homogenize_fg {C : ConvexSet R A} :
-    IsPolytope R (C : Set A) ↔ (homogenize W C).FG := by classical
-  refine ⟨homogenize_fg, fun hfg ↦ ?_⟩
+    IsPolytope R (C : Set A) ↔ (homogenize ℋ C).FG := by classical
+  refine ⟨homogenize_fg _, fun hfg ↦ ?_⟩
   -- get cone generators that lie in the embedding of A
   obtain ⟨g, hg, hs⟩ := homogenize_fg_ofPoint_range hfg
   -- un-embed them
-  use g.preimage hom.ofPoint hom.ofPoint_injective.injOn
+  use g.preimage ℋ.ofPoint ℋ.ofPoint_injective.injOn
   -- show they generate C
   simp only [Finset.coe_preimage]
   apply le_antisymm
   · intro x hx
     rw [← preimage_hull_eq_convexHull_preimage hs]
     simp only [hg, homogenize]
-    exact Submodule.mem_span_of_mem <| Set.mem_image_of_mem hom.ofPoint hx
+    exact Submodule.mem_span_of_mem <| Set.mem_image_of_mem ℋ.ofPoint hx
   · apply C.isConvexSet.convexHull_subset_iff.mpr
     intro x hx
     simp only [Set.mem_preimage, SetLike.mem_coe] at hx
     have := Set.mem_preimage.mpr <| Submodule.mem_span_of_mem (R := {c : R // 0 ≤ c}) hx
     simp_rw [hg, homogenize] at this
-    rw [preimage_hull_eq_convexHull_preimage (Set.image_subset_range hom.ofPoint C)] at this
+    rw [preimage_hull_eq_convexHull_preimage (Set.image_subset_range ℋ.ofPoint C)] at this
     rw [← C.isConvexSet.convexHull_eq_self]
-    simpa [← C.isConvexSet.convexHull_eq_self, Set.preimage_image_eq _ hom.ofPoint_injective]
+    simpa [← C.isConvexSet.convexHull_eq_self, Set.preimage_image_eq _ ℋ.ofPoint_injective]
 
 end Ring
 
@@ -80,13 +80,13 @@ variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
 variable [IsModuleConvexSpace R W]
 
-variable [hom : IsHomogenization R A W]
+variable {ℋ : IsHomogenization R A W}
 
 open Pointwise Submodule in
 /-- Dehomogenizing a finitely generated positive cone yields a polytope. -/
 theorem FG.dehomogenize_isPolytope {C : PointedCone R W} (h : C.FG)
-    (hc : C ≤ hom.weight.positive) : IsPolytope R (dehomogenize A C : Set A) := by
-  rw [IsPolytope.iff_homogenize_fg (W := W)]
+    (hc : C ≤ ℋ.weight.positive) : IsPolytope R (dehomogenize ℋ C : Set A) := by
+  rw [IsPolytope.iff_homogenize_fg ℋ]
   simpa [homogenize_dehomogenize_of_le_positive hc]
 
 end Field

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean

@@ -28,33 +28,34 @@ variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
 variable [IsModuleConvexSpace R W]
 
-variable [hom : Affine.IsHomogenization R A W]
+variable (ℋ : Affine.IsHomogenization R A W)
 
+variable {ℋ} in
 /-- If the homogenization of a point `q` is a positive combination of the homogenization
 of two other points, then `q` lies in the open segment between them. -/
 theorem pos_combo_openSegment {r₁ r₂ t : R} {p₁ p₂ q : A}
     (h₁ : 0 < r₁) (h₂ : 0 < r₂) (hₜ : 0 < t)
-    (h : r₁ • hom.ofPoint p₁ + r₂ • hom.ofPoint p₂ = t • hom.ofPoint q) :
+    (h : r₁ • ℋ.ofPoint p₁ + r₂ • ℋ.ofPoint p₂ = t • ℋ.ofPoint q) :
       q ∈ Convexity.openSegment R p₁ p₂ := by
-  have : r₁ + r₂ = t := by simpa [hom.weight_one, map_add, map_smul] using congr_arg hom.weight h
+  have : r₁ + r₂ = t := by simpa [ℋ.weight_one, map_add, map_smul] using congr_arg ℋ.weight h
   have : t⁻¹ • r₁ + t⁻¹ • r₂ = 1 := by
       simp_rw [← smul_add, smul_eq_mul, this, mul_comm, Field.mul_inv_cancel _ hₜ.ne.symm]
   use (t⁻¹ • r₁), (t⁻¹ • r₂), (smul_pos (by positivity) h₁), (smul_pos (by positivity) h₂), this
-  apply hom.ofPoint_injective
-  have : t⁻¹ • (r₁ • hom.ofPoint p₁ + r₂ • hom.ofPoint p₂) = hom.ofPoint q := by
+  apply ℋ.ofPoint_injective
+  have : t⁻¹ • (r₁ • ℋ.ofPoint p₁ + r₂ • ℋ.ofPoint p₂) = ℋ.ofPoint q := by
     rw [h, smul_smul, inv_mul_cancel₀ (ne_of_gt hₜ), one_smul]
-  simp [hom.ofPoint.isAffineMap.map_convexCombPair, convexCombPair_eq_sum, ← this, smul_smul]
+  simp [ℋ.ofPoint.isAffineMap.map_convexCombPair, convexCombPair_eq_sum, ← this, smul_smul]
 
 /-- If `F` is a face of `P`, then the homogenization of `F` is a face of the homogenization
 of `P`. -/
 theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) :
-    (F.homogenize W).IsFaceOf (P.homogenize W) where
-  le := homogenizeOrderHom.monotone' he.le
+    (F.homogenize ℋ).IsFaceOf (P.homogenize ℋ) where
+  le := (homogenizeOrderHom ℋ).monotone' he.le
   mem_of_smul_add_mem := by
     intro v w a hv hw ha hvw
-    have hhom : (P.homogenize W).Salient := homogenize_salient
+    have hhom := homogenize_salient ℋ P
     by_cases hnf : (F : Set A).Nonempty
-    · have cF := F.isConvexSet.image hom.ofPoint.isAffineMap
+    · have cF := F.isConvexSet.image ℋ.ofPoint.isAffineMap
       apply (Set.ext_iff.mp (PointedCone.hull_eq_smul (hnf.image _) cF) _).mpr
       by_cases hv0 : v = 0
       · exact ⟨0, le_rfl, mem_smul_set.mpr (by simpa [hv0] using nonempty_def.mp hnf)⟩
@@ -70,13 +71,13 @@ theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) :
           rw [smul_assoc, hra, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ ha.ne.symm, one_smul]
         · obtain ⟨rw, rw0, q, ⟨q', qq, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hw hw0
           obtain ⟨rv, rv0, _, ⟨p', pp, rfl⟩, _, _⟩ := smul_pos_of_mem_homogenize hv hv0
-          have : a • (rv • hom.ofPoint p') + (rw • hom.ofPoint q') ≠ 0 := by
+          have : a • (rv • ℋ.ofPoint p') + (rw • ℋ.ofPoint q') ≠ 0 := by
             intro hc
-            exact (smul_ne_zero rw0.ne.symm (ofPoint_ne_zero q')) <|
+            exact (smul_ne_zero rw0.ne.symm (ℋ.ofPoint_ne_zero q')) <|
               hhom _ hw _ (PointedCone.smul_mem _ ha.le hv) (by simpa [add_comm] using hc)
           obtain ⟨_, rvw0, _, ⟨_, qqp, rfl⟩, pdp⟩ := smul_pos_of_mem_homogenize hvw this
           have := he.left_mem_of_mem_openSegment pp qq qqp ?_
-          · refine ⟨rv, rv0.le, smul_mem_smul_set <| mem_image_of_mem ofPoint this⟩
+          · refine ⟨rv, rv0.le, smul_mem_smul_set <| mem_image_of_mem ℋ.ofPoint this⟩
           rw [← smul_assoc _ rv] at pdp
           exact pos_combo_openSegment (smul_pos ha rv0) rw0 rvw0 pdp.symm
     · have := not_nonempty_iff_eq_empty.mp hnf
@@ -89,34 +90,33 @@ theorem homogenize_isFaceOf {F P : ConvexSet R A} (he : F.IsFaceOf P) :
         rw [this]
         exact PointedCone.smul_mem _ (by positivity) hw) (add_neg_cancel v)
 
-variable (A) in
 /-- If `F` is a face of `C`, then the dehomogenization of `F` is a face of the dehomogenization
 of `C`. -/
 theorem dehomogenize_isFaceOf {F C : PointedCone R W} (hf : F.IsFaceOf C) :
-    (ConvexSet.dehomogenize A F).IsFaceOf (ConvexSet.dehomogenize A C) where
+    (ConvexSet.dehomogenize ℋ F).IsFaceOf (ConvexSet.dehomogenize ℋ C) where
   le := preimage_mono (fun _ x ↦ hf.le x)
   left_mem_of_mem_openSegment  := by
     rintro x hx y hy z hz ⟨a, b, ha, hb, hab, hzo⟩
     refine hf.mem_of_smul_add_mem hx (C.smul_mem hb.le hy) ha ?_
     rwa [← convexCombPair_eq_sum _ _ ha.le hb.le hab,
-      ← hom.ofPoint.isAffineMap.map_convexCombPair, hzo]
+      ← ℋ.ofPoint.isAffineMap.map_convexCombPair, hzo]
 
 /-- The isomorphism between the face lattice of a convex set `P` and the face lattice of
 its homogenization cone.
 
 This isomorphism is used to translate results between face lattices of cones and face lattices
 of convex sets.
 -/
-def Face.homogenizeIso {P : ConvexSet R A} :
-    Face P ≃o PointedCone.Face (P.homogenize W) where
-  toFun F := ⟨_, hom.homogenize_isFaceOf F.isFaceOf⟩
-  invFun F := ⟨dehomogenize A F.toSubmodule,
-    by simpa [dehomogenize_homogenize] using dehomogenize_isFaceOf A F.isFaceOf⟩
+def Face.homogenizeIso (P : ConvexSet R A) :
+    Face P ≃o PointedCone.Face (P.homogenize ℋ) where
+  toFun F := ⟨_, ℋ.homogenize_isFaceOf F.isFaceOf⟩
+  invFun F := ⟨dehomogenize ℋ F.toSubmodule,
+    by simpa [dehomogenize_homogenize ℋ] using dehomogenize_isFaceOf ℋ F.isFaceOf⟩
   map_rel_iff' := by
     intro a b
     refine ⟨fun h x xm ↦ ?_, fun h _ xm ↦ span_mono (image_mono h) xm⟩
-    refine (ofPoint_mem_homogenize_iff_mem W x b.toConvexSet).mp (h ?_)
-    exact (ofPoint_mem_homogenize_iff_mem W x a.toConvexSet).mpr xm
+    refine (ofPoint_mem_homogenize_iff_mem _ x b.toConvexSet).mp (h ?_)
+    exact (ofPoint_mem_homogenize_iff_mem _ x a.toConvexSet).mpr xm
   left_inv _ := by simp [dehomogenize_homogenize]
   right_inv F := by
     have := homogenize_dehomogenize_of_le_positive