# mathlib3documentation

linear_algebra.affine_space.affine_equiv

# Affine equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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

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

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

We equip `affine_equiv k P P` with a `group` structure with multiplication corresponding to composition in `affine_equiv.group`.

## 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₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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.

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

Reinterpret an `affine_equiv` as an `affine_map`.

Equations
@[simp]
theorem affine_equiv.to_affine_map_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
theorem affine_equiv.to_affine_map_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
@[simp]
theorem affine_equiv.to_affine_map_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :
e = e'
@[protected, instance]
def affine_equiv.equiv_like {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
equiv_like (P₁ ≃ᵃ[k] P₂) P₁ P₂
Equations
@[protected, instance]
def affine_equiv.has_coe_to_fun {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
has_coe_to_fun (P₁ ≃ᵃ[k] P₂) (λ (_x : P₁ ≃ᵃ[k] P₂), P₁ P₂)
Equations
@[protected, instance]
def affine_equiv.equiv.has_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
has_coe (P₁ ≃ᵃ[k] P₂) (P₁ P₂)
Equations
@[simp]
theorem affine_equiv.map_vadd {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[protected, instance]
def affine_equiv.affine_map.has_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
has_coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)
Equations
@[simp]
theorem affine_equiv.coe_to_affine_map {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[simp, norm_cast]
theorem affine_equiv.coe_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem affine_equiv.coe_linear {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[ext]
theorem affine_equiv.ext {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {e e' : P₁ ≃ᵃ[k] P₂} (h : (x : P₁), e x = e' x) :
e = e'
theorem affine_equiv.coe_fn_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
@[simp, norm_cast]
theorem affine_equiv.coe_fn_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :
e = e' e = e'
theorem affine_equiv.to_equiv_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] :
@[simp]
theorem affine_equiv.to_equiv_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :
e.to_equiv = e'.to_equiv e = e'
@[simp]
theorem affine_equiv.coe_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (h : (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p) :
{to_equiv := e, linear := e', map_vadd' := h} = e
def affine_equiv.mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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
@[simp]
theorem affine_equiv.coe_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
e' p h) = e
@[simp]
theorem affine_equiv.linear_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
e' p h).linear = e'
@[symm]
def affine_equiv.symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem affine_equiv.symm_linear {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
def affine_equiv.simps.apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₁ P₂
Equations
def affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₂ P₁
Equations
@[protected]
theorem affine_equiv.bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[protected]
theorem affine_equiv.surjective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[protected]
theorem affine_equiv.injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem affine_equiv.of_bijective_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) (ᾰ : P₂) :
.symm) = hφ).inv_fun
@[simp]
theorem affine_equiv.of_bijective_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) (ᾰ : P₁) :
= hφ).to_fun
noncomputable def affine_equiv.of_bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) :
P₁ ≃ᵃ[k] P₂

Bijective affine maps are affine isomorphisms.

Equations
@[simp]
theorem affine_equiv.linear_of_bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) :
theorem affine_equiv.of_bijective.symm_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) :
@[simp]
theorem affine_equiv.range_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂) :
e ((e.symm) p) = p
@[simp]
theorem affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} :
e p₁ = e p₂ p₁ = p₂
@[simp]
theorem affine_equiv.image_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : set P₂) :
(f.symm) '' s = f ⁻¹' s
@[simp]
theorem affine_equiv.preimage_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : set P₁) :
(f.symm) ⁻¹' s = f '' s
@[refl]
def affine_equiv.refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
P₁ ≃ᵃ[k] P₁

Identity map as an `affine_equiv`.

Equations
@[simp]
theorem affine_equiv.coe_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
P₁) = id
@[simp]
theorem affine_equiv.coe_refl_to_affine_map (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
P₁) = P₁
@[simp]
theorem affine_equiv.refl_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (x : P₁) :
P₁) x = x
@[simp]
theorem affine_equiv.to_equiv_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
P₁).to_equiv =
@[simp]
theorem affine_equiv.linear_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
P₁).linear =
@[simp]
theorem affine_equiv.symm_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
P₁).symm =
@[trans]
def affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] [add_comm_group V₃] [ V₃] [ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
P₁ ≃ᵃ[k] P₃

Composition of two `affine_equiv`alences, applied left to right.

Equations
@[simp]
theorem affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] [add_comm_group V₃] [ V₃] [ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
(e.trans e') = e' e
@[simp]
theorem affine_equiv.coe_trans_to_affine_map {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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] [add_comm_group V₃] [ V₃] [ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
(e.trans e') = e'.comp e
@[simp]
theorem affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] [add_comm_group V₃] [ 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} {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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] [add_comm_group V₃] [ V₃] [ P₃] [add_comm_group V₄] [ 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.trans P₂) = e
@[simp]
theorem affine_equiv.refl_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₁).trans e = e
@[simp]
theorem affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.trans e.symm =
@[simp]
theorem affine_equiv.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] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) :
e.symm.trans e =
@[simp]
theorem affine_equiv.apply_line_map {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [add_comm_group V₂] [ V₂] [ P₂] (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :
e ( b) c) = (affine_map.line_map (e a) (e b)) c
@[protected, instance]
def affine_equiv.group {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
group (P₁ ≃ᵃ[k] P₁)
Equations
theorem affine_equiv.one_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
1 =
@[simp]
theorem affine_equiv.coe_one {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
theorem affine_equiv.mul_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (e e' : P₁ ≃ᵃ[k] P₁) :
e * e' = e'.trans e
@[simp]
theorem affine_equiv.coe_mul {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (e e' : P₁ ≃ᵃ[k] P₁) :
(e * e') = e e'
theorem affine_equiv.inv_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (e : P₁ ≃ᵃ[k] P₁) :
def affine_equiv.linear_hom {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
(P₁ ≃ᵃ[k] P₁) →* V₁ ≃ₗ[k] V₁

`affine_equiv.linear` on automorphisms is a `monoid_hom`.

Equations
@[simp]
theorem affine_equiv.linear_hom_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (self : P₁ ≃ᵃ[k] P₁) :
= self.linear
@[simp]
theorem affine_equiv.coe_equiv_units_affine_map_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (e : P₁ ≃ᵃ[k] P₁) :
def affine_equiv.equiv_units_affine_map {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
(P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ

The group of `affine_equiv`s are equivalent to the group of units of `affine_map`.

This is the affine version of `linear_map.general_linear_group.general_linear_equiv`.

Equations
@[simp]
theorem affine_equiv.equiv_units_affine_map_symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (ᾰ : P₁) :
= u ᾰ
@[simp]
theorem affine_equiv.linear_equiv_units_affine_map_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) :
@[simp]
theorem affine_equiv.coe_inv_equiv_units_affine_map_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (e : P₁ ≃ᵃ[k] P₁) :
@[simp]
theorem affine_equiv.equiv_units_affine_map_symm_apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (ᾰ : P₁) :
@[simp]
theorem affine_equiv.vadd_const_symm_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (b p' : P₁) :
b).symm) p' = p' -ᵥ b
def affine_equiv.vadd_const (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ 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.vadd_const_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (b : P₁) (v : V₁) :
v = v +ᵥ b
@[simp]
theorem affine_equiv.linear_vadd_const (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (b : P₁) :
=
def affine_equiv.const_vsub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ 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) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (p : P₁) :
@[simp]
theorem affine_equiv.coe_const_vsub_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (p : P₁) :
p).symm) = λ (v : V₁), -v +ᵥ p
@[simp]
theorem affine_equiv.const_vadd_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v : V₁) (ᾰ : P₁) :
v) = v +ᵥ
def affine_equiv.const_vadd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ 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 `affine_map.const_vadd` as it is always an equivalence. This is roughly to `distrib_mul_action.to_linear_equiv` as `+ᵥ` is to `•`.

Equations
@[simp]
theorem affine_equiv.linear_const_vadd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v : V₁) :
v).linear =
@[simp]
theorem affine_equiv.const_vadd_zero (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
0 =
@[simp]
theorem affine_equiv.const_vadd_add (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v w : V₁) :
(v + w) = w).trans v)
@[simp]
theorem affine_equiv.const_vadd_symm (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v : V₁) :
v).symm = (-v)
@[simp]
theorem affine_equiv.const_vadd_hom_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v : multiplicative V₁) :
v =
def affine_equiv.const_vadd_hom (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] :
→* P₁ ≃ᵃ[k] P₁

A more bundled version of `affine_equiv.const_vadd`.

Equations
theorem affine_equiv.const_vadd_nsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (n : ) (v : V₁) :
(n v) = v ^ n
theorem affine_equiv.const_vadd_zsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (z : ) (v : V₁) :
(z v) = v ^ z
def affine_equiv.homothety_units_mul_hom {R : Type u_10} {V : Type u_11} {P : Type u_12} [comm_ring R] [ V] [ P] (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
@[simp]
theorem affine_equiv.coe_homothety_units_mul_hom_apply {R : Type u_10} {V : Type u_11} {P : Type u_12} [comm_ring R] [ V] [ P] (p : P) (t : Rˣ) :
@[simp]
theorem affine_equiv.coe_homothety_units_mul_hom_apply_symm {R : Type u_10} {V : Type u_11} {P : Type u_12} [comm_ring R] [ V] [ P] (p : P) (t : Rˣ) :
@[simp]
theorem affine_equiv.coe_homothety_units_mul_hom_eq_homothety_hom_coe {R : Type u_10} {V : Type u_11} {P : Type u_12} [comm_ring R] [ V] [ P] (p : P) :
def affine_equiv.point_reflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ 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) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (x y : P₁) :
= x -ᵥ y +ᵥ x
@[simp]
theorem affine_equiv.point_reflection_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (x : P₁) :
@[simp]
theorem affine_equiv.to_equiv_point_reflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (x : P₁) :
@[simp]
theorem affine_equiv.point_reflection_self (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (x : P₁) :
= x
theorem affine_equiv.point_reflection_involutive (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (x : P₁) :
theorem affine_equiv.point_reflection_fixed_iff_of_injective_bit0 (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] {x y : P₁}  :
= y y = x

`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) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (y : P₁) :
function.injective (λ (x : P₁), y)
theorem affine_equiv.injective_point_reflection_left_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [invertible 2] (y : P₁) :
function.injective (λ (x : P₁), y)
theorem affine_equiv.point_reflection_fixed_iff_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] [invertible 2] {x y : P₁} :
= y y = x
def linear_equiv.to_affine_equiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ 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_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] (e : V₁ ≃ₗ[k] V₂) :
theorem affine_map.line_map_vadd {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v v' : V₁) (p : P₁) (c : k) :
v') c +ᵥ p = (affine_map.line_map (v +ᵥ p) (v' +ᵥ p)) c
theorem affine_map.line_map_vsub {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (p₁ p₂ p₃ : P₁) (c : k) :
p₂) c -ᵥ p₃ = (affine_map.line_map (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c
theorem affine_map.vsub_line_map {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (p₁ p₂ p₃ : P₁) (c : k) :
p₁ -ᵥ p₃) c = (affine_map.line_map (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c
theorem affine_map.vadd_line_map {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [ V₁] [ P₁] (v : V₁) (p₁ p₂ : P₁) (c : k) :
v +ᵥ p₂) c = (affine_map.line_map (v +ᵥ p₁) (v +ᵥ p₂)) c
theorem affine_map.homothety_neg_one_apply {P₁ : Type u_2} {V₁ : Type u_6} [add_comm_group V₁] [ P₁] {R' : Type u_10} [comm_ring R'] [module R' V₁] (c p : P₁) :
(-1)) p = p