Affine independence

This file defines affinely independent families of points.

Main definitions

affine_independent 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 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) → 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

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

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_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} :

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

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

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

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

p0 ∈ affine_span k (p '' s1) → 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 ι} :

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

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

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

ℕ → Type u_3

points : fin (n + 1) → P
independent : affine_independent k c.points

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 → affine.simplex k P 0

Construct a 0-simplex from a point.

Equations

affine.simplex.mk_of_point k p = {points := λ (_x : fin (0 + 1)), p, independent := _}

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

affine.simplex.inhabited k = {default := affine.simplex.mk_of_point k (inhabited.default P)}

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)

Equations

_ = _

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

(∀ (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 : ℕ} :

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.mono_of_fin h, independent := _}

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.

mathlib documentation

linear_algebra.affine_space.independent

Affine independence

Main definitions

References

General documentation

Additional documentation

Library

mathlib documentation

linear_algebra.​affine_space.​independent

Affine independence

Main definitions

References

General documentation

Additional documentation

Library

linear_algebra.affine_space.independent