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] [add_torsor 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] [add_torsor V P] {ι : Type u_4} (p : ι → P) :
affine_independent k p ↔ ∀ (s : finset ι) (w : ι → k), s.sum (λ (i : ι), 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] [add_torsor 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] [add_torsor V P] {ι : Type u_4} [fintype ι] (p : ι → P) :
affine_independent k p ↔ ∀ (w : ι → k), finset.univ.sum (λ (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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor V P] {ι : Type u_4} (p : ι → P) :
affine_independent k p ↔ ∀ (s1 s2 : finset ι) (w1 w2 : ι → k), s1.sum (λ (i : ι), w1 i) = 1 → s2.sum (λ (i : ι), 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 affine_independent_iff_eq_of_fintype_affine_combination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [fintype ι] (p : ι → P) :
affine_independent k p ↔ ∀ (w1 w2 : ι → k), finset.univ.sum (λ (i : ι), w1 i) = 1 → finset.univ.sum (λ (i : ι), w2 i) = 1 → ⇑(finset.univ.affine_combination p) w1 = ⇑(finset.univ.affine_combination 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.

source
theorem affine_independent.units_line_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (hp : affine_independent k p) (j : ι) (w : ι → kˣ) :
affine_independent k (λ (i : ι), ⇑(affine_map.line_map (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 linear_independent.units_smul.

source
theorem affine_independent.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] [add_torsor V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k p) (s₁ s₂ : finset ι) (w₁ w₂ : ι → k) (hw₁ : s₁.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s₂.sum (λ (i : ι), w₂ i) = 1) (h : ⇑(s₁.affine_combination p) w₁ = ⇑(s₂.affine_combination p) w₂) :
↑s₁.indicator w₁ = ↑s₂.indicator w₂
source
@[protected]
theorem affine_independent.injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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.comp_embedding {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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
@[protected]
theorem affine_independent.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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
@[protected]
theorem affine_independent.range {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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_equiv {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') {p : ι' → P} :
affine_independent k (p ∘ ⇑e) ↔ affine_independent k p
source
@[protected]
theorem affine_independent.mono {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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_set_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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 affine_independent.of_comp {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hai : affine_independent k (⇑f ∘ p)) :
affine_independent 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.

source
theorem affine_independent.map' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (hai : affine_independent k p) (f : P →ᵃ[k] P₂) (hf : function.injective ⇑f) :
affine_independent k (⇑f ∘ p)

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

source
theorem affine_map.affine_independent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hf : function.injective ⇑f) :
affine_independent k (⇑f ∘ p) ↔ affine_independent k p

Injective affine maps preserve affine independence.

source
theorem affine_equiv.affine_independent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (e : P ≃ᵃ[k] P₂) :
affine_independent k (⇑e ∘ p) ↔ affine_independent k p

Affine equivalences preserve affine independence of families of points.

source
theorem affine_equiv.affine_independent_set_of_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {s : set P} (e : P ≃ᵃ[k] P₂) :
affine_independent k coe ↔ affine_independent k coe

Affine equivalences preserve affine independence of subsets.

source
theorem affine_independent.exists_mem_inter_of_exists_mem_inter_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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_independent.affine_span_disjoint_of_disjoint {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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
@[protected, simp]
theorem affine_independent.mem_affine_span_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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 affine_independent.not_mem_affine_span_diff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor 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_nontrivial_relation_sum_zero_of_not_affine_ind {k : Type u_1} {V : Type u_2} [ring k] [add_comm_group V] [module k V] {t : finset V} (h : ¬affine_independent k coe) :
∃ (f : V → k), t.sum (λ (e : V), f e • e) = 0 ∧ t.sum (λ (e : V), f e) = 0 ∧ ∃ (x : V) (H : x ∈ t), f x ≠ 0
source
theorem affine_independent_iff {k : Type u_1} {V : Type u_2} [ring k] [add_comm_group V] [module k V] {ι : Type u_3} {p : ι → V} :
affine_independent k p ↔ ∀ (s : finset ι) (w : ι → k), s.sum w = 0 → s.sum (λ (e : ι), w e • p e) = 0 → ∀ (e : ι), 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.

source
theorem exists_subset_affine_independent_affine_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor 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 exists_affine_independent (k : Type u_1) (V : Type u_2) {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
∃ (t : set P) (H : t ⊆ s), affine_span k t = affine_span k s ∧ affine_independent k coe
source
theorem affine_independent_of_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor 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] [add_torsor V P] (n : ℕ) :
Type u_3

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

Instances for affine.simplex
source
@[reducible]
def affine.triangle (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor 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] [add_torsor 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] [add_torsor 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
@[protected, 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] [add_torsor V P] [inhabited P] :
inhabited (affine.simplex k P 0)
Equations
source
@[protected, 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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.order_emb_of_fin h) i)

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

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] [add_torsor 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.order_emb_of_fin h)

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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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.