mathlib documentation

linear_algebra.affine_space.affine_equiv

Affine equivalences

In this file we define affine_equiv k P₁ P₂ (notation: P₁ ≃ᵃ[k] P₂) to be the type of affine equivalences between P₁ and `P₂, i.e., equivalences such that both forward and inverse maps are affine maps.

We define the following equivalences:

Tags

affine space, affine equivalence

@[nolint]
structure affine_equiv (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_4} {V₂ : Type u_5} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] :
Type (max u_2 u_3 u_4 u_5)

An affine equivalence is an equivalence between affine spaces such that both forward and inverse maps are affine.

We define it using an equiv for the map and a linear_equiv for the linear part in order to allow affine equivalences with good definitional equalities.

@[instance]
def affine_equiv.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] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

Equations
def linear_equiv.to_affine_equiv {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [semimodule k V₁] [add_comm_group V₂] [semimodule k V₂] (e : V₁ ≃ₗ[k] V₂) :
V₁ ≃ᵃ[k] V₂

Interpret a linear equivalence between modules as an affine equivalence.

Equations
@[simp]
theorem linear_equiv.coe_to_affine_equiv {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [semimodule k V₁] [add_comm_group V₂] [semimodule k V₂] (e : V₁ ≃ₗ[k] V₂) :

def affine_equiv.refl (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :
P₁ ≃ᵃ[k] P₁

Identity map as an affine_equiv.

Equations
@[simp]
theorem affine_equiv.coe_refl (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :

theorem affine_equiv.refl_apply (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x : P₁) :
(affine_equiv.refl k P₁) x = x

@[simp]
theorem affine_equiv.to_equiv_refl (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :

@[simp]
theorem affine_equiv.linear_refl (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :

@[simp]
theorem affine_equiv.map_vadd {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) :
e (v +ᵥ p) = (e.linear) v +ᵥ e p

@[simp]
theorem affine_equiv.coe_to_equiv {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

def affine_equiv.to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₁ →ᵃ[k] P₂

Reinterpret an affine_equiv as an affine_map.

Equations
@[simp]
theorem affine_equiv.coe_to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.to_affine_map_mk {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (f : P₁ P₂) (f' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p) :
{to_equiv := f, linear := f', map_vadd' := h}.to_affine_map = {to_fun := f, linear := f', map_vadd' := h}

@[simp]
theorem affine_equiv.linear_to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

theorem affine_equiv.injective_to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] :

@[simp]
theorem affine_equiv.to_affine_map_inj {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :

@[ext]
theorem affine_equiv.ext {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ (x : P₁), e x = e' x) :
e = e'

theorem affine_equiv.injective_coe_fn {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] :
function.injective (λ (e : P₁ ≃ᵃ[k] P₂) (x : P₁), e x)

@[simp]
theorem affine_equiv.coe_fn_inj {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :
e = e' e = e'

theorem affine_equiv.injective_to_equiv {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] :

@[simp]
theorem affine_equiv.to_equiv_inj {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :
e.to_equiv = e'.to_equiv e = e'

def affine_equiv.mk' {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
P₁ ≃ᵃ[k] P₂

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

Equations
@[simp]
theorem affine_equiv.coe_mk' {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :

@[simp]
theorem affine_equiv.to_equiv_mk' {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :

@[simp]
theorem affine_equiv.linear_mk' {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
(affine_equiv.mk' e e' p h).linear = e'

def affine_equiv.symm {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₂ ≃ᵃ[k] P₁

Inverse of an affine equivalence as an affine equivalence.

Equations
@[simp]
theorem affine_equiv.symm_to_equiv {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.symm_linear {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

theorem affine_equiv.bijective {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

theorem affine_equiv.surjective {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

theorem affine_equiv.injective {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.range_eq {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.apply_symm_apply {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂) :
e ((e.symm) p) = p

@[simp]
theorem affine_equiv.symm_apply_apply {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) :
(e.symm) (e p) = p

theorem affine_equiv.apply_eq_iff_eq_symm_apply {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₂} :
e p₁ = p₂ p₁ = (e.symm) p₂

@[simp]
theorem affine_equiv.apply_eq_iff_eq {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} :
e p₁ = e p₂ p₁ = p₂

@[simp]
theorem affine_equiv.symm_refl {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :

def affine_equiv.trans {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {P₁ : Type u_6} {P₂ : Type u_7} {P₃ : Type u_8} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] [add_comm_group V₃] [semimodule k V₃] [affine_space V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
P₁ ≃ᵃ[k] P₃

Composition of two affine_equivalences, applied left to right.

Equations
@[simp]
theorem affine_equiv.coe_trans {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {P₁ : Type u_6} {P₂ : Type u_7} {P₃ : Type u_8} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] [add_comm_group V₃] [semimodule k V₃] [affine_space V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
(e.trans e') = e' e

theorem affine_equiv.trans_apply {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {P₁ : Type u_6} {P₂ : Type u_7} {P₃ : Type u_8} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] [add_comm_group V₃] [semimodule k V₃] [affine_space V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) :
(e.trans e') p = e' (e p)

theorem affine_equiv.trans_assoc {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {V₄ : Type u_5} {P₁ : Type u_6} {P₂ : Type u_7} {P₃ : Type u_8} {P₄ : Type u_9} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] [add_comm_group V₃] [semimodule k V₃] [affine_space V₃ P₃] [add_comm_group V₄] [semimodule k V₄] [affine_space V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄) :
(e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)

@[simp]
theorem affine_equiv.trans_refl {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.refl_trans {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.trans_symm {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.symm_trans {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

@[simp]
theorem affine_equiv.apply_line_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_6} {P₂ : Type u_7} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [add_comm_group V₂] [semimodule k V₂] [affine_space V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :

@[instance]
def affine_equiv.group {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :
group (P₁ ≃ᵃ[k] P₁)

Equations
theorem affine_equiv.one_def {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :

@[simp]
theorem affine_equiv.coe_one {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] :

theorem affine_equiv.mul_def {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁) :
e * e' = e'.trans e

@[simp]
theorem affine_equiv.coe_mul {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁) :
e * e' = e e'

theorem affine_equiv.inv_def {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :

def affine_equiv.vadd_const (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (b : P₁) :
V₁ ≃ᵃ[k] P₁

The map v ↦ v +ᵥ b as an affine equivalence between a module V and an affine space P with tangent space V.

Equations
@[simp]
theorem affine_equiv.linear_vadd_const (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (b : P₁) :

@[simp]
theorem affine_equiv.vadd_const_apply (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (b : P₁) (v : V₁) :

@[simp]
theorem affine_equiv.vadd_const_symm_apply (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (b p : P₁) :

def affine_equiv.const_vsub (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (p : P₁) :
P₁ ≃ᵃ[k] V₁

p' ↦ p -ᵥ p' as an equivalence.

Equations
@[simp]
theorem affine_equiv.coe_const_vsub (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (p : P₁) :

@[simp]
theorem affine_equiv.coe_const_vsub_symm (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (p : P₁) :
((affine_equiv.const_vsub k p).symm) = λ (v : V₁), -v +ᵥ p

def affine_equiv.const_vadd (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (v : V₁) :
P₁ ≃ᵃ[k] P₁

The map p ↦ v +ᵥ p as an affine automorphism of an affine space.

Equations
@[simp]
theorem affine_equiv.linear_const_vadd (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (v : V₁) :

@[simp]
theorem affine_equiv.const_vadd_apply (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (v : V₁) (p : P₁) :

@[simp]
theorem affine_equiv.const_vadd_symm_apply (k : Type u_1) {V₁ : Type u_2} (P₁ : Type u_6) [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (v : V₁) (p : P₁) :

def affine_equiv.point_reflection (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x : P₁) :
P₁ ≃ᵃ[k] P₁

Point reflection in x as a permutation.

Equations
theorem affine_equiv.point_reflection_apply (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x y : P₁) :

@[simp]
theorem affine_equiv.point_reflection_symm (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x : P₁) :

@[simp]
theorem affine_equiv.to_equiv_point_reflection (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x : P₁) :

@[simp]
theorem affine_equiv.point_reflection_self (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x : P₁) :

theorem affine_equiv.point_reflection_involutive (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (x : P₁) :

theorem affine_equiv.point_reflection_fixed_iff_of_injective_bit0 (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] {x y : P₁} (h : function.injective bit0) :

x is the only fixed point of point_reflection x. This lemma requires x + x = y + y ↔ x = y. There is no typeclass to use here, so we add it as an explicit argument.

theorem affine_equiv.injective_point_reflection_left_of_injective_bit0 (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (h : function.injective bit0) (y : P₁) :

theorem affine_equiv.injective_point_reflection_left_of_module (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [invertible 2] (y : P₁) :

theorem affine_equiv.point_reflection_fixed_iff_of_module (k : Type u_1) {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] [invertible 2] {x y : P₁} :

theorem affine_map.line_map_vadd {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (v v' : V₁) (p : P₁) (c : k) :

theorem affine_map.line_map_vsub {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k) :
(affine_map.line_map p₁ p₂) c -ᵥ p₃ = (affine_map.line_map (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c

theorem affine_map.vsub_line_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k) :
p₁ -ᵥ (affine_map.line_map p₂ p₃) c = (affine_map.line_map (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c

theorem affine_map.vadd_line_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_6} [ring k] [add_comm_group V₁] [semimodule k V₁] [affine_space V₁ P₁] (v : V₁) (p₁ p₂ : P₁) (c : k) :
v +ᵥ (affine_map.line_map p₁ p₂) c = (affine_map.line_map (v +ᵥ p₁) (v +ᵥ p₂)) c

theorem affine_map.homothety_neg_one_apply {V₁ : Type u_2} {P₁ : Type u_6} [add_comm_group V₁] [affine_space V₁ P₁] {R' : Type u_10} [comm_ring R'] [semimodule R' V₁] (c p : P₁) :