feat(Geometry/Convex/Cone): Rename PointedCone.span to PointedCone.hull (leanprover-community#36953)

Rename `PointedCone.span` to `PointedCone.hull`. Also adjusting cone lemma names and doc-strings.

This PR is the outcome of the discussion here: [#mathlib4 > Design for positive cones @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Design.20for.20positive.20cones/near/580814590)

Co-authored-by: Martin Winter <martin.winter.math@gmail.com>

Author: martinwintermath

Mathlib/Geometry/Convex/Cone/Dual.lean

@@ -103,16 +103,19 @@ variable (s) in
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma dual_span (s : Set M) : dual p (span R s) = dual p s := by
+lemma dual_hull (s : Set M) : dual p (hull R s) = dual p s := by
   refine le_antisymm (dual_anti Submodule.subset_span) (fun x hx y hy => ?_)
   induction hy using Submodule.span_induction with
   | mem _y h => exact hx h
   | zero => simp
   | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
   | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
 
+@[deprecated "`PointedCone.span` was renamed to `PointedCone.hull`" (since := "2026-03-22")]
+alias dual_span := dual_hull
+
 @[simp] lemma dual_sup (C D : PointedCone R M) : dual p (C ⊔ D : PointedCone R M) = dual p (C ∪ D)
-  := by simp [← dual_span]
+  := by simp [← dual_hull]
 
 variable {M' : Type*} [AddCommGroup M'] [Module R M']
 

Mathlib/Geometry/Convex/Cone/Pointed.lean

@@ -55,25 +55,25 @@ lemma mem_ofSubmodule_iff {S : Submodule R E} {x : E} : x ∈ (S : PointedCone R
 
 set_option backward.isDefEq.respectTransparency false in
 lemma ofSubmodule_inj {S T : Submodule R E} : ofSubmodule S = ofSubmodule T ↔ S = T :=
-  Submodule.restrictScalars_inj ..
+  restrictScalars_inj ..
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Coercion from submodules to pointed cones as an order embedding. -/
 abbrev ofSubmoduleEmbedding : Submodule R E ↪o PointedCone R E :=
-  Submodule.restrictScalarsEmbedding ..
+  restrictScalarsEmbedding ..
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Coercion from submodules to pointed cones as a lattice homomorphism. -/
 abbrev ofSubmoduleLatticeHom : CompleteLatticeHom (Submodule R E) (PointedCone R E) :=
-  Submodule.restrictScalarsLatticeHom ..
+  restrictScalarsLatticeHom ..
 
 set_option backward.isDefEq.respectTransparency false in
 lemma ofSubmodule_inf (S T : Submodule R E) : S ⊓ T = (S ⊓ T : PointedCone R E) :=
-  Submodule.restrictScalars_inf _ _ _
+  restrictScalars_inf _ _ _
 
 set_option backward.isDefEq.respectTransparency false in
 lemma ofSubmodule_sup (S T : Submodule R E) : S ⊔ T = (S ⊔ T : PointedCone R E) :=
-  Submodule.restrictScalars_sup _ _ _
+  restrictScalars_sup _ _ _
 
 lemma ofSubmodule_sInf (s : Set (Submodule R E)) : sInf s = sInf (ofSubmodule '' s) :=
   ofSubmoduleLatticeHom.map_sInf' s
@@ -170,24 +170,30 @@ def ofConeComb (C : Set E) (nonempty : C.Nonempty)
   .ofLinearComb C nonempty fun x hx y hy ⟨a, ha⟩ ⟨b, hb⟩ => coneComb x hx y hy a ha b hb
 
 variable (R) in
-/-- The span of a set `s` is the smallest pointed cone that contains `s`.
+/-- The cone hull of a set `s` is the smallest pointed cone that contains `s`.
 
-Pointed cones being defined as submodules over nonnegative scalars, this is exactly the
-submodule span of `s` w.r.t. nonnegative scalars. -/
-abbrev span (s : Set E) : PointedCone R E := Submodule.span R≥0 s
+Pointed cones being defined as submodules over nonnegative scalars, this is implemented as
+the submodule span of `s` w.r.t. nonnegative scalars. -/
+abbrev hull (s : Set E) : PointedCone R E := span R≥0 s
 
-lemma subset_span {s : Set E} : s ⊆ PointedCone.span R s := Submodule.subset_span
+lemma subset_hull {s : Set E} : s ⊆ PointedCone.hull R s := subset_span
+
+@[deprecated "`PointedCone.span` was renamed to `PointedCone.hull`" (since := "2026-03-22")]
+alias subset_span := subset_hull
 
 /-- Elements of the cone hull are expressible as conical combination of elements from s. -/
-lemma mem_span_set {s : Set E} : x ∈ span R s ↔
+lemma mem_hull_set {s : Set E} : x ∈ hull R s ↔
       ∃ c : E →₀ R, ↑c.support ⊆ s ∧ (∀ y, 0 ≤ c y) ∧ c.sum (fun m r => r • m) = x := by
-  rw [Submodule.mem_span_set]
+  rw [mem_span_set]
   constructor
   · rintro ⟨c, hc, rfl⟩
     exact ⟨⟨c.support, Subtype.val ∘ c, by simp [← Subtype.val_inj]⟩, hc, fun y ↦ (c y).2, rfl⟩
   · rintro ⟨c, hc, hc₀, rfl⟩
     exact ⟨⟨c.support, fun y ↦ ⟨c y, hc₀ _⟩, by simp⟩, hc, rfl⟩
 
+@[deprecated "`PointedCone.span` was renamed to `PointedCone.hull`" (since := "2026-03-22")]
+alias mem_span_set := mem_hull_set
+
 end Definitions
 
 section Maps

Mathlib/Geometry/Convex/Cone/Simplicial.lean

@@ -10,18 +10,18 @@ public import Mathlib.Geometry.Convex.Cone.Pointed
 /-!
 # Simplicial cones
 
-A **simplicial cone** is a pointed convex cone that equals the conic span of a finite linearly
+A **simplicial cone** is a pointed convex cone that equals the conic hull of a finite linearly
 independent set of vectors. We do not require that the generators span the ambient module.
 However, when the cone is also generating, its generators linearly span the module.
 
 ## Main definitions
 
-* `PointedCone.IsSimplicial`: A pointed cone is simplicial if it equals the conic span of a finite
+* `PointedCone.IsSimplicial`: A pointed cone is simplicial if it equals the conic hull of a finite
   linearly independent set.
 
 ## Results
 
-* `PointedCone.IsSimplicial.span`: The conic span of a linearly independent finite set is
+* `PointedCone.IsSimplicial.span`: The conic hull of a linearly independent finite set is
   simplicial.
 
 ## References
@@ -38,16 +38,16 @@ variable (C : PointedCone R M)
 
 namespace PointedCone
 
-/-- A pointed cone is simplicial if it equals the conic span of a finite set that is linearly
+/-- A pointed cone is simplicial if it equals the conic hull of a finite set that is linearly
 independent over `R`. -/
 def IsSimplicial : Prop :=
-  ∃ s : Set M, s.Finite ∧ LinearIndepOn R id s ∧ span R s = C
+  ∃ s : Set M, s.Finite ∧ LinearIndepOn R id s ∧ hull R s = C
 
 namespace IsSimplicial
 
-/-- The conic span of a finite linearly independent set is simplicial. -/
-protected theorem span {s : Set M} (hs : s.Finite) (hli : LinearIndepOn R id s) :
-    (PointedCone.span R s).IsSimplicial := ⟨s, hs, hli, rfl⟩
+/-- The conic hull of a finite linearly independent set is simplicial. -/
+protected theorem hull {s : Set M} (hs : s.Finite) (hli : LinearIndepOn R id s) :
+    (PointedCone.hull R s).IsSimplicial := ⟨s, hs, hli, rfl⟩
 
 end IsSimplicial
 

Mathlib/Geometry/Convex/Cone/TensorProduct.lean

@@ -58,7 +58,7 @@ namespace PointedCone
 tensor products `x ⊗ₜ y` with `x ∈ C₁` and `y ∈ C₂`. -/
 noncomputable def minTensorProduct (C₁ : PointedCone R G) (C₂ : PointedCone R H) :
     PointedCone R (G ⊗[R] H) :=
-  .span R (.image2 (· ⊗ₜ[R] ·) C₁ C₂)
+  .hull R (.image2 (· ⊗ₜ[R] ·) C₁ C₂)
 
 /-- The maximal tensor product of two cones is the dual (pointed cone) of the minimal tensor product
 of the dual cones. -/
@@ -75,7 +75,7 @@ theorem mem_maxTensorProduct {C₁ : PointedCone R G} {C₂ : PointedCone R H} {
       ∀ φ ∈ PointedCone.dual (dualPairing R G).flip C₁,
       ∀ ψ ∈ PointedCone.dual (dualPairing R H).flip C₂,
       0 ≤ dualDistrib R G H (φ ⊗ₜ[R] ψ) z := by
-  simp only [maxTensorProduct, minTensorProduct, dual_span, mem_dual, Set.forall_mem_image2,
+  simp only [maxTensorProduct, minTensorProduct, dual_hull, mem_dual, Set.forall_mem_image2,
     SetLike.mem_coe, mem_dual, LinearMap.flip_apply, dualPairing_apply]
 
 /-- Elementary tensors are members of the maximal tensor product. -/
@@ -110,7 +110,7 @@ variable {C₁ C₁' : PointedCone R G} {C₂ C₂' : PointedCone R H} {z : G 
 @[simp]
 theorem minTensorProduct_comm :
     (minTensorProduct C₁ C₂).map (TensorProduct.comm R G H) = minTensorProduct C₂ C₁ := by
-  simp [minTensorProduct, map, span, Submodule.map_span, Set.image_image2,
+  simp [minTensorProduct, map, hull, Submodule.map_span, Set.image_image2,
     Set.image2_swap (· ⊗ₜ[R] · : H → G → _)]
 
 /-- The maximal tensor product is commutative. -/