Affine spaces

This file gives further properties of affine subspaces (over modules) and the affine span of a set of points.

Main definitions

• AffineSubspace.Parallel, notation ∥, gives the property of two affine subspaces being parallel (one being a translate of the other).

@[simp]

theorem vectorSpan_vadd (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) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s

theorem AffineSubspace.vsub_right_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) : p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Given a point in an affine subspace, a result of subtracting that point on the right is in the direction if and only if the other point is in the subspace.

theorem AffineSubspace.vsub_left_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) : p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s

Given a point in an affine subspace, a result of subtracting that point on the left is in the direction if and only if the other point is in the subspace.

@[reducible, inline]

abbrev AffineSubspace.toAddTorsor {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] : AddTorsor ↥s.direction ↥s

This is not an instance because it loops with AddTorsor.nonempty.

Equations

• s.toAddTorsor = AddTorsor.mk ⋯ ⋯

@[simp]

theorem AffineSubspace.coe_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] (a b : ↥s) : ↑(a -ᵥ b) = ↑a -ᵥ ↑b

@[simp]

theorem AffineSubspace.coe_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] (a : ↥s.direction) (b : ↥s) : ↑(a +ᵥ b) = ↑a +ᵥ ↑b

def AffineSubspace.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] : ↥s →ᵃ[k] P

Embedding of an affine subspace to the ambient space, as an affine map.

Equations

• s.subtype = { toFun := Subtype.val, linear := s.direction.subtype, map_vadd' := ⋯ }

@[simp]

theorem AffineSubspace.subtype_linear {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] : s.subtype.linear = s.direction.subtype

@[simp]

theorem AffineSubspace.subtype_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} [Nonempty ↥s] (p : ↥s) : s.subtype p = ↑p

theorem AffineSubspace.subtype_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] : Function.Injective ⇑s.subtype

@[simp]

theorem AffineSubspace.coe_subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] : ⇑s.subtype = Subtype.val

@[deprecated AffineSubspace.coe_subtype (since := "2025-02-18")]

theorem AffineSubspace.coeSubtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty ↥s] : ⇑s.subtype = Subtype.val

Alias of AffineSubspace.coe_subtype.

theorem AffineMap.lineMap_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {Q : AffineSubspace k P} {p₀ p₁ : P} (c : k) (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q) : (lineMap p₀ p₁) c ∈ Q

@[simp]

theorem AffineSubspace.coe_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (p : P) : ↑(affineSpan k {p}) = {p}

The affine span of a single point, coerced to a set, contains just that point.

@[simp]

theorem AffineSubspace.mem_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {p₁ p₂ : P} : p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂

A point is in the affine span of a single point if and only if they are equal.

instance AffineSubspace.unique_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (p : P) : Unique ↥(affineSpan k {p})

Equations

• AffineSubspace.unique_affineSpan_singleton k V p = { default := ⟨p, ⋯⟩, uniq := ⋯ }

@[simp]

theorem AffineSubspace.preimage_coe_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (x : P) : Subtype.val ⁻¹' {x} = Set.univ

def AffineSubspace.topEquiv (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] : ↥⊤ ≃ᵃ[k] P

The top affine subspace is linearly equivalent to the affine space. This is the affine version of Submodule.topEquiv.

Equations

• AffineSubspace.topEquiv k V P = { toEquiv := Equiv.Set.univ P, linear := (LinearEquiv.ofEq ⊤.direction ⊤ ⋯).trans Submodule.topEquiv, map_vadd' := ⋯ }

@[simp]

theorem AffineSubspace.topEquiv_apply (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (self : { x : P // x ∈ Set.univ }) : (topEquiv k V P) self = ↑self

@[simp]

theorem AffineSubspace.topEquiv_symm_apply_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (a : P) : ↑((topEquiv k V P).symm a) = a

@[simp]

theorem AffineSubspace.linear_topEquiv (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] : (topEquiv k V P).linear = (LinearEquiv.ofEq ⊤.direction ⊤ ⋯).trans Submodule.topEquiv

theorem AffineSubspace.subsingleton_of_subsingleton_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ⊤) : Subsingleton P

theorem AffineSubspace.eq_univ_of_subsingleton_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ⊤) : s = Set.univ

theorem AffineSubspace.direction_lt_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂) (hn : (↑s₁).Nonempty) : s₁.direction < s₂.direction

If one nonempty affine subspace is less than another, the same applies to their directions

theorem vectorSpan_eq_span_vsub_set_left (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) : vectorSpan k s = Submodule.span k ((fun (x : P) => p -ᵥ x) '' s)

The vectorSpan is the span of the pairwise subtractions with a given point on the left.

theorem vectorSpan_eq_span_vsub_set_right (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) : vectorSpan k s = Submodule.span k ((fun (x : P) => x -ᵥ p) '' s)

The vectorSpan is the span of the pairwise subtractions with a given point on the right.

theorem vectorSpan_eq_span_vsub_set_left_ne (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) : vectorSpan k s = Submodule.span k ((fun (x : P) => p -ᵥ x) '' (s \ {p}))

The vectorSpan is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

theorem vectorSpan_eq_span_vsub_set_right_ne (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) : vectorSpan k s = Submodule.span k ((fun (x : P) => x -ᵥ p) '' (s \ {p}))

The vectorSpan is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

theorem vectorSpan_eq_span_vsub_finset_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [DecidableEq P] [DecidableEq V] {s : Finset P} {p : P} (hp : p ∈ s) : vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun (x : P) => x -ᵥ p) (s.erase p))

The vectorSpan is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

theorem vectorSpan_image_eq_span_vsub_set_left_ne (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) {s : Set ι} {i : ι} (hi : i ∈ s) : vectorSpan k (p '' s) = Submodule.span k ((fun (x : P) => p i -ᵥ x) '' (p '' (s \ {i})))

The vectorSpan of the image of a function is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

theorem vectorSpan_image_eq_span_vsub_set_right_ne (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) {s : Set ι} {i : ι} (hi : i ∈ s) : vectorSpan k (p '' s) = Submodule.span k ((fun (x : P) => x -ᵥ p i) '' (p '' (s \ {i})))

The vectorSpan of the image of a function is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

theorem vectorSpan_range_eq_span_range_vsub_left (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) (i0 : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : ι) => p i0 -ᵥ p i)

The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the left.

theorem vectorSpan_range_eq_span_range_vsub_right (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) (i0 : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : ι) => p i -ᵥ p i0)

The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the right.

theorem vectorSpan_range_eq_span_range_vsub_left_ne (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) (i₀ : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₀ }) => p i₀ -ᵥ p ↑i)

The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

theorem vectorSpan_range_eq_span_range_vsub_right_ne (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) (i₀ : ι) : vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : { x : ι // x ≠ i₀ }) => p ↑i -ᵥ p i₀)

The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

@[simp]

theorem affineSpan_coe_preimage_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (A : Set P) [Nonempty ↑A] : affineSpan k (Subtype.val ⁻¹' A) = ⊤

A set, considered as a subset of its spanned affine subspace, spans the whole subspace.

theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top {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} (p : P) (h : Submodule.span k (Set.range Subtype.val) = ⊤) : affineSpan k ({p} ∪ (fun (v : V) => v +ᵥ p) '' s) = ⊤

Suppose a set of vectors spans V. Then a point p, together with those vectors added to p, spans P.

theorem vectorSpan_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ p₂ : P) : vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}

The vectorSpan of two points is the span of their difference.

theorem vectorSpan_pair_rev (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ p₂ : P) : vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}

The vectorSpan of two points is the span of their difference (reversed).

theorem 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] {p₁ p₂ : P} {v : V} : v ∈ vectorSpan k {p₁, p₂} ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v

A vector lies in the vectorSpan of two points if and only if it is a multiple of their difference.

theorem mem_vectorSpan_pair_rev {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ p₂ : P} {v : V} : v ∈ vectorSpan k {p₁, p₂} ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v

A vector lies in the vectorSpan of two points if and only if it is a multiple of their difference (reversed).

theorem AffineMap.lineMap_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] (r : k) (p₁ p₂ : P) : (lineMap p₁ p₂) r ∈ affineSpan k {p₁, p₂}

A combination of two points expressed with lineMap lies in their affine span.

theorem AffineMap.lineMap_rev_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] (r : k) (p₁ p₂ : P) : (lineMap p₂ p₁) r ∈ affineSpan k {p₁, p₂}

A combination of two points expressed with lineMap (with the two points reversed) lies in their affine span.

theorem smul_vsub_vadd_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] (r : k) (p₁ p₂ : P) : r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ affineSpan k {p₁, p₂}

A multiple of the difference of two points added to the first point lies in their affine span.

theorem smul_vsub_rev_vadd_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] (r : k) (p₁ p₂ : P) : r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ affineSpan k {p₁, p₂}

A multiple of the difference of two points added to the second point lies in their affine span.

theorem vadd_left_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] {p₁ p₂ : P} {v : V} : v +ᵥ p₁ ∈ affineSpan k {p₁, p₂} ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v

A vector added to the first point lies in the affine span of two points if and only if it is a multiple of their difference.

theorem vadd_right_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] {p₁ p₂ : P} {v : V} : v +ᵥ p₂ ∈ affineSpan k {p₁, p₂} ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v

A vector added to the second point lies in the affine span of two points if and only if it is a multiple of their difference.

theorem AffineSubspace.direction_sup {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s₁) (hp₂ : p₂ ∈ s₂) : (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

The direction of the sup of two nonempty affine subspaces is the sup of the two directions and of any one difference between points in the two subspaces.

theorem AffineSubspace.direction_affineSpan_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) : (affineSpan k (insert p₂ ↑s)).direction = Submodule.span k {p₂ -ᵥ p₁} ⊔ s.direction

The direction of the span of the result of adding a point to a nonempty affine subspace is the sup of the direction of that subspace and of any one difference between that point and a point in the subspace.

theorem AffineSubspace.mem_affineSpan_insert_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ p : P) : p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Given a point p₁ in an affine subspace s, and a point p₂, a point p is in the span of s with p₂ added if and only if it is a multiple of p₂ -ᵥ p₁ added to a point in s.

@[simp]

theorem AffineMap.vectorSpan_image_eq_submodule_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁} : Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)

def AffineSubspace.map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) : AffineSubspace k P₂

The image of an affine subspace under an affine map as an affine subspace.

Equations

• AffineSubspace.map f s = { carrier := ⇑f '' ↑s, smul_vsub_vadd_mem := ⋯ }

@[simp]

theorem AffineSubspace.coe_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) : ↑(map f s) = ⇑f '' ↑s

@[simp]

theorem AffineSubspace.mem_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₂} {s : AffineSubspace k P₁} : x ∈ map f s ↔ ∃ y ∈ s, f y = x

theorem AffineSubspace.mem_map_of_mem {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {x : P₁} {s : AffineSubspace k P₁} (h : x ∈ s) : f x ∈ map f s

@[simp]

theorem AffineSubspace.mem_map_iff_mem_of_injective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₁} (hf : Function.Injective ⇑f) : f x ∈ map f s ↔ x ∈ s

@[simp]

theorem AffineSubspace.map_bot {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) : map f ⊥ = ⊥

@[simp]

theorem AffineSubspace.map_eq_bot_iff {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : AffineSubspace k P₁} : map f s = ⊥ ↔ s = ⊥

@[simp]

theorem AffineSubspace.map_id {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (s : AffineSubspace k P₁) : map (AffineMap.id k P₁) s = s

theorem AffineSubspace.map_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (s : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) : map g (map f s) = map (g.comp f) s

@[simp]

theorem AffineSubspace.map_direction {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) : (map f s).direction = Submodule.map f.linear s.direction

theorem AffineSubspace.map_span {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : Set P₁) : map f (affineSpan k s) = affineSpan k (⇑f '' s)

def AffineSubspace.inclusion {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ S₂ : AffineSubspace k P₁} [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ ≤ S₂) : ↥S₁ →ᵃ[k] ↥S₂

Affine map from a smaller to a larger subspace of the same space.

This is the affine version of Submodule.inclusion.

Equations

• AffineSubspace.inclusion h = { toFun := Set.inclusion h, linear := Submodule.inclusion ⋯, map_vadd' := ⋯ }

@[simp]

theorem AffineSubspace.inclusion_linear {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ S₂ : AffineSubspace k P₁} [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ ≤ S₂) : (inclusion h).linear = Submodule.inclusion ⋯

@[simp]

theorem AffineSubspace.coe_inclusion_apply {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ S₂ : AffineSubspace k P₁} [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ ≤ S₂) (x : ↥S₁) : ↑((inclusion h) x) = ↑x

@[simp]

theorem AffineSubspace.inclusion_rfl {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ : AffineSubspace k P₁} [Nonempty ↥S₁] : inclusion ⋯ = AffineMap.id k ↥S₁

@[simp]

theorem AffineMap.map_top_of_surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (hf : Function.Surjective ⇑f) : AffineSubspace.map f ⊤ = ⊤

theorem AffineMap.span_eq_top_of_surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁} (hf : Function.Surjective ⇑f) (h : affineSpan k s = ⊤) : affineSpan k (⇑f '' s) = ⊤

def AffineEquiv.ofEq {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ = S₂) : ↥S₁ ≃ᵃ[k] ↥S₂

Affine equivalence between two equal affine subspace.

This is the affine version of LinearEquiv.ofEq.

Equations

• AffineEquiv.ofEq S₁ S₂ h = { toEquiv := Equiv.Set.ofEq ⋯, linear := LinearEquiv.ofEq S₁.direction S₂.direction ⋯, map_vadd' := ⋯ }

@[simp]

theorem AffineEquiv.linear_ofEq {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ = S₂) : (ofEq S₁ S₂ h).linear = LinearEquiv.ofEq S₁.direction S₂.direction ⋯

@[simp]

theorem AffineEquiv.coe_ofEq_apply {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ = S₂) (x : ↥S₁) : ↑((ofEq S₁ S₂ h) x) = ↑x

@[simp]

theorem AffineEquiv.ofEq_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [Nonempty ↥S₁] [Nonempty ↥S₂] (h : S₁ = S₂) : (ofEq S₁ S₂ h).symm = ofEq S₂ S₁ ⋯

@[simp]

theorem AffineEquiv.ofEq_rfl {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) [Nonempty ↥S₁] : ofEq S₁ S₁ ⋯ = refl k ↥S₁

theorem AffineEquiv.span_eq_top_iff {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {s : Set P₁} (e : P₁ ≃ᵃ[k] P₂) : affineSpan k s = ⊤ ↔ affineSpan k (⇑e '' s) = ⊤

def AffineSubspace.comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : AffineSubspace k P₁

The preimage of an affine subspace under an affine map as an affine subspace.

Equations

• AffineSubspace.comap f s = { carrier := ⇑f ⁻¹' ↑s, smul_vsub_vadd_mem := ⋯ }

@[simp]

theorem AffineSubspace.coe_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : ↑(comap f s) = ⇑f ⁻¹' ↑s

@[simp]

theorem AffineSubspace.mem_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₂} : x ∈ comap f s ↔ f x ∈ s

theorem AffineSubspace.comap_mono {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s t : AffineSubspace k P₂} : s ≤ t → comap f s ≤ comap f t

@[simp]

theorem AffineSubspace.comap_top {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} : comap f ⊤ = ⊤

@[simp]

theorem AffineSubspace.comap_bot {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) : comap f ⊥ = ⊥

@[simp]

theorem AffineSubspace.comap_id {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (s : AffineSubspace k P₁) : comap (AffineMap.id k P₁) s = s

theorem AffineSubspace.comap_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (s : AffineSubspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) : comap f (comap g s) = comap (g.comp f) s

theorem AffineSubspace.map_le_iff_le_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s : AffineSubspace k P₁} {t : AffineSubspace k P₂} : map f s ≤ t ↔ s ≤ comap f t

theorem AffineSubspace.gc_map_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) : GaloisConnection (map f) (comap f)

theorem AffineSubspace.map_comap_le {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : map f (comap f s) ≤ s

theorem AffineSubspace.le_comap_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) : s ≤ comap f (map f s)

theorem AffineSubspace.map_sup {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (s t : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) : map f (s ⊔ t) = map f s ⊔ map f t

theorem AffineSubspace.map_iSup {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {ι : Sort u_8} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₁) : map f (iSup s) = ⨆ (i : ι), map f (s i)

theorem AffineSubspace.comap_inf {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (s t : AffineSubspace k P₂) (f : P₁ →ᵃ[k] P₂) : comap f (s ⊓ t) = comap f s ⊓ comap f t

theorem AffineSubspace.comap_supr {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {ι : Sort u_8} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₂) : comap f (iInf s) = ⨅ (i : ι), comap f (s i)

@[simp]

theorem AffineSubspace.comap_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁) : comap (↑e.symm) s = map (↑e) s

@[simp]

theorem AffineSubspace.map_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₂) : map (↑e.symm) s = comap (↑e) s

theorem AffineSubspace.comap_span {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : comap (↑f) (affineSpan k s) = affineSpan k (⇑f ⁻¹' s)

def AffineSubspace.Parallel {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s₁ s₂ : AffineSubspace k P) : Prop

Two affine subspaces are parallel if one is related to the other by adding the same vector to all points.

Equations

• s₁.Parallel s₂ = ∃ (v : V), s₂ = AffineSubspace.map (↑(AffineEquiv.constVAdd k P v)) s₁

def Affine.«term_∥_» : Lean.TrailingParserDescr

Two affine subspaces are parallel if one is related to the other by adding the same vector to all points.

Equations

• Affine.«term_∥_» = Lean.ParserDescr.trailingNode `Affine.«term_∥_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∥ ") (Lean.ParserDescr.cat `term 51))

theorem AffineSubspace.Parallel.symm {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : AffineSubspace k P} (h : s₁.Parallel s₂) : s₂.Parallel s₁

theorem AffineSubspace.parallel_comm {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : AffineSubspace k P} : s₁.Parallel s₂ ↔ s₂.Parallel s₁

theorem AffineSubspace.Parallel.refl {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) : s.Parallel s

theorem AffineSubspace.Parallel.trans {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ s₃ : AffineSubspace k P} (h₁₂ : s₁.Parallel s₂) (h₂₃ : s₂.Parallel s₃) : s₁.Parallel s₃

theorem AffineSubspace.Parallel.direction_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : AffineSubspace k P} (h : s₁.Parallel s₂) : s₁.direction = s₂.direction

@[simp]

theorem AffineSubspace.parallel_bot_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} : s.Parallel ⊥ ↔ s = ⊥

@[simp]

theorem AffineSubspace.bot_parallel_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} : ⊥.Parallel s ↔ s = ⊥

theorem AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : AffineSubspace k P} : s₁.Parallel s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

theorem AffineSubspace.Parallel.vectorSpan_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : Set P} (h : (affineSpan k s₁).Parallel (affineSpan k s₂)) : vectorSpan k s₁ = vectorSpan k s₂

theorem AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ s₂ : Set P} : (affineSpan k s₁).Parallel (affineSpan k s₂) ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)

theorem AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ p₂ p₃ p₄ : P} : (affineSpan k {p₁, p₂}).Parallel (affineSpan k {p₃, p₄}) ↔ vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}