# Affine equivalences #

In this file we define AffineEquiv 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:

• AffineEquiv.refl k P: the identity map as an AffineEquiv;

• e.symm: the inverse map of an AffineEquiv as an AffineEquiv;

• e.trans e': composition of two AffineEquivs; note that the order follows mathlib's CategoryTheory convention (apply e, then e'), not the convention used in function composition and compositions of bundled morphisms.

We equip AffineEquiv k P P with a Group structure with multiplication corresponding to composition in AffineEquiv.group.

## Tags #

affine space, affine equivalence

structure AffineEquiv (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] extends :
Type (max (max (max u_2 u_3) u_4) u_5)

An affine equivalence, denoted P₁ ≃ᵃ[k] P₂, 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 LinearEquiv for the linear part in order to allow affine equivalences with good definitional equalities.

Instances For
theorem AffineEquiv.map_vadd' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (self : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) :
self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p

An affine equivalence, denoted P₁ ≃ᵃ[k] P₂, 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 LinearEquiv for the linear part in order to allow affine equivalences with good definitional equalities.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AffineEquiv.toAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₁ →ᵃ[k] P₂

Reinterpret an AffineEquiv as an AffineMap.

Equations
• e = { toFun := e.toFun, linear := e.linear, map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.toAffineMap_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ P₂) (f' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p) :
{ toEquiv := f, linear := f', map_vadd' := h } = { toFun := f, linear := f', map_vadd' := h }
@[simp]
theorem AffineEquiv.linear_toAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
(↑e).linear = e.linear
theorem AffineEquiv.toAffineMap_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
Function.Injective AffineEquiv.toAffineMap
@[simp]
theorem AffineEquiv.toAffineMap_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} :
e = e' e = e'
instance AffineEquiv.equivLike {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂
Equations
• AffineEquiv.equivLike = { coe := fun (f : P₁ ≃ᵃ[k] P₂) => f.toFun, inv := fun (f : P₁ ≃ᵃ[k] P₂) => f.invFun, left_inv := , right_inv := , coe_injective' := }
instance AffineEquiv.instCoeFunForall {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
CoeFun (P₁ ≃ᵃ[k] P₂) fun (x : P₁ ≃ᵃ[k] P₂) => P₁P₂
Equations
• AffineEquiv.instCoeFunForall = DFunLike.hasCoeToFun
instance AffineEquiv.instCoeOutEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ P₂)
Equations
• AffineEquiv.instCoeOutEquiv = { coe := AffineEquiv.toEquiv }
@[simp]
theorem AffineEquiv.map_vadd {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) :
e (v +ᵥ p) = e.linear v +ᵥ e p
@[simp]
theorem AffineEquiv.coe_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.toEquiv = e
instance AffineEquiv.instCoeAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)
Equations
• AffineEquiv.instCoeAffineMap = { coe := AffineEquiv.toAffineMap }
@[simp]
theorem AffineEquiv.coe_toAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e = e
@[simp]
theorem AffineEquiv.coe_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e = e
@[simp]
theorem AffineEquiv.coe_linear {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
(↑e).linear = e.linear
theorem AffineEquiv.ext_iff {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} :
e = e' ∀ (x : P₁), e x = e' x
theorem AffineEquiv.ext {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} (h : ∀ (x : P₁), e x = e' x) :
e = e'
theorem AffineEquiv.coeFn_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
Function.Injective DFunLike.coe
theorem AffineEquiv.coeFn_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} :
e = e' e = e'
theorem AffineEquiv.toEquiv_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] :
Function.Injective AffineEquiv.toEquiv
@[simp]
theorem AffineEquiv.toEquiv_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} :
e.toEquiv = e'.toEquiv e = e'
@[simp]
theorem AffineEquiv.coe_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p) :
{ toEquiv := e, linear := e', map_vadd' := h } = e
def AffineEquiv.mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor 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 a map e : P₁ → P₂, a linear equivalence 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
• AffineEquiv.mk' e e' p h = { toFun := e, invFun := fun (q' : P₂) => e'.symm (q' -ᵥ e p) +ᵥ p, left_inv := , right_inv := , linear := e', map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.coe_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
(AffineEquiv.mk' (⇑e) e' p h) = e
@[simp]
theorem AffineEquiv.linear_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
(AffineEquiv.mk' (⇑e) e' p h).linear = e'
def AffineEquiv.symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₂ ≃ᵃ[k] P₁

Inverse of an affine equivalence as an affine equivalence.

Equations
• e.symm = { toEquiv := e.symm, linear := e.linear.symm, map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.symm_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.symm = e.symm.toEquiv
@[simp]
theorem AffineEquiv.symm_linear {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.linear.symm = e.symm.linear
def AffineEquiv.Simps.apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₁P₂

See Note [custom simps projection]

Equations
Instances For
def AffineEquiv.Simps.symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₂P₁

See Note [custom simps projection]

Equations
• = e.symm
Instances For
theorem AffineEquiv.bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
theorem AffineEquiv.surjective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
theorem AffineEquiv.injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem AffineEquiv.ofBijective_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : ) (a : P₁) :
a = φ a
@[simp]
theorem AffineEquiv.linear_ofBijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : ) :
.linear = LinearEquiv.ofBijective φ.linear
noncomputable def AffineEquiv.ofBijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : ) :
P₁ ≃ᵃ[k] P₂

Bijective affine maps are affine isomorphisms.

Equations
Instances For
theorem AffineEquiv.ofBijective.symm_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : ) :
.symm.toEquiv = (Equiv.ofBijective (⇑φ) ).symm
@[simp]
theorem AffineEquiv.range_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
= Set.univ
@[simp]
theorem AffineEquiv.apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂) :
e (e.symm p) = p
@[simp]
theorem AffineEquiv.symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) :
e.symm (e p) = p
theorem AffineEquiv.apply_eq_iff_eq_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₂} :
e p₁ = p₂ p₁ = e.symm p₂
theorem AffineEquiv.apply_eq_iff_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₁} :
e p₁ = e p₂ p₁ = p₂
@[simp]
theorem AffineEquiv.image_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) :
f.symm '' s = f ⁻¹' s
@[simp]
theorem AffineEquiv.preimage_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) :
f.symm ⁻¹' s = f '' s
def AffineEquiv.refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
P₁ ≃ᵃ[k] P₁

Identity map as an AffineEquiv.

Equations
• = { toEquiv := , linear := , map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.coe_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(AffineEquiv.refl k P₁) = id
@[simp]
theorem AffineEquiv.coe_refl_to_affineMap (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(AffineEquiv.refl k P₁) = AffineMap.id k P₁
@[simp]
theorem AffineEquiv.refl_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :
(AffineEquiv.refl k P₁) x = x
@[simp]
theorem AffineEquiv.toEquiv_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(AffineEquiv.refl k P₁).toEquiv =
@[simp]
theorem AffineEquiv.linear_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(AffineEquiv.refl k P₁).linear =
@[simp]
theorem AffineEquiv.symm_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(AffineEquiv.refl k P₁).symm =
def AffineEquiv.trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] [] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
P₁ ≃ᵃ[k] P₃

Composition of two AffineEquivalences, applied left to right.

Equations
• e.trans e' = { toEquiv := e.trans e'.toEquiv, linear := e.linear.trans e'.linear, map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.coe_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] [] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
(e.trans e') = e' e
@[simp]
theorem AffineEquiv.coe_trans_to_affineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] [] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
(e.trans e') = (↑e').comp e
@[simp]
theorem AffineEquiv.trans_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] [] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) :
(e.trans e') p = e' (e p)
theorem AffineEquiv.trans_assoc {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] [] [Module k V₃] [AddTorsor V₃ P₃] [] [Module k V₄] [AddTorsor 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 AffineEquiv.trans_refl {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.trans (AffineEquiv.refl k P₂) = e
@[simp]
theorem AffineEquiv.refl_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
(AffineEquiv.refl k P₁).trans e = e
@[simp]
theorem AffineEquiv.self_trans_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.trans e.symm =
@[simp]
theorem AffineEquiv.symm_trans_self {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.symm.trans e =
@[simp]
theorem AffineEquiv.apply_lineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a : P₁) (b : P₁) (c : k) :
e ( c) = (AffineMap.lineMap (e a) (e b)) c
instance AffineEquiv.group {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
Group (P₁ ≃ᵃ[k] P₁)
Equations
• AffineEquiv.group =
theorem AffineEquiv.one_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
1 =
@[simp]
theorem AffineEquiv.coe_one {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
1 = id
theorem AffineEquiv.mul_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) (e' : P₁ ≃ᵃ[k] P₁) :
e * e' = e'.trans e
@[simp]
theorem AffineEquiv.coe_mul {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) (e' : P₁ ≃ᵃ[k] P₁) :
(e * e') = e e'
theorem AffineEquiv.inv_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :
e⁻¹ = e.symm
@[simp]
theorem AffineEquiv.linearHom_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (self : P₁ ≃ᵃ[k] P₁) :
AffineEquiv.linearHom self = self.linear
def AffineEquiv.linearHom {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(P₁ ≃ᵃ[k] P₁) →* V₁ ≃ₗ[k] V₁

AffineEquiv.linear on automorphisms is a MonoidHom.

Equations
• AffineEquiv.linearHom = { toFun := AffineEquiv.linear, map_one' := , map_mul' := }
Instances For
@[simp]
theorem AffineEquiv.equivUnitsAffineMap_symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :
(AffineEquiv.equivUnitsAffineMap.symm u) a = u a
@[simp]
theorem AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :
(AffineEquiv.equivUnitsAffineMap.symm u).symm a = u⁻¹ a
@[simp]
theorem AffineEquiv.equivUnitsAffineMap_symm_apply_invFun {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :
(AffineEquiv.equivUnitsAffineMap.symm u).invFun a = u⁻¹ a
@[simp]
theorem AffineEquiv.equivUnitsAffineMap_symm_apply_toFun {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :
(AffineEquiv.equivUnitsAffineMap.symm u) a = u a
@[simp]
theorem AffineEquiv.linear_equivUnitsAffineMap_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) :
(AffineEquiv.equivUnitsAffineMap.symm u).linear = ((Units.map AffineMap.linearHom) u)
@[simp]
theorem AffineEquiv.val_equivUnitsAffineMap_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :
(AffineEquiv.equivUnitsAffineMap e) = e
@[simp]
theorem AffineEquiv.val_inv_equivUnitsAffineMap_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :
(AffineEquiv.equivUnitsAffineMap e)⁻¹ = e.symm
def AffineEquiv.equivUnitsAffineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
(P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ

The group of AffineEquivs are equivalent to the group of units of AffineMap.

This is the affine version of LinearMap.GeneralLinearGroup.generalLinearEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AffineEquiv.vaddConst_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) (v : V₁) :
v = v +ᵥ b
@[simp]
theorem AffineEquiv.vaddConst_symm_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) (p' : P₁) :
.symm p' = p' -ᵥ b
@[simp]
theorem AffineEquiv.linear_vaddConst (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) :
.linear =
def AffineEquiv.vaddConst (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor 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
• = { toEquiv := , linear := , map_vadd' := }
Instances For
def AffineEquiv.constVSub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) :
P₁ ≃ᵃ[k] V₁

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

Equations
• = { toEquiv := , linear := , map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.coe_constVSub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) :
= fun (x : P₁) => p -ᵥ x
@[simp]
theorem AffineEquiv.coe_constVSub_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) :
.symm = fun (v : V₁) => -v +ᵥ p
@[simp]
theorem AffineEquiv.linear_constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) :
@[simp]
theorem AffineEquiv.constVAdd_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) :
∀ (x : P₁), (AffineEquiv.constVAdd k P₁ v) x = v +ᵥ x
def AffineEquiv.constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) :
P₁ ≃ᵃ[k] P₁

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

Note that there is no need for an AffineMap.constVAdd as it is always an equivalence. This is roughly to DistribMulAction.toLinearEquiv as +ᵥ is to •.

Equations
• = { toEquiv := , linear := , map_vadd' := }
Instances For
@[simp]
theorem AffineEquiv.constVAdd_zero (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
=
@[simp]
theorem AffineEquiv.constVAdd_add (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (w : V₁) :
@[simp]
theorem AffineEquiv.constVAdd_symm (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) :
@[simp]
theorem AffineEquiv.constVAddHom_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : ) :
def AffineEquiv.constVAddHom (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] :
→* P₁ ≃ᵃ[k] P₁

A more bundled version of AffineEquiv.constVAdd.

Equations
• = { toFun := fun (v : ) => AffineEquiv.constVAdd k P₁ (Multiplicative.toAdd v), map_one' := , map_mul' := }
Instances For
theorem AffineEquiv.constVAdd_nsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (n : ) (v : V₁) :
AffineEquiv.constVAdd k P₁ (n v) = ^ n
theorem AffineEquiv.constVAdd_zsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (z : ) (v : V₁) :
AffineEquiv.constVAdd k P₁ (z v) = ^ z
def AffineEquiv.homothetyUnitsMulHom {R : Type u_10} {V : Type u_11} {P : Type u_12} [] [] [Module R V] [] (p : P) :

Fixing a point in affine space, homothety about this point gives a group homomorphism from (the centre of) the units of the scalars into the group of affine equivalences.

Equations
• = AffineEquiv.equivUnitsAffineMap.symm.toMonoidHom.comp
Instances For
@[simp]
theorem AffineEquiv.coe_homothetyUnitsMulHom_apply {R : Type u_10} {V : Type u_11} {P : Type u_12} [] [] [Module R V] [] (p : P) (t : Rˣ) :
= (AffineMap.homothety p t)
@[simp]
theorem AffineEquiv.coe_homothetyUnitsMulHom_apply_symm {R : Type u_10} {V : Type u_11} {P : Type u_12} [] [] [Module R V] [] (p : P) (t : Rˣ) :
.symm =
@[simp]
theorem AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe {R : Type u_10} {V : Type u_11} {P : Type u_12} [] [] [Module R V] [] (p : P) :
AffineEquiv.toAffineMap = Units.val
def AffineEquiv.pointReflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :
P₁ ≃ᵃ[k] P₁

Point reflection in x as a permutation.

Equations
• = .trans
Instances For
theorem AffineEquiv.pointReflection_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) (y : P₁) :
y = x -ᵥ y +ᵥ x
@[simp]
theorem AffineEquiv.pointReflection_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :
.symm =
@[simp]
theorem AffineEquiv.toEquiv_pointReflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :
.toEquiv =
@[simp]
theorem AffineEquiv.pointReflection_self (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :
x = x
theorem AffineEquiv.pointReflection_involutive (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :
theorem AffineEquiv.pointReflection_fixed_iff_of_injective_bit0 (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] {x : P₁} {y : P₁} (h : Function.Injective fun (x : V₁) => 2 x) :
y = y y = x

x is the only fixed point of pointReflection 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 AffineEquiv.injective_pointReflection_left_of_injective_bit0 (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (h : Function.Injective fun (x : V₁) => 2 x) (y : P₁) :
Function.Injective fun (x : P₁) => y
theorem AffineEquiv.injective_pointReflection_left_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] (y : P₁) :
Function.Injective fun (x : P₁) => y
theorem AffineEquiv.pointReflection_fixed_iff_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] [] {x : P₁} {y : P₁} :
y = y y = x
def LinearEquiv.toAffineEquiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [] [Module k V₂] (e : V₁ ≃ₗ[k] V₂) :
V₁ ≃ᵃ[k] V₂

Interpret a linear equivalence between modules as an affine equivalence.

Equations
• e.toAffineEquiv = { toEquiv := e.toEquiv, linear := e, map_vadd' := }
Instances For
@[simp]
theorem LinearEquiv.coe_toAffineEquiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [] [Module k V₁] [] [Module k V₂] (e : V₁ ≃ₗ[k] V₂) :
e.toAffineEquiv = e
theorem AffineMap.lineMap_vadd {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (v' : V₁) (p : P₁) (c : k) :
(AffineMap.lineMap v v') c +ᵥ p = (AffineMap.lineMap (v +ᵥ p) (v' +ᵥ p)) c
theorem AffineMap.lineMap_vsub {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (p₁ : P₁) (p₂ : P₁) (p₃ : P₁) (c : k) :
(AffineMap.lineMap p₁ p₂) c -ᵥ p₃ = (AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c
theorem AffineMap.vsub_lineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (p₁ : P₁) (p₂ : P₁) (p₃ : P₁) (c : k) :
p₁ -ᵥ (AffineMap.lineMap p₂ p₃) c = (AffineMap.lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c
theorem AffineMap.vadd_lineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (p₁ : P₁) (p₂ : P₁) (c : k) :
v +ᵥ (AffineMap.lineMap p₁ p₂) c = (AffineMap.lineMap (v +ᵥ p₁) (v +ᵥ p₂)) c
theorem AffineMap.homothety_neg_one_apply {P₁ : Type u_2} {V₁ : Type u_6} [] [AddTorsor V₁ P₁] {R' : Type u_10} [CommRing R'] [Module R' V₁] (c : P₁) (p : P₁) :
(AffineMap.homothety c (-1)) p = p