mathlib documentation

linear_algebra.affine_space.independent

Affine independence #

This file defines affinely independent families of points.

Main definitions #

References #

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
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 sw i = 0

The definition of affine_independent.

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) :

A family with at most one point is affinely independent.

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.

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.

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.

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 sv 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.

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) = 1s2.sum (λ (i : ι), w2 i) = 1(s1.affine_combination p) w1 = (s2.affine_combination p) w2s1.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 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) = 1finset.univ.sum (λ (i : ι), w2 i) = 1(finset.univ.affine_combination p) w1 = (finset.univ.affine_combination p) w2w1 = 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 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.

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₂
@[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) :

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

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) :

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

@[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.

@[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) :

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

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} :
@[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.

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) :

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

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)) :

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 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) :

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

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) :

Injective affine maps preserve affine independence.

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 equivalences preserve affine independence of families of points.

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 equivalences preserve affine independence of subsets.

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.

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.

@[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.

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.

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
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 = 0s.sum (λ (e : ι), w e p e) = 0∀ (e : ι), e sw e = 0

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

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.

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
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.

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
@[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.

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) :

Construct a 0-simplex from a point.

Equations
@[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) :

The point in a simplex constructed with mk_of_point.

@[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] :
Equations
@[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] :
@[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.

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.

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) :

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

Equations
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.

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) :

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

@[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)) :

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

@[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) :

The set of points of a face.

@[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) :

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} [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.

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) :

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} [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) :

Two simplices with the same points have the same centroid.