Simplex in affine space

This file defines n-dimensional simplices in affine space.

Main definitions

• Simplex is a bundled type with collection of n + 1 points in affine space that are affinely independent, where n is the dimension of the simplex.

• Triangle is a simplex with three points, defined as an abbreviation for simplex with n = 2.

• face is a simplex with a subset of the points of the original simplex.

References

• https://en.wikipedia.org/wiki/Simplex

structure Affine.Simplex (k : Type u_1) {V : Type u_2} (P : Type u_5) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (n : ℕ) : Type u_5

A Simplex k P n is a collection of n + 1 affinely independent points.

• points : Fin (n + 1) → P
• independent : AffineIndependent k self.points

@[reducible, inline]

abbrev Affine.Triangle (k : Type u_1) {V : Type u_2} (P : Type u_5) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] : Type u_5

A Triangle k P is a collection of three affinely independent points.

Equations

• Affine.Triangle k P = Affine.Simplex k P 2

def Affine.Simplex.mkOfPoint (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) : Simplex k P 0

Construct a 0-simplex from a point.

Equations

• Affine.Simplex.mkOfPoint k p = { points := fun (x : Fin (0 + 1)) => p, independent := ⋯ }

@[simp]

theorem Affine.Simplex.mkOfPoint_points (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (i : Fin 1) : (mkOfPoint k p).points i = p

The point in a simplex constructed with mkOfPoint.

instance Affine.Simplex.instInhabitedOfNatNat (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Inhabited P] : Inhabited (Simplex k P 0)

Equations

• Affine.Simplex.instInhabitedOfNatNat k = { default := Affine.Simplex.mkOfPoint k default }

instance Affine.Simplex.nonempty (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] : Nonempty (Simplex k P 0)

theorem Affine.Simplex.ext {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s1 s2 : Simplex k P n} (h : ∀ (i : Fin (n + 1)), s1.points i = s2.points i) : s1 = s2

Two simplices are equal if they have the same points.

theorem Affine.Simplex.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s1 s2 : Simplex k P n} : s1 = s2 ↔ ∀ (i : Fin (n + 1)), s1.points i = s2.points i

Two simplices are equal if and only if they have the same points.

def Affine.Simplex.face {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : Simplex k P m

A face of a simplex is a simplex with the given subset of points.

Equations

• s.face h = { points := s.points ∘ ⇑(fs.orderEmbOfFin h), independent := ⋯ }

theorem Affine.Simplex.face_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) (i : Fin (m + 1)) : (s.face h).points i = s.points ((fs.orderEmbOfFin h) i)

The points of a face of a simplex are given by mono_of_fin.

theorem Affine.Simplex.face_points' {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : (s.face h).points = s.points ∘ ⇑(fs.orderEmbOfFin h)

The points of a face of a simplex are given by mono_of_fin.

@[simp]

theorem Affine.Simplex.face_eq_mkOfPoint {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) : s.face ⋯ = mkOfPoint k (s.points i)

A single-point face equals the 0-simplex constructed with mkOfPoint.

@[simp]

theorem Affine.Simplex.range_face_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : Set.range (s.face h).points = s.points '' ↑fs

The set of points of a face.

def Affine.Simplex.faceOpposite {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Simplex k P (n - 1)

The face of a simplex with all but one point.

Equations

• s.faceOpposite i = s.face ⋯

@[simp]

theorem Affine.Simplex.range_faceOpposite_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Set.range (s.faceOpposite i).points = s.points '' {i}ᶜ

theorem Affine.Simplex.faceOpposite_point_eq_point_succAbove {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) (j : Fin (n - 1 + 1)) : (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))

theorem Affine.Simplex.faceOpposite_point_eq_point_rev {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 1) (i : Fin 2) (n : Fin 1) : (s.faceOpposite i).points n = s.points i.rev

@[simp]

theorem Affine.Simplex.faceOpposite_point_eq_point_one {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 1) (n : Fin 1) : (s.faceOpposite 0).points n = s.points 1

@[simp]

theorem Affine.Simplex.faceOpposite_point_eq_point_zero {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 1) (n : Fin 1) : (s.faceOpposite 1).points n = s.points 0

instance Affine.Simplex.instNonemptyElemComplSetSingletonOfNontrivial {α : Type u_8} [Nontrivial α] (i : α) : Nonempty ↑{i}ᶜ

Needed to make affineSpan (s.points '' {i}ᶜ) nonempty.

@[simp]

theorem Affine.Simplex.mem_affineSpan_image_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Set (Fin (n + 1))} {i : Fin (n + 1)} : s.points i ∈ affineSpan k (s.points '' fs) ↔ i ∈ fs

@[deprecated Affine.Simplex.mem_affineSpan_image_iff (since := "2025-05-18")]

theorem Affine.Simplex.mem_affineSpan_range_face_points_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {i : Fin (n + 1)} : s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs

@[deprecated Affine.Simplex.mem_affineSpan_image_iff (since := "2025-05-18")]

theorem Affine.Simplex.mem_affineSpan_range_faceOpposite_points_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} [NeZero n] (s : Simplex k P n) {i j : Fin (n + 1)} : s.points i ∈ affineSpan k (Set.range (s.faceOpposite j).points) ↔ i ≠ j

def Affine.Simplex.map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : Simplex k P₂ n

Push forward an affine simplex under an injective affine map.

Equations

• s.map f hf = { points := ⇑f ∘ s.points, independent := ⋯ }

@[simp]

theorem Affine.Simplex.map_points {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : (s.map f hf).points = ⇑f ∘ s.points

@[simp]

theorem Affine.Simplex.map_id {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : s.map (AffineMap.id k P) ⋯ = s

theorem Affine.Simplex.map_comp {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {P : Type u_5} {P₂ : Type u_6} {P₃ : Type u_7} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V] [Module k V₂] [Module k V₃] [AddTorsor V P] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (g : P₂ →ᵃ[k] P₃) (hg : Function.Injective ⇑g) : s.map (g.comp f) ⋯ = (s.map f hf).map g hg

@[simp]

theorem Affine.Simplex.face_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : (s.map f hf).face h = (s.face h).map f hf

@[simp]

theorem Affine.Simplex.faceOpposite_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} [NeZero n] (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (i : Fin (n + 1)) : (s.map f hf).faceOpposite i = (s.faceOpposite i).map f hf

@[simp]

theorem Affine.Simplex.map_mkOfPoint {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (p : P) : (mkOfPoint k p).map f hf = mkOfPoint k (f p)

def Affine.Simplex.reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : Simplex k P n

Remap a simplex along an Equiv of index types.

Equations

• s.reindex e = { points := s.points ∘ ⇑e.symm, independent := ⋯ }

@[simp]

theorem Affine.Simplex.reindex_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (a✝ : Fin (n + 1)) : (s.reindex e).points a✝ = (s.points ∘ ⇑e.symm) a✝

@[simp]

theorem Affine.Simplex.reindex_refl {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : s.reindex (Equiv.refl (Fin (n + 1))) = s

Reindexing by Equiv.refl yields the original simplex.

@[simp]

theorem Affine.Simplex.reindex_trans {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n₁ n₂ n₃ : ℕ} (e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)) (e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1)) (s : Simplex k P n₁) : s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃

Reindexing by the composition of two equivalences is the same as reindexing twice.

@[simp]

theorem Affine.Simplex.reindex_reindex_symm {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).reindex e.symm = s

Reindexing by an equivalence and its inverse yields the original simplex.

@[simp]

theorem Affine.Simplex.reindex_symm_reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e.symm).reindex e = s

Reindexing by the inverse of an equivalence and that equivalence yields the original simplex.

@[simp]

theorem Affine.Simplex.reindex_range_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : Set.range (s.reindex e).points = Set.range s.points

Reindexing a simplex produces one with the same set of points.

theorem Affine.Simplex.reindex_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : (s.map f hf).reindex e = (s.reindex e).map f hf

def Affine.Simplex.restrict {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) : Simplex k (↥S) n

Restrict an affine simplex to an affine subspace that contains it.

Equations

• s.restrict S hS = { points := fun (i : Fin (n + 1)) => ⟨s.points i, ⋯⟩, independent := ⋯ }

@[simp]

theorem Affine.Simplex.restrict_points_coe {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) (i : Fin (n + 1)) : ↑((s.restrict S hS).points i) = s.points i

@[simp]

theorem Affine.Simplex.restrict_map_inclusion {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (S₁ S₂ : AffineSubspace k P) (hS₁ : affineSpan k (Set.range s.points) ≤ S₁) (hS₂ : S₁ ≤ S₂) : (s.restrict S₁ hS₁).map (AffineSubspace.inclusion hS₂) ⋯ = s.restrict S₂ ⋯

Restricting to S₁ then mapping to a larger S₂ is the same as restricting to S₂.

@[simp]

theorem Affine.Simplex.map_subtype_restrict {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (S : AffineSubspace k P) [Nonempty ↥S] (s : Simplex k (↥S) n) : (s.map S.subtype ⋯).restrict S ⋯ = s

theorem Affine.Simplex.restrict_map_restrict {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (S₁ : AffineSubspace k P) (S₂ : AffineSubspace k P₂) (hS₁ : affineSpan k (Set.range s.points) ≤ S₁) (hfS : AffineSubspace.map f S₁ ≤ S₂) : (s.restrict S₁ hS₁).map (f.restrict hfS) ⋯ = (s.map f hf).restrict S₂ ⋯

Restricting to S₁ then mapping through the restriction of f to S₁ →ᵃ[k] S₂ is the same as mapping through unrestricted f, then restricting to S₂.

@[simp]

theorem Affine.Simplex.restrict_map_subtype {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : (s.restrict (affineSpan k (Set.range s.points)) ⋯).map (affineSpan k (Set.range s.points)).subtype ⋯ = s

Restricting to affineSpan k (Set.range s.points) can be reversed by mapping through AffineSubspace.subtype.

def Affine.Simplex.interior {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : Set P

The interior of a simplex is the set of points that can be expressed as an affine combination of the vertices with weights strictly between 0 and 1. This is equivalent to the intrinsic interior of the convex hull of the vertices.

Equations

• s.interior = {p : P | ∃ (w : Fin (n + 1) → k), ∑ i : Fin (n + 1), w i = 1 ∧ (∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1) ∧ (Finset.affineCombination k Finset.univ s.points) w = p}

theorem Affine.Simplex.affineCombination_mem_interior_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) : (Finset.affineCombination k Finset.univ s.points) w ∈ s.interior ↔ ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1

def Affine.Simplex.closedInterior {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : Set P

s.closedInterior is the set of points that can be expressed as an affine combination of the vertices with weights between 0 and 1 inclusive. This is equivalent to the convex hull of the vertices or the closure of the interior.

Equations

• One or more equations did not get rendered due to their size.

theorem Affine.Simplex.affineCombination_mem_closedInterior_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) : (Finset.affineCombination k Finset.univ s.points) w ∈ s.closedInterior ↔ ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1

theorem Affine.Simplex.interior_subset_closedInterior {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : s.interior ⊆ s.closedInterior

theorem Affine.Simplex.closedInterior_subset_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s : Simplex k P n} : s.closedInterior ⊆ ↑(affineSpan k (Set.range s.points))

@[simp]

theorem Affine.Simplex.interior_eq_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 0) : s.interior = ∅

@[simp]

theorem Affine.Simplex.closedInterior_eq_singleton {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [AddCommGroup V] [Module k V] [AddTorsor V P] [ZeroLEOneClass k] (s : Simplex k P 0) : s.closedInterior = {s.points 0}