Affine independence

This file defines affinely independent families of points.

Main definitions

• AffineIndependent defines affinely independent families of points as those where no nontrivial weighted subtraction is 0. This is proved equivalent to two other formulations: linear independence of the results of subtracting a base point in the family from the other points in the family, or any equal affine combinations having the same weights. A bundled type Simplex is provided for finite affinely independent families of points, with an abbreviation Triangle for the case of three points.

References

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

def AffineIndependent (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) : Prop

An indexed family is said to be affinely independent if no nontrivial weighted subtractions (where the sum of weights is 0) are 0.

Equations

• AffineIndependent k p = ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0

theorem affineIndependent_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) : AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0

The definition of AffineIndependent.

theorem affineIndependent_of_subsingleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Subsingleton ι] (p : ι → P) : AffineIndependent k p

A family with at most one point is affinely independent.

theorem affineIndependent_iff_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Fintype ι] (p : ι → P) : AffineIndependent k p ↔ ∀ (w : ι → k), ∑ i : ι, w i = 0 → (Finset.univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0

A family indexed by a Fintype is affinely independent if and only if no nontrivial weighted subtractions over Finset.univ (where the sum of the weights is 0) are 0.

theorem affineIndependent_iff_linearIndependent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) (i1 : ι) : AffineIndependent k p ↔ LinearIndependent k fun (i : { x : ι // x ≠ i1 }) => p ↑i -ᵥ p i1

A family is affinely independent if and only if the differences from a base point in that family are linearly independent.

theorem affineIndependent_set_iff_linearIndependent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p₁ : P} (hp₁ : p₁ ∈ s) : (AffineIndependent k fun (p : ↑s) => ↑p) ↔ LinearIndependent k fun (v : ↑((fun (p : P) => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

A set is affinely independent if and only if the differences from a base point in that set are linearly independent.

theorem linearIndependent_set_iff_affineIndependent_vadd_union_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set V} (hs : ∀ v ∈ s, v ≠ 0) (p₁ : P) : (LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun (p : ↑({p₁} ∪ (fun (v : V) => v +ᵥ p₁) '' s)) => ↑p

A set of nonzero vectors is linearly independent if and only if, given a point p₁, the vectors added to p₁ and p₁ itself are affinely independent.

theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) : AffineIndependent k p ↔ ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k), ∑ i ∈ s1, w1 i = 1 → ∑ i ∈ s2, w2 i = 1 → (Finset.affineCombination k s1 p) w1 = (Finset.affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2

A family is affinely independent if and only if any affine combinations (with sum of weights 1) that evaluate to the same point have equal Set.indicator.

theorem affineIndependent_iff_eq_of_fintype_affineCombination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Fintype ι] (p : ι → P) : AffineIndependent k p ↔ ∀ (w1 w2 : ι → k), ∑ i : ι, w1 i = 1 → ∑ i : ι, w2 i = 1 → (Finset.affineCombination k Finset.univ p) w1 = (Finset.affineCombination k Finset.univ p) w2 → w1 = w2

A finite family is affinely independent if and only if any affine combinations (with sum of weights 1) that evaluate to the same point are equal.

theorem AffineIndependent.units_lineMap {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (hp : AffineIndependent k p) (j : ι) (w : ι → kˣ) : AffineIndependent k fun (i : ι) => (AffineMap.lineMap (p j) (p i)) ↑(w i)

If we single out one member of an affine-independent family of points and affinely transport all others along the line joining them to this member, the resulting new family of points is affine- independent.

This is the affine version of LinearIndependent.units_smul.

theorem AffineIndependent.indicator_eq_of_affineCombination_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) (s₁ : Finset ι) (s₂ : Finset ι) (w₁ : ι → k) (w₂ : ι → k) (hw₁ : ∑ i ∈ s₁, w₁ i = 1) (hw₂ : ∑ i ∈ s₂, w₂ i = 1) (h : (Finset.affineCombination k s₁ p) w₁ = (Finset.affineCombination k s₂ p) w₂) : (↑s₁).indicator w₁ = (↑s₂).indicator w₂

theorem AffineIndependent.injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) : Function.Injective p

An affinely independent family is injective, if the underlying ring is nontrivial.

theorem AffineIndependent.comp_embedding {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ↪ ι) {p : ι → P} (ha : AffineIndependent k p) : AffineIndependent k (p ∘ ⇑f)

If a family is affinely independent, so is any subfamily given by composition of an embedding into index type with the original family.

theorem AffineIndependent.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) (s : Set ι) : AffineIndependent k fun (i : ↑s) => p ↑i

If a family is affinely independent, so is any subfamily indexed by a subtype of the index type.

theorem AffineIndependent.range {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) : AffineIndependent k fun (x : ↑(Set.range p)) => ↑x

If an indexed family of points is affinely independent, so is the corresponding set of points.

theorem affineIndependent_equiv {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') {p : ι' → P} : AffineIndependent k (p ∘ ⇑e) ↔ AffineIndependent k p

theorem AffineIndependent.mono {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {t : Set P} (ha : AffineIndependent k fun (x : ↑t) => ↑x) (hs : s ⊆ t) : AffineIndependent k fun (x : ↑s) => ↑x

If a set of points is affinely independent, so is any subset.

theorem AffineIndependent.of_set_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k fun (x : ↑(Set.range p)) => ↑x) (hi : Function.Injective p) : AffineIndependent k p

If the range of an injective indexed family of points is affinely independent, so is that family.

theorem AffineIndependent.of_comp {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hai : AffineIndependent k (⇑f ∘ p)) : AffineIndependent k p

If the image of a family of points in affine space under an affine transformation is affine- independent, then the original family of points is also affine-independent.

theorem AffineIndependent.map' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (hai : AffineIndependent k p) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : AffineIndependent k (⇑f ∘ p)

The image of a family of points in affine space, under an injective affine transformation, is affine-independent.

theorem AffineMap.affineIndependent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : AffineIndependent k (⇑f ∘ p) ↔ AffineIndependent k p

Injective affine maps preserve affine independence.

theorem AffineEquiv.affineIndependent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (e : P ≃ᵃ[k] P₂) : AffineIndependent k (⇑e ∘ p) ↔ AffineIndependent k p

Affine equivalences preserve affine independence of families of points.

theorem AffineEquiv.affineIndependent_set_of_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {s : Set P} (e : P ≃ᵃ[k] P₂) : AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val

Affine equivalences preserve affine independence of subsets.

theorem AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) {s1 : Set ι} {s2 : Set ι} {p0 : P} (hp0s1 : p0 ∈ affineSpan k (p '' s1)) (hp0s2 : p0 ∈ affineSpan k (p '' s2)) : ∃ (i : ι), i ∈ s1 ∩ s2

If a family is affinely independent, and the spans of points indexed by two subsets of the index type have a point in common, those subsets of the index type have an element in common, if the underlying ring is nontrivial.

theorem AffineIndependent.affineSpan_disjoint_of_disjoint {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) {s1 : Set ι} {s2 : Set ι} (hd : Disjoint s1 s2) : Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))

If a family is affinely independent, the spans of points indexed by disjoint subsets of the index type are disjoint, if the underlying ring is nontrivial.

@[simp]

theorem AffineIndependent.mem_affineSpan_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∈ affineSpan k (p '' s) ↔ i ∈ s

If a family is affinely independent, a point in the family is in the span of some of the points given by a subset of the index type if and only if that point's index is in the subset, if the underlying ring is nontrivial.

theorem AffineIndependent.not_mem_affineSpan_diff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∉ affineSpan k (p '' (s \ {i}))

If a family is affinely independent, a point in the family is not in the affine span of the other points, if the underlying ring is nontrivial.

theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {t : Finset V} (h : ¬AffineIndependent k Subtype.val) : ∃ (f : V → k), ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

theorem affineIndependent_iff {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_5} {p : ι → V} : AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0

Viewing a module as an affine space modelled on itself, we can characterise affine independence in terms of linear combinations.

theorem AffineIndependent.eq_zero_of_sum_eq_zero {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {s : Finset ι} {w : ι → k} {p : ι → V} (hp : AffineIndependent k p) (hw₀ : ∑ i ∈ s, w i = 0) (hw₁ : ∑ i ∈ s, w i • p i = 0) (i : ι) : i ∈ s → w i = 0

theorem AffineIndependent.eq_of_sum_eq_sum {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {s : Finset ι} {w₁ : ι → k} {w₂ : ι → k} {p : ι → V} (hp : AffineIndependent k p) (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i) (hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i) (i : ι) : i ∈ s → w₁ i = w₂ i

theorem AffineIndependent.eq_zero_of_sum_eq_zero_subtype {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {s : Finset V} (hp : AffineIndependent k Subtype.val) {w : V → k} (hw₀ : ∑ x ∈ s, w x = 0) (hw₁ : ∑ x ∈ s, w x • x = 0) (x : V) : x ∈ s → w x = 0

theorem AffineIndependent.eq_of_sum_eq_sum_subtype {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {s : Finset V} (hp : AffineIndependent k Subtype.val) {w₁ : V → k} {w₂ : V → k} (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i) (hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i) (i : V) : i ∈ s → w₁ i = w₂ i

theorem weightedVSub_mem_vectorSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w : ι → k} {w₁ : ι → k} {w₂ : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 0) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) : (s.weightedVSub p) w ∈ vectorSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Given an affinely independent family of points, a weighted subtraction lies in the vectorSpan of two points given as affine combinations if and only if it is a weighted subtraction with weights a multiple of the difference between the weights of the two points.

theorem affineCombination_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w : ι → k} {w₁ : ι → k} {w₂ : ι → k} {s : Finset ι} : ∑ i ∈ s, w i = 1 → ∑ i ∈ s, w₁ i = 1 → ∑ i ∈ s, w₂ i = 1 → ((Finset.affineCombination k s p) w ∈ affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔ ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i)

Given an affinely independent family of points, an affine combination lies in the span of two points given as affine combinations if and only if it is an affine combination with weights those of one point plus a multiple of the difference between the weights of the two points.

theorem exists_subset_affineIndependent_affineSpan_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : AffineIndependent k fun (p : ↑s) => ↑p) : ∃ (t : Set P), s ⊆ t ∧ (AffineIndependent k fun (p : ↑t) => ↑p) ∧ affineSpan k t = ⊤

An affinely independent set of points can be extended to such a set that spans the whole space.

theorem exists_affineIndependent (k : Type u_1) (V : Type u_2) {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) : ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val

theorem affineIndependent_of_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} (h : p₁ ≠ p₂) : AffineIndependent k ![p₁, p₂]

Two different points are affinely independent.

theorem AffineIndependent.affineIndependent_of_not_mem_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} {i : ι} (ha : AffineIndependent k fun (x : { y : ι // y ≠ i }) => p ↑x) (hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})) : AffineIndependent k p

If all but one point of a family are affinely independent, and that point does not lie in the affine span of that family, the family is affinely independent.

theorem affineIndependent_of_ne_of_mem_of_mem_of_not_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∉ s) : AffineIndependent k ![p₁, p₂, p₃]

If distinct points p₁ and p₂ lie in s but p₃ does not, the three points are affinely independent.

theorem affineIndependent_of_ne_of_mem_of_not_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₁p₃ : p₁ ≠ p₃) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∉ s) (hp₃ : p₃ ∈ s) : AffineIndependent k ![p₁, p₂, p₃]

If distinct points p₁ and p₃ lie in s but p₂ does not, the three points are affinely independent.

theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ : P} {p₂ : P} {p₃ : P} (hp₂p₃ : p₂ ≠ p₃) (hp₁ : p₁ ∉ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) : AffineIndependent k ![p₁, p₂, p₃]

If distinct points p₂ and p₃ lie in s but p₁ does not, the three points are affinely independent.

theorem sign_eq_of_affineCombination_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [LinearOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w : ι → k} {w₁ : ι → k} {w₂ : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (hs : (Finset.affineCombination k s p) w ∈ affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂}) {i : ι} {j : ι} (hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0) (hj0 : w₁ j = 0) (hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)) : SignType.sign (w i) = SignType.sign (w j)

Given an affinely independent family of points, suppose that an affine combination lies in the span of two points given as affine combinations, and suppose that, for two indices, the coefficients in the first point in the span are zero and those in the second point in the span have the same sign. Then the coefficients in the combination lying in the span have the same sign.

theorem sign_eq_of_affineCombination_mem_affineSpan_single_lineMap {k : Type u_1} {V : Type u_2} {P : Type u_3} [LinearOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) {i₁ : ι} {i₂ : ι} {i₃ : ι} (h₁ : i₁ ∈ s) (h₂ : i₂ ∈ s) (h₃ : i₃ ∈ s) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {c : k} (hc0 : 0 < c) (hc1 : c < 1) (hs : (Finset.affineCombination k s p) w ∈ affineSpan k {p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c}) : SignType.sign (w i₂) = SignType.sign (w i₃)

Given an affinely independent family of points, suppose that an affine combination lies in the span of one point of that family and a combination of another two points of that family given by lineMap with coefficient between 0 and 1. Then the coefficients of those two points in the combination lying in the span have the same sign.

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

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

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

theorem Affine.Simplex.independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (self : Affine.Simplex k P n) : AffineIndependent k self.points

@[reducible, inline]

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

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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) : Affine.Simplex k P 0

Construct a 0-simplex from a point.

Equations

• Affine.Simplex.mkOfPoint k p = let_fun this := Affine.Simplex.mkOfPoint.proof_1; { 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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (i : Fin 1) : (Affine.Simplex.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Inhabited P] : Inhabited (Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] : Nonempty (Affine.Simplex k P 0)

Equations

• ⋯ = ⋯

theorem Affine.Simplex.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s1 : Affine.Simplex k P n} {s2 : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s1 : Affine.Simplex k P n) (s2 : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) (i : Fin (n + 1)) : s.face ⋯ = Affine.Simplex.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.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.

@[simp]

theorem Affine.Simplex.reindex_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m : ℕ} {n : ℕ} (s : Affine.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

def Affine.Simplex.reindex {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m : ℕ} {n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : Affine.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_refl {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.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_3} [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 : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m : ℕ} {n : ℕ} (s : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m : ℕ} {n : ℕ} (s : Affine.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_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m : ℕ} {n : ℕ} (s : Affine.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.

@[simp]

theorem Affine.Simplex.face_centroid_eq_centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : Finset.centroid k Finset.univ (s.face h).points = Finset.centroid k fs s.points

The centroid of a face of a simplex as the centroid of a subset of the points.

@[simp]

theorem Affine.Simplex.centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n) {fs₁ : Finset (Fin (n + 1))} {fs₂ : Finset (Fin (n + 1))} {m₁ : ℕ} {m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂

Over a characteristic-zero division ring, the centroids given by two subsets of the points of a simplex are equal if and only if those faces are given by the same subset of points.

theorem Affine.Simplex.face_centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n) {fs₁ : Finset (Fin (n + 1))} {fs₂ : Finset (Fin (n + 1))} {m₁ : ℕ} {m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) : Finset.centroid k Finset.univ (s.face h₁).points = Finset.centroid k Finset.univ (s.face h₂).points ↔ fs₁ = fs₂

Over a characteristic-zero division ring, the centroids of two faces of a simplex are equal if and only if those faces are given by the same subset of points.

theorem Affine.Simplex.centroid_eq_of_range_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s₁ : Affine.Simplex k P n} {s₂ : Affine.Simplex k P n} (h : Set.range s₁.points = Set.range s₂.points) : Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points

Two simplices with the same points have the same centroid.