mathlib3 documentation

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:

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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₁ P₂

See Note [custom simps projection]

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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
P₂ P₁

See Note [custom simps projection]

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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) (ᾰ : P₂) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) (ᾰ : P₁) :
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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] :
@[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₁] [module k V₁] [add_torsor V₁ 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₁] [module k V₁] [add_torsor V₁ P₁] (x : P₁) :
(affine_equiv.refl k 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₁] [module k V₁] [add_torsor V₁ P₁] :
@[simp]
theorem affine_equiv.linear_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] :
@[simp]
theorem affine_equiv.symm_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor 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} {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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor V₃ P₃] [add_comm_group V₄] [module k V₄] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :
@[protected, instance]
def affine_equiv.group {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] :
@[simp]
theorem affine_equiv.coe_one {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (self : P₁ ≃ᵃ[k] P₁) :
@[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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] :
(P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ

The group of affine_equivs 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₁] [module k V₁] [add_torsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (ᾰ : 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (b p' : P₁) :
def affine_equiv.vadd_const (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (b : P₁) (v : V₁) :
@[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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (p : P₁) :
((affine_equiv.const_vsub k 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₁] [module k V₁] [add_torsor V₁ P₁] (v : V₁) (ᾰ : P₁) :
(affine_equiv.const_vadd k 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (v : V₁) :
@[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₁] [module k V₁] [add_torsor V₁ P₁] :
@[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₁] [module k V₁] [add_torsor V₁ P₁] (v w : 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₁] [module k V₁] [add_torsor V₁ P₁] (v : 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₁] [module k V₁] [add_torsor V₁ P₁] (v : multiplicative 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₁] [module k V₁] [add_torsor V₁ P₁] :
multiplicative V₁ →* 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₁] [module k V₁] [add_torsor V₁ P₁] (n : ) (v : V₁) :
theorem affine_equiv.const_vadd_zsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] (z : ) (v : V₁) :
def affine_equiv.homothety_units_mul_hom {R : Type u_10} {V : Type u_11} {P : Type u_12} [comm_ring R] [add_comm_group V] [module R V] [add_torsor 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
def affine_equiv.point_reflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (x y : P₁) :
@[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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor V₁ P₁] (x : P₁) :
theorem affine_equiv.point_reflection_involutive (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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₁] [module k V₁] [add_torsor 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) {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] (h : function.injective bit0) (y : P₁) :
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₁] [module k V₁] [add_torsor V₁ P₁] [invertible 2] (y : P₁) :
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₁] [module k V₁] [add_torsor V₁ P₁] [invertible 2] {x y : P₁} :
def linear_equiv.to_affine_equiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [module k V₁] [add_comm_group V₂] [module 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_6} {V₂ : Type u_7} [ring k] [add_comm_group V₁] [module k V₁] [add_comm_group V₂] [module k 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₁] [module k V₁] [add_torsor V₁ P₁] (v v' : V₁) (p : P₁) (c : k) :
theorem affine_map.line_map_vsub {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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} {P₁ : Type u_2} {V₁ : Type u_6} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor 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 {P₁ : Type u_2} {V₁ : Type u_6} [add_comm_group V₁] [add_torsor V₁ P₁] {R' : Type u_10} [comm_ring R'] [module R' V₁] (c p : P₁) :