mathlib documentation

linear_algebra.affine_space.independent

Affine independence

This file defines affinely independent families of points.

Main definitions

References

source
def affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space 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
source
theorem affine_independent_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} (p : ι → P) :
affine_independent k p ↔ ∀ (s : finset ι) (w : ι → k), ∑ (i : ι) in s, w i = 0 → ⇑(s.weighted_vsub p) w = 0 → ∀ (i : ι), i ∈ s → w i = 0

The definition of affine_independent.

source
theorem affine_independent_of_subsingleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [subsingleton ι] (p : ι → P) :
affine_independent k p

A family with at most one point is affinely independent.

source
theorem affine_independent_iff_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) :
affine_independent k p ↔ ∀ (w : ι → k), ∑ (i : ι), w i = 0 → ⇑(finset.univ.weighted_vsub 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.

source
theorem affine_independent_iff_linear_independent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} (p : ι → P) (i1 : ι) :
affine_independent k p ↔ linear_independent k (λ (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.

source
theorem affine_independent_set_iff_linear_independent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {s : set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
affine_independent k (λ (p : ↥s), ↑p) ↔ linear_independent k (λ (v : ↥((λ (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.

source
theorem linear_independent_set_iff_affine_independent_vadd_union_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {s : set V} (hs : ∀ (v : V), v ∈ s → v ≠ 0) (p₁ : P) :
linear_independent k (λ (v : ↥s), ↑v) ↔ affine_independent k (λ (p : ↥({p₁} ∪ (λ (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.

source
theorem affine_independent_iff_indicator_eq_of_affine_combination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} (p : ι → P) :
affine_independent k p ↔ ∀ (s1 s2 : finset ι) (w1 w2 : ι → k), ∑ (i : ι) in s1, w1 i = 1 → ∑ (i : ι) in s2, w2 i = 1 → ⇑(s1.affine_combination p) w1 = ⇑(s2.affine_combination 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.

source
theorem injective_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) :
function.injective p

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

source
theorem affine_independent_embedding_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ↪ ι) {p : ι → P} (ha : affine_independent k p) :
affine_independent 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.

source
theorem affine_independent_subtype_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k p) (s : set ι) :
affine_independent k (λ (i : ↥s), p ↑i)

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

source
theorem affine_independent_set_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k p) :
affine_independent k (λ (x : ↥(set.range p)), ↑x)

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

source
theorem affine_independent_of_subset_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {s t : set P} (ha : affine_independent k (λ (x : ↥t), ↑x)) (hs : s ⊆ t) :
affine_independent k (λ (x : ↥s), ↑x)

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

source
theorem affine_independent_of_affine_independent_set_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k (λ (x : ↥(set.range p)), ↑x)) (hi : function.injective p) :
affine_independent k p

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

source
theorem exists_mem_inter_of_exists_mem_inter_affine_span_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) {s1 s2 : set ι} {p0 : P} (hp0s1 : p0 ∈ affine_span k (p '' s1)) (hp0s2 : p0 ∈ affine_span 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.

source
theorem affine_span_disjoint_of_disjoint_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) {s1 s2 : set ι} (hd : s1 ∩ s2 = ∅) :
↑(affine_span k (p '' s1)) ∩ ↑(affine_span 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.

source
@[simp]
theorem mem_affine_span_iff_mem_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) (i : ι) (s : set ι) :
p i ∈ affine_span 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.

source
theorem not_mem_affine_span_diff_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) (i : ι) (s : set ι) :
p i ∉ affine_span 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.

source
theorem exists_subset_affine_independent_affine_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [add_comm_group V] [module k V] [affine_space V P] {s : set P} (h : affine_independent k (λ (p : ↥s), ↑p)) :
∃ (t : set P), s ⊆ t ∧ affine_independent k (λ (p : ↥t), ↑p) ∧ affine_span k t = ⊤

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

source
theorem affine_independent_of_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [add_comm_group V] [module k V] [affine_space V P] {p₁ p₂ : P} (h : p₁ ≠ p₂) :
affine_independent k ![p₁, p₂]

Two different points are affinely independent.

source
structure affine.simplex (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [affine_space V P] (n : ℕ) :
Type u_3

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

source
def affine.triangle (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [affine_space V P] :
Type u_3

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

source
def affine.simplex.mk_of_point (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] (p : P) :
affine.simplex k P 0

Construct a 0-simplex from a point.

Equations
source
@[simp]
theorem affine.simplex.mk_of_point_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] (p : P) (i : fin 1) :
(affine.simplex.mk_of_point k p).points i = p

The point in a simplex constructed with mk_of_point.

source
@[instance]
def affine.simplex.inhabited (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] [inhabited P] :
inhabited (affine.simplex k P 0)

Equations
source
@[instance]
def affine.simplex.nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] :
nonempty (affine.simplex k P 0)

source
@[ext]
theorem affine.simplex.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {n : ℕ} {s1 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.

source
theorem affine.simplex.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {n : ℕ} (s1 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.

source
def affine.simplex.face {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space 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
source
theorem affine.simplex.face_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space 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.mono_of_fin h i)

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

source
@[simp]
theorem affine.simplex.face_eq_mk_of_point {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space V P] {n : ℕ} (s : affine.simplex k P n) (i : fin (n + 1)) :
s.face _ = affine.simplex.mk_of_point k (s.points i)

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

source
@[simp]
theorem affine.simplex.range_face_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [affine_space 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.

source
@[simp]
theorem affine.simplex.face_centroid_eq_centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space 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.

source
@[simp]
theorem affine.simplex.centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] [char_zero k] {n : ℕ} (s : affine.simplex k P n) {fs₁ 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.

source
theorem affine.simplex.face_centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] [char_zero k] {n : ℕ} (s : affine.simplex k P n) {fs₁ 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.

source
theorem affine.simplex.centroid_eq_of_range_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [affine_space V P] {n : ℕ} {s₁ 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.