# mathlibdocumentation

linear_algebra.affine_space.basic

# Affine spaces

This file defines affine spaces (over modules) and subspaces, affine maps, and the affine span of a set of points. For affine combinations of points, see linear_algebra.affine_space.combination. For affinely independent families of points, see linear_algebra.affine_space.independent. For some additional results relating to finite-dimensional subspaces of affine spaces, see linear_algebra.affine_space.finite_dimensional.

## Main definitions

• affine_space V P is an abbreviation for add_torsor V P in the case of module k V. P is the type of points in the space and V the k-module of displacement vectors. Definitions and results not depending on the module structure appear in algebra.add_torsor instead of here; that includes the instance of an add_group as an add_torsor over itself, which thus gives a module as an affine_space over itself. Definitions of affine spaces vary as to whether a space with no points is permitted; here, we require a nonempty type of points (via the definition of torsors requiring a nonempty type). Affine spaces are defined over any module, with stronger type class requirements on k being used for individual lemmas where needed.
• affine_subspace k P is the type of affine subspaces. Unlike affine spaces, affine subspaces are allowed to be empty, and lemmas that do not apply to empty affine subspaces have nonempty hypotheses. There is a complete_lattice structure on affine subspaces.
• affine_subspace.direction gives the submodule spanned by the pairwise differences of points in an affine_subspace. There are various lemmas relating to the set of vectors in the direction, and relating the lattice structure on affine subspaces to that on their directions.
• affine_span gives the affine subspace spanned by a set of points, with vector_span giving its direction. affine_span is defined in terms of span_points, which gives an explicit description of the points contained in the affine span; span_points itself should generally only be used when that description is required, with affine_span being the main definition for other purposes. Two other descriptions of the affine span are proved equivalent: it is the Inf of affine subspaces containing the points, and (if [nontrivial k]) it contains exactly those points that are affine combinations of points in the given set.
• affine_map is the type of affine maps between two affine spaces with the same ring k. Various basic examples of affine maps are defined, including const, id, line_map and homothety.

## Notations

• P1 →ᵃ[k] P2 is a notation for affine_map k P1 P2

## Implementation notes

out_param is used to make V an implicit argument (deduced from P) in most cases; include V is needed in many cases for V, and type classes using it, to be added as implicit arguments to individual lemmas. As for modules, k is an explicit argument rather than implied by P or V.

This file only provides purely algebraic definitions and results. Those depending on analysis or topology are defined elsewhere; see analysis.normed_space.add_torsor and topology.algebra.affine.

TODO: Some key definitions are not yet present.

• Coercions from an affine_subspace to the subtype of its points, and a corresponding affine_space instance on that subtype in the case of a nonempty subspace.
• affine_equiv (see issue #2909).
• Affine frames. An affine frame might perhaps be represented as an affine_equiv to a finsupp (in the general case) or function type (in the finite-dimensional case) that gives the coordinates, with appropriate proofs of existence when k is a field.
• Although results on affine combinations implicitly provide barycentric frames and coordinates, there is no explicit representation of the map from a point to its coordinates.

## References

• https://en.wikipedia.org/wiki/Affine_space
• https://en.wikipedia.org/wiki/Principal_homogeneous_space
def vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :
set P V

The submodule spanning the differences of a (possibly empty) set of points.

Equations
theorem vector_span_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :
s = (s -ᵥ s)

The definition of vector_span, for rewriting.

theorem vector_span_mono (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s₁ s₂ : set P} :
s₁ s₂ s₁ s₂

vector_span is monotone.

@[simp]
theorem vector_span_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] :

The vector_span of the empty set is ⊥.

@[simp]
theorem vector_span_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) :
{p} =

The vector_span of a single point is ⊥.

theorem vsub_set_subset_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :
s -ᵥ s s)

The s -ᵥ s lies within the vector_span k s.

theorem vsub_mem_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p1 p2 : P} :
p1 sp2 sp1 -ᵥ p2 s

Each pairwise difference is in the vector_span.

def span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :
set Pset P

The points in the affine span of a (possibly empty) set of points. Use affine_span instead to get an affine_subspace k P.

Equations
• s = {p : P | ∃ (p1 : P) (H : p1 s) (v : V) (H : v s), p = v +ᵥ p1}
theorem mem_span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) (s : set P) :
p sp s

A point in a set is in its affine span.

theorem subset_span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :
s s

A set is contained in its span_points.

@[simp]
theorem span_points_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :

The span_points of a set is nonempty if and only if that set is.

theorem vadd_mem_span_points_of_mem_span_points_of_mem_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p : P} {v : V} :
p sv sv +ᵥ p s

Adding a point in the affine span and a vector in the spanning submodule produces a point in the affine span.

theorem vsub_mem_vector_span_of_mem_span_points_of_mem_span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p1 p2 : P} :
p1 sp2 sp1 -ᵥ p2 s

Subtracting two points in the affine span produces a vector in the spanning submodule.

structure affine_subspace (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] :
Type u_3

An affine_subspace k P is a subset of an affine_space V P that, if not empty, has an affine space structure induced by a corresponding subspace of the module k V.

def submodule.to_affine_subspace {k : Type u_1} {V : Type u_2} [ring k] [ V] :
V

Reinterpret p : submodule k V as an affine_subspace k V.

Equations
@[instance]
def affine_subspace.has_coe (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] :
has_coe P) (set P)

Equations
@[instance]
def affine_subspace.has_mem (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] :
P)

Equations
@[simp]
theorem affine_subspace.mem_coe (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] (p : P) (s : P) :
p s p s

A point is in an affine subspace coerced to a set if and only if it is in that affine subspace.

def affine_subspace.direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :
V

The direction of an affine subspace is the submodule spanned by the pairwise differences of points. (Except in the case of an empty affine subspace, where the direction is the zero submodule, every vector in the direction is the difference of two points in the affine subspace.)

Equations
theorem affine_subspace.direction_eq_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : P) :

The direction equals the vector_span.

def affine_subspace.direction_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} :
s.nonempty V

Alternative definition of the direction when the affine subspace is nonempty. This is defined so that the order on submodules (as used in the definition of submodule.span) can be used in the proof of coe_direction_eq_vsub_set, and is not intended to be used beyond that proof.

Equations
theorem affine_subspace.direction_of_nonempty_eq_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} (h : s.nonempty) :

direction_of_nonempty gives the same submodule as direction.

theorem affine_subspace.coe_direction_eq_vsub_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} :

The set of vectors in the direction of a nonempty affine subspace is given by vsub_set.

theorem affine_subspace.mem_direction_iff_eq_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} (h : s.nonempty) (v : V) :
v s.direction ∃ (p1 : P) (H : p1 s) (p2 : P) (H : p2 s), v = p1 -ᵥ p2

A vector is in the direction of a nonempty affine subspace if and only if it is the subtraction of two vectors in the subspace.

theorem affine_subspace.vadd_mem_of_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {v : V} (hv : v s.direction) {p : P} :
p sv +ᵥ p s

Adding a vector in the direction to a point in the subspace produces a point in the subspace.

theorem affine_subspace.vsub_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p1 p2 : P} :
p1 sp2 sp1 -ᵥ p2 s.direction

Subtracting two points in the subspace produces a vector in the direction.

theorem affine_subspace.vadd_mem_iff_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} (v : V) {p : P} :
p s(v +ᵥ p s v s.direction)

Adding a vector to a point in a subspace produces a point in the subspace if and only if the vector is in the direction.

theorem affine_subspace.coe_direction_eq_vsub_set_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} :
p s(s.direction) = (λ (_x : P), _x -ᵥ p) '' s

Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the right.

theorem affine_subspace.coe_direction_eq_vsub_set_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} :
p s(s.direction) =

Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the left.

theorem affine_subspace.mem_direction_iff_eq_vsub_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} (hp : p s) (v : V) :
v s.direction ∃ (p2 : P) (H : p2 s), v = p2 -ᵥ p

Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the right.

theorem affine_subspace.mem_direction_iff_eq_vsub_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} (hp : p s) (v : V) :
v s.direction ∃ (p2 : P) (H : p2 s), v = p -ᵥ p2

Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the left.

theorem affine_subspace.vsub_right_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} (hp : p s) (p2 : P) :
p2 -ᵥ p s.direction p2 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 affine_subspace.vsub_left_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} (hp : p s) (p2 : P) :
p -ᵥ p2 s.direction p2 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.

@[ext]
theorem affine_subspace.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s1 s2 : P} :
s1 = s2s1 = s2

Two affine subspaces are equal if they have the same points.

theorem affine_subspace.ext_of_direction_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s1 s2 : P} :
s1.direction = s2.direction(s1 s2).nonemptys1 = s2

Two affine subspaces with the same direction and nonempty intersection are equal.

theorem affine_subspace.eq_iff_direction_eq_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s₁ s₂ : P} {p : P} :
p s₁p s₂(s₁ = s₂ s₁.direction = s₂.direction)

Two affine subspaces with nonempty intersection are equal if and only if their directions are equal.

def affine_subspace.mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :
P → V

Construct an affine subspace from a point and a direction.

Equations
theorem affine_subspace.self_mem_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) (direction : V) :
p direction

An affine subspace constructed from a point and a direction contains that point.

theorem affine_subspace.vadd_mem_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {v : V} (p : P) {direction : V} :
v directionv +ᵥ p direction

An affine subspace constructed from a point and a direction contains the result of adding a vector in that direction to that point.

theorem affine_subspace.mk'_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) (direction : V) :
direction).nonempty

An affine subspace constructed from a point and a direction is nonempty.

@[simp]
theorem affine_subspace.direction_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) (direction : V) :
direction).direction = direction

The direction of an affine subspace constructed from a point and a direction.

@[simp]
theorem affine_subspace.mk'_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p : P} :
p s

Constructing an affine subspace from a point in a subspace and that subspace's direction yields the original subspace.

theorem affine_subspace.span_points_subset_coe_of_subset_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {s1 : P} :
s s1 s s1

If an affine subspace contains a set of points, it contains the span_points of that set.

def affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :
set P

The affine span of a set of points is the smallest affine subspace containing those points. (Actually defined here in terms of spans in modules.)

Equations
@[simp]
theorem coe_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :
s) = s

The affine span, converted to a set, is span_points.

theorem subset_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :
s s)

A set is contained in its affine span.

theorem direction_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :
s).direction = s

The direction of the affine span is the vector_span.

theorem mem_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {p : P} {s : set P} :
p sp s

A point in a set is in its affine span.

@[instance]
def affine_subspace.complete_lattice {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] :

Equations
@[instance]
def affine_subspace.inhabited {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] :

Equations
theorem affine_subspace.le_def {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :
s1 s2 s1 s2

The ≤ order on subspaces is the same as that on the corresponding sets.

theorem affine_subspace.le_def' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :
s1 s2 ∀ (p : P), p s1p s2

One subspace is less than or equal to another if and only if all its points are in the second subspace.

theorem affine_subspace.lt_def {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :
s1 < s2 s1 s2

The < order on subspaces is the same as that on the corresponding sets.

theorem affine_subspace.not_le_iff_exists {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :
¬s1 s2 ∃ (p : P) (H : p s1), p s2

One subspace is not less than or equal to another if and only if it has a point not in the second subspace.

theorem affine_subspace.exists_of_lt {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s1 s2 : P} :
s1 < s2(∃ (p : P) (H : p s2), p s1)

If a subspace is less than another, there is a point only in the second.

theorem affine_subspace.lt_iff_le_and_exists {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :
s1 < s2 s1 s2 ∃ (p : P) (H : p s2), p s1

A subspace is less than another if and only if it is less than or equal to the second subspace and there is a point only in the second.

theorem affine_subspace.eq_of_direction_eq_of_nonempty_of_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s₁ s₂ : P} :
s₁.direction = s₂.directions₁.nonemptys₁ s₂s₁ = s₂

If an affine subspace is nonempty and contained in another with the same direction, they are equal.

theorem affine_subspace.affine_span_eq_Inf (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] (s : set P) :
s = Inf {s' : | s s'}

The affine span is the Inf of subspaces containing the given points.

def affine_subspace.gi (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

The Galois insertion formed by affine_span and coercion back to a set.

Equations
@[simp]
theorem affine_subspace.span_empty (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

The span of the empty set is ⊥.

@[simp]
theorem affine_subspace.span_univ (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

The span of univ is ⊤.

@[simp]
theorem affine_subspace.coe_affine_span_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] (p : P) :
{p}) = {p}

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

@[simp]
theorem affine_subspace.mem_affine_span_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] (p1 p2 : P) :
p1 {p2} p1 = p2

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

theorem affine_subspace.span_union (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] (s t : set P) :
(s t) = s t

The span of a union of sets is the sup of their spans.

theorem affine_subspace.span_Union (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] {ι : Type u_4} (s : ι → set P) :
(⋃ (i : ι), s i) = ⨆ (i : ι), (s i)

The span of a union of an indexed family of sets is the sup of their spans.

@[simp]
theorem affine_subspace.top_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

⊤, coerced to a set, is the whole set of points.

theorem affine_subspace.mem_top (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] (p : P) :

All points are in ⊤.

@[simp]
theorem affine_subspace.direction_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

The direction of ⊤ is the whole module as a submodule.

@[simp]
theorem affine_subspace.bot_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

⊥, coerced to a set, is the empty set.

theorem affine_subspace.not_mem_bot (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [ V] [S : P] (p : P) :

No points are in ⊥.

@[simp]
theorem affine_subspace.direction_bot (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [ V] [S : P] :

The direction of ⊥ is the submodule ⊥.

@[simp]
theorem affine_subspace.direction_eq_top_iff_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s : P} :

A nonempty affine subspace is ⊤ if and only if its direction is ⊤.

@[simp]
theorem affine_subspace.inf_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :
s1 s2 = s1 s2

The inf of two affine subspaces, coerced to a set, is the intersection of the two sets of points.

theorem affine_subspace.mem_inf_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (p : P) (s1 s2 : P) :
p s1 s2 p s1 p s2

A point is in the inf of two affine subspaces if and only if it is in both of them.

theorem affine_subspace.direction_inf {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :

The direction of the inf of two affine subspaces is less than or equal to the inf of their directions.

theorem affine_subspace.direction_inf_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s₁ s₂ : P} {p : P} :
p s₁p s₂(s₁ s₂).direction = s₁.direction s₂.direction

If two affine subspaces have a point in common, the direction of their inf equals the inf of their directions.

theorem affine_subspace.direction_inf_of_mem_inf {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s₁ s₂ : P} {p : P} :
p s₁ s₂(s₁ s₂).direction = s₁.direction s₂.direction

If two affine subspaces have a point in their inf, the direction of their inf equals the inf of their directions.

theorem affine_subspace.direction_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s1 s2 : P} :
s1 s2s1.direction s2.direction

If one affine subspace is less than or equal to another, the same applies to their directions.

theorem affine_subspace.direction_lt_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s1 s2 : P} :
s1 < s2s1.nonemptys1.direction < s2.direction

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

theorem affine_subspace.sup_direction_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s1 s2 : P) :

The sup of the directions of two affine subspaces is less than or equal to the direction of their sup.

theorem affine_subspace.sup_direction_lt_of_nonempty_of_inter_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s1 s2 : P} :
s1.nonemptys2.nonemptys1 s2 = s1.direction s2.direction < (s1 s2).direction

The sup of the directions of two nonempty affine subspaces with empty intersection is less than the direction of their sup.

theorem affine_subspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s1 s2 : P} :

If the directions of two nonempty affine subspaces span the whole module, they have nonempty intersection.

theorem affine_subspace.inter_eq_singleton_of_nonempty_of_is_compl {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] {s1 s2 : P} :
s1.nonemptys2.nonempty s2.direction(∃ (p : P), s1 s2 = {p})

If the directions of two nonempty affine subspaces are complements of each other, they intersect in exactly one point.

@[simp]
theorem affine_subspace.affine_span_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [S : P] (s : P) :
s = s

Coercing a subspace to a set then taking the affine span produces the original subspace.

theorem vector_span_eq_span_vsub_set_left (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p : P} :
p s s = '' s)

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

theorem vector_span_eq_span_vsub_set_right (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p : P} :
p s s = ((λ (_x : P), _x -ᵥ p) '' s)

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

theorem vector_span_eq_span_vsub_set_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p : P} :
p s s = '' (s \ {p}))

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

theorem vector_span_eq_span_vsub_set_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p : P} :
p s s = ((λ (_x : P), _x -ᵥ p) '' (s \ {p}))

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

theorem vector_span_image_eq_span_vsub_set_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) {s : set ι} {i : ι} :
i s (p '' s) = (has_vsub.vsub (p i) '' (p '' (s \ {i})))

The vector_span 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 vector_span_image_eq_span_vsub_set_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) {s : set ι} {i : ι} :
i s (p '' s) = ((λ (_x : P), _x -ᵥ p i) '' (p '' (s \ {i})))

The vector_span 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 vector_span_range_eq_span_range_vsub_left (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) (i0 : ι) :
(set.range p) = (set.range (λ (i : ι), p i0 -ᵥ p i))

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

theorem vector_span_range_eq_span_range_vsub_right (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) (i0 : ι) :
(set.range p) = (set.range (λ (i : ι), p i -ᵥ p i0))

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

theorem vector_span_range_eq_span_range_vsub_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) (i₀ : ι) :
(set.range p) = (set.range (λ (i : {x // x i₀}), p i₀ -ᵥ p i))

The vector_span 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 vector_span_range_eq_span_range_vsub_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) (i₀ : ι) :
(set.range p) = (set.range (λ (i : {x // x i₀}), p i -ᵥ p i₀))

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

theorem affine_span_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (s : set P) :

The affine span of a set is nonempty if and only if that set is.

theorem affine_span_singleton_union_vadd_eq_top_of_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set V} (p : P) :
({p} (λ (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 affine_span_mono (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s₁ s₂ : set P} :
s₁ s₂ s₁ s₂

affine_span is monotone.

theorem affine_span_insert_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) (ps : set P) :
(insert p ps)) = (insert p ps)

Taking the affine span of a set, adding a point and taking the span again produces the same results as adding the point to the set and taking the span.

theorem affine_span_insert_eq_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {p : P} {ps : set P} :
p ps (insert p ps) = ps

If a point is in the affine span of a set, adding it to that set does not change the affine span.

theorem affine_subspace.direction_sup {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s1 s2 : P} {p1 p2 : P} :
p1 s1p2 s2(s1 s2).direction = s1.direction s2.direction {p2 -ᵥ p1}

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 affine_subspace.direction_affine_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p1 p2 : P} :
p1 s (insert p2 s)).direction = {p2 -ᵥ p1} 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 affine_subspace.mem_affine_span_insert_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : P} {p1 : P} (hp1 : p1 s) (p2 p : P) :
p (insert p2 s) ∃ (r : k) (p0 : P) (hp0 : p0 s), p = r (p2 -ᵥ p1) +ᵥ p0

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

structure affine_map (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
Type (max u_2 u_3 u_4 u_5)

An affine_map k P1 P2 (notation: P1 →ᵃ[k] P2) is a map from P1 to P2 that induces a corresponding linear map from V1 to V2.

@[instance]
def affine_map.has_coe_to_fun (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :

Equations
def linear_map.to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] :
(V₁ →ₗ[k] V₂)(V₁ →ᵃ[k] V₂)

Reinterpret a linear map as an affine map.

Equations
@[simp]
theorem linear_map.coe_to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] (f : V₁ →ₗ[k] V₂) :

@[simp]
theorem linear_map.to_affine_map_linear {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] (f : V₁ →ₗ[k] V₂) :

@[simp]
theorem affine_map.coe_mk {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (linear : V1 →ₗ[k] V2) (add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p) :
{to_fun := f, linear := linear, map_vadd' := add} = f

Constructing an affine map and coercing back to a function produces the same map.

@[simp]
theorem affine_map.to_fun_eq_coe {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :

to_fun is the same as the result of coercing to a function.

@[simp]
theorem affine_map.map_vadd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1) :
f (v +ᵥ p) = (f.linear) v +ᵥ f p

An affine map on the result of adding a vector to a point produces the same result as the linear map applied to that vector, added to the affine map applied to that point.

@[simp]
theorem affine_map.linear_map_vsub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) (p1 p2 : P1) :
(f.linear) (p1 -ᵥ p2) = f p1 -ᵥ f p2

The linear map on the result of subtracting two points is the result of subtracting the result of the affine map on those two points.

@[ext]
theorem affine_map.ext {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] {f g : P1 →ᵃ[k] P2} :
(∀ (p : P1), f p = g p)f = g

Two affine maps are equal if they coerce to the same function.

theorem affine_map.ext_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] {f g : P1 →ᵃ[k] P2} :
f = g ∀ (p : P1), f p = g p

theorem affine_map.injective_coe_fn {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
function.injective (λ (f : P1 →ᵃ[k] P2) (x : P1), f x)

theorem affine_map.congr_arg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) {x y : P1} :
x = yf x = f y

theorem affine_map.congr_fun {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] {f g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) :
f x = g x

def affine_map.const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
P2 → (P1 →ᵃ[k] P2)

Constant function as an affine_map.

Equations
@[simp]
theorem affine_map.coe_const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p : P2) :
P1 p) = p

@[simp]
theorem affine_map.const_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p : P2) :
P1 p).linear = 0

@[instance]
def affine_map.nonempty {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :

def affine_map.mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) :
(∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p)(P1 →ᵃ[k] P2)

Construct an affine map by verifying the relation between the map and its linear part at one base point. Namely, this function takes a map f : P₁ → P₂, a linear map f' : V₁ →ₗ[k] V₂, and a point p such that for any other point p' we have f p' = f' (p' -ᵥ p) +ᵥ f p.

Equations
@[simp]
theorem affine_map.coe_mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
f' p h) = f

@[simp]
theorem affine_map.mk'_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
f' p h).linear = f'

@[instance]
def affine_map.add_comm_group {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :

The set of affine maps to a vector space is an additive commutative group.

Equations
@[simp]
theorem affine_map.coe_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
0 = 0

@[simp]
theorem affine_map.zero_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
0.linear = 0

@[simp]
theorem affine_map.coe_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (f g : P1 →ᵃ[k] V2) :
(f + g) = f + g

@[simp]
theorem affine_map.add_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (f g : P1 →ᵃ[k] V2) :
(f + g).linear = f.linear + g.linear

@[instance]
def affine_map.add_torsor {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
affine_space (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2)

The space of affine maps from P1 to P2 is an affine space over the space of affine maps from P1 to the vector space V2 corresponding to P2.

Equations
@[simp]
theorem affine_map.vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) :
(f +ᵥ g) p = f p +ᵥ g p

@[simp]
theorem affine_map.vsub_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f g : P1 →ᵃ[k] P2) (p : P1) :
(f -ᵥ g) p = f p -ᵥ g p

def affine_map.fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
P1 × P2 →ᵃ[k] P1

prod.fst as an affine_map.

Equations
@[simp]
theorem affine_map.coe_fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :

@[simp]
theorem affine_map.fst_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :

def affine_map.snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
P1 × P2 →ᵃ[k] P2

prod.snd as an affine_map.

Equations
@[simp]
theorem affine_map.coe_snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :

@[simp]
theorem affine_map.snd_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :

def affine_map.id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [ V1] [ P1] :
P1 →ᵃ[k] P1

Identity map as an affine map.

Equations
@[simp]
theorem affine_map.coe_id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [ V1] [ P1] :
P1) = id

The identity affine map acts as the identity.

@[simp]
theorem affine_map.id_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [ V1] [ P1] :

theorem affine_map.id_apply (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p : P1) :
P1) p = p

The identity affine map acts as the identity.

@[instance]
def affine_map.inhabited {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] :

Equations
def affine_map.comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ V3] [ P3] :
(P2 →ᵃ[k] P3)(P1 →ᵃ[k] P2)(P1 →ᵃ[k] P3)

Composition of affine maps.

Equations
@[simp]
theorem affine_map.coe_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ V3] [ P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) :
(f.comp g) = f g

Composition of affine maps acts as applying the two functions.

theorem affine_map.comp_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ V3] [ P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1) :
(f.comp g) p = f (g p)

Composition of affine maps acts as applying the two functions.

@[simp]
theorem affine_map.comp_id {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
f.comp P1) = f

@[simp]
theorem affine_map.id_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
P2).comp f = f

theorem affine_map.comp_assoc {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} {V4 : Type u_8} {P4 : Type u_9} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ V3] [ P3] [add_comm_group V4] [ V4] [ P4] (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2) :
(f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)

@[instance]
def affine_map.monoid {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] :
monoid (P1 →ᵃ[k] P1)

Equations
@[simp]
theorem affine_map.coe_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (f g : P1 →ᵃ[k] P1) :
f * g = f g

@[simp]
theorem affine_map.coe_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] :

### Definition of affine_map.line_map and lemmas about it

def affine_map.line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] :
P1 → P1 → (k →ᵃ[k] P1)

The affine map from k to P1 sending 0 to p₀ and 1 to p₁.

Equations
theorem affine_map.coe_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) :
p₁) = λ (c : k), c (p₁ -ᵥ p₀) +ᵥ p₀

theorem affine_map.line_map_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
p₁) c = c (p₁ -ᵥ p₀) +ᵥ p₀

theorem affine_map.line_map_apply_module' {k : Type u_1} {V1 : Type u_2} [ring k] [add_comm_group V1] [ V1] (p₀ p₁ : V1) (c : k) :
p₁) c = c (p₁ - p₀) + p₀

theorem affine_map.line_map_apply_module {k : Type u_1} {V1 : Type u_2} [ring k] [add_comm_group V1] [ V1] (p₀ p₁ : V1) (c : k) :
p₁) c = (1 - c) p₀ + c p₁

theorem affine_map.line_map_apply_ring' {k : Type u_1} [ring k] (a b c : k) :
b) c = c * (b - a) + a

theorem affine_map.line_map_apply_ring {k : Type u_1} [ring k] (a b c : k) :
b) c = (1 - c) * a + c * b

theorem affine_map.line_map_vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p : P1) (v : V1) (c : k) :
(v +ᵥ p)) c = c v +ᵥ p

@[simp]
theorem affine_map.line_map_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) :
p₁).linear = linear_map.id.smul_right (p₁ -ᵥ p₀)

theorem affine_map.line_map_same_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p : P1) (c : k) :
p) c = p

@[simp]
theorem affine_map.line_map_same {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p : P1) :
= p

@[simp]
theorem affine_map.line_map_apply_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) :
p₁) 0 = p₀

@[simp]
theorem affine_map.line_map_apply_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) :
p₁) 1 = p₁

@[simp]
theorem affine_map.apply_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) :
f ( p₁) c) = (affine_map.line_map (f p₀) (f p₁)) c

@[simp]
theorem affine_map.comp_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) :
f.comp p₁) = affine_map.line_map (f p₀) (f p₁)

@[simp]
theorem affine_map.fst_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p₀ p₁ : P1 × P2) (c : k) :
( p₁) c).fst = p₁.fst) c

@[simp]
theorem affine_map.snd_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p₀ p₁ : P1 × P2) (c : k) :
( p₁) c).snd = p₁.snd) c

theorem affine_map.line_map_symm {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) :
p₁ = p₀).comp 0)

theorem affine_map.line_map_apply_one_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
p₁) (1 - c) = p₀) c

theorem affine_map.decomp {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [add_comm_group V2] [ V2] (f : V1 →ᵃ[k] V2) :
f = (f.linear) + λ (z : V1), f 0

Decomposition of an affine map in the special case when the point space and vector space are the same.

theorem affine_map.decomp' {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [add_comm_group V2] [ V2] (f : V1 →ᵃ[k] V2) :
(f.linear) = f - λ (z : V1), f 0

Decomposition of an affine map in the special case when the point space and vector space are the same.

theorem affine_map.image_interval {k : Type u_1} (f : k →ᵃ[k] k) (a b : k) :
f '' b = set.interval (f a) (f b)

@[instance]
def affine_map.module {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [comm_ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
(P1 →ᵃ[k] V2)

If k is a commutative ring, then the set of affine maps with codomain in a k-module is a k-module.

Equations
@[simp]
theorem affine_map.coe_smul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [comm_ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (c : k) (f : P1 →ᵃ[k] V2) :
(c f) = c f

def affine_map.homothety {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] :
P1 → k → (P1 →ᵃ[k] P1)

homothety c r is the homothety about c with scale factor r.

Equations
theorem affine_map.homothety_def {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) (r : k) :
= r P1 -ᵥ P1 c) +ᵥ P1 c

theorem affine_map.homothety_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) (r : k) (p : P1) :
r) p = r (p -ᵥ c) +ᵥ c

@[simp]
theorem affine_map.homothety_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) :
= P1

theorem affine_map.homothety_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) (r₁ r₂ : k) :
(r₁ * r₂) = r₁).comp r₂)

@[simp]
theorem affine_map.homothety_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) :
= P1 c

@[simp]
theorem affine_map.homothety_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) (r₁ r₂ : k) :
(r₁ + r₂) = r₁ P1 -ᵥ P1 c) +ᵥ

def affine_map.homothety_hom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] :
P1 → (k →* P1 →ᵃ[k] P1)

homothety as a multiplicative monoid homomorphism.

Equations
@[simp]
theorem affine_map.coe_homothety_hom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) :

def affine_map.homothety_affine {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] :
P1 → (k →ᵃ[k] P1 →ᵃ[k] P1)

homothety as an affine map.

Equations
@[simp]
theorem affine_map.coe_homothety_affine {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [ V1] [ P1] (c : P1) :