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

source

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

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.

toFun : P₁ → P₂
invFun : P₂ → P₁
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
linear : V₁ ≃ₗ[k] V₂
The underlying linear equiv of modules.
map_vadd' (p : P₁) (v : V₁) : self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p

Instances For

source

def «term_≃ᵃ[_]_» :

Lean.TrailingParserDescr

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

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [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

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [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 }

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

(↑e).linear = ↑e.linear

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

Function.Injective toAffineMap

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :

↑e = ↑e' ↔ e = e'

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [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' := ⋯ }

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂)

Equations

AffineEquiv.instCoeOutEquiv = { coe := AffineEquiv.toEquiv }

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) :

e (v +ᵥ p) = e.linear v +ᵥ e p

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

⇑e.toEquiv = ⇑e

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)

Equations

AffineEquiv.instCoeAffineMap = { coe := AffineEquiv.toAffineMap }

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

⇑↑e = ⇑e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

⇑↑e = ⇑e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

(↑e).linear = ↑e.linear

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ (x : P₁), e x = e' x) :

e = e'

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :

e = e' ↔ ∀ (x : P₁), e x = e' x

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

Function.Injective DFunLike.coe

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :

⇑e = ⇑e' ↔ e = e'

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

Function.Injective toEquiv

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} :

e.toEquiv = e'.toEquiv ↔ e = e'

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [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

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [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

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :

⇑(mk' (⇑e) e' p h) = ⇑e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :

(mk' (⇑e) e' p h).linear = e'

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [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

source

@[simp]

theorem AffineEquiv.toEquiv_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.symm.toEquiv = e.symm

source

@[deprecated "use instead `toEquiv_symm`, in the reverse direction" (since := "2025-06-08")]

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.symm = e.symm.toEquiv

source

@[simp]

theorem AffineEquiv.coe_symm_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

⇑e.symm = ⇑e.symm

source

@[simp]

theorem AffineEquiv.linear_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.symm.linear = e.linear.symm

source

@[deprecated "use instead `linear_symm`, in the reverse direction" (since := "2025-06-08")]

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.linear.symm = e.symm.linear

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

P₁ → P₂

See Note [custom simps projection]

Equations

AffineEquiv.Simps.apply e = ⇑e

Instances For

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

P₂ → P₁

See Note [custom simps projection]

Equations

AffineEquiv.Simps.symm_apply e = ⇑e.symm

Instances For

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

Function.Bijective ⇑e

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

Function.Surjective ⇑e

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

Function.Injective ⇑e

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) :

P₁ ≃ᵃ[k] P₂

Bijective affine maps are affine isomorphisms.

Equations

AffineEquiv.ofBijective hφ = { toEquiv := Equiv.ofBijective (⇑φ) hφ, linear := LinearEquiv.ofBijective φ.linear ⋯, map_vadd' := ⋯ }

Instances For

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) :

(ofBijective hφ).linear = LinearEquiv.ofBijective φ.linear ⋯

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) (a : P₁) :

(ofBijective hφ) a = φ a

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) :

(ofBijective hφ).symm.toEquiv = (Equiv.ofBijective (⇑φ) hφ).symm

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

Set.range ⇑e = Set.univ

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂) :

e (e.symm p) = p

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) :

e.symm (e p) = p

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₂} :

e p₁ = p₂ ↔ p₁ = e.symm p₂

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} :

e p₁ = e p₂ ↔ p₁ = p₂

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) :

⇑f.symm '' s = ⇑f ⁻¹' s

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) :

⇑f.symm ⁻¹' s = ⇑f '' s

source

def AffineEquiv.refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

P₁ ≃ᵃ[k] P₁

Identity map as an AffineEquiv.

Equations

AffineEquiv.refl k P₁ = { toEquiv := Equiv.refl P₁, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.coe_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

⇑(refl k P₁) = id

source

@[simp]

theorem AffineEquiv.coe_refl_to_affineMap (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

↑(refl k P₁) = AffineMap.id k P₁

source

@[simp]

theorem AffineEquiv.refl_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :

(refl k P₁) x = x

source

@[simp]

theorem AffineEquiv.toEquiv_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

(refl k P₁).toEquiv = Equiv.refl P₁

source

@[simp]

theorem AffineEquiv.linear_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

(refl k P₁).linear = LinearEquiv.refl k V₁

source

@[simp]

theorem AffineEquiv.symm_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

(refl k P₁).symm = refl k P₁

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [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

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :

⇑(e.trans e') = ⇑e' ∘ ⇑e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :

↑(e.trans e') = (↑e').comp ↑e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) :

(e.trans e') p = e' (e p)

source

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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [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₃)

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.trans (refl k P₂) = e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

(refl k P₁).trans e = e

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.trans e.symm = refl k P₁

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :

e.symm.trans e = refl k P₂

source

@[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] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :

e ((AffineMap.lineMap a b) c) = (AffineMap.lineMap (e a) (e b)) c

source

instance AffineEquiv.group {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

Group (P₁ ≃ᵃ[k] P₁)

Equations

One or more equations did not get rendered due to their size.

source

theorem AffineEquiv.one_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

1 = refl k P₁

source

@[simp]

theorem AffineEquiv.coe_one {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

⇑1 = id

source

theorem AffineEquiv.mul_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁) :

e * e' = e'.trans e

source

@[simp]

theorem AffineEquiv.coe_mul {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁) :

⇑(e * e') = ⇑e ∘ ⇑e'

source

theorem AffineEquiv.inv_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :

e⁻¹ = e.symm

source

def AffineEquiv.linearHom {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [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

source

@[simp]

theorem AffineEquiv.linearHom_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (self : P₁ ≃ᵃ[k] P₁) :

linearHom self = self.linear

source

def AffineEquiv.equivUnitsAffineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [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

source

@[simp]

theorem AffineEquiv.linear_equivUnitsAffineMap_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) :

(equivUnitsAffineMap.symm u).linear = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u)

source

@[simp]

theorem AffineEquiv.val_inv_equivUnitsAffineMap_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :

↑(equivUnitsAffineMap e)⁻¹ = ↑e.symm

source

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :

(equivUnitsAffineMap.symm u) a = ↑u a

source

@[simp]

theorem AffineEquiv.val_equivUnitsAffineMap_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) :

↑(equivUnitsAffineMap e) = ↑e

source

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :

(equivUnitsAffineMap.symm u).symm a = ↑u⁻¹ a

source

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_toFun {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :

(equivUnitsAffineMap.symm u) a = ↑u a

source

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_invFun {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) :

(equivUnitsAffineMap.symm u).invFun a = ↑u⁻¹ a

source

def AffineEquiv.prodCongr {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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) :

P₁ × P₃ ≃ᵃ[k] P₂ × P₄

Product of two affine equivalences. The map comes from Equiv.prodCongr

Equations

e₁.prodCongr e₂ = { toEquiv := (↑e₁).prodCongr ↑e₂, linear := e₁.linear.prodCongr e₂.linear, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.linear_prodCongr {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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) :

(e₁.prodCongr e₂).linear = e₁.linear.prodCongr e₂.linear

source

@[simp]

theorem AffineEquiv.prodCongr_symm {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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) :

(e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

source

@[simp]

theorem AffineEquiv.prodCongr_apply {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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) (p : P₁ × P₃) :

(e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)

source

@[simp]

theorem AffineEquiv.coe_prodCongr {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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) :

↑(e₁.prodCongr e₂) = (↑e₁).prodMap ↑e₂

source

def AffineEquiv.prodComm (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

P₁ × P₂ ≃ᵃ[k] P₂ × P₁

Product of affine spaces is commutative up to affine isomorphism.

Equations

AffineEquiv.prodComm k P₁ P₂ = { toEquiv := Equiv.prodComm P₁ P₂, linear := LinearEquiv.prodComm k V₁ V₂, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.linear_prodComm (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

(prodComm k P₁ P₂).linear = LinearEquiv.prodComm k V₁ V₂

source

@[simp]

theorem AffineEquiv.prodComm_apply (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (a✝ : P₁ × P₂) :

(prodComm k P₁ P₂) a✝ = a✝.swap

source

@[simp]

theorem AffineEquiv.prodComm_symm (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] :

(prodComm k P₁ P₂).symm = prodComm k P₂ P₁

source

def AffineEquiv.prodAssoc (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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] :

(P₁ × P₂) × P₃ ≃ᵃ[k] P₁ × P₂ × P₃

Product of affine spaces is associative up to affine isomorphism.

Equations

AffineEquiv.prodAssoc k P₁ P₂ P₃ = { toEquiv := Equiv.prodAssoc P₁ P₂ P₃, linear := LinearEquiv.prodAssoc k V₁ V₂ V₃, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.linear_prodAssoc (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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] :

(prodAssoc k P₁ P₂ P₃).linear = LinearEquiv.prodAssoc k V₁ V₂ V₃

source

@[simp]

theorem AffineEquiv.prodAssoc_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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (p : (P₁ × P₂) × P₃) :

(prodAssoc k P₁ P₂ P₃) p = (p.1.1, p.1.2, p.2)

source

@[simp]

theorem AffineEquiv.prodAssoc_symm_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] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (p : P₁ × P₂ × P₃) :

(prodAssoc k P₁ P₂ P₃).symm p = ((p.1, p.2.1), p.2.2)

source

def AffineEquiv.vaddConst (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [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

AffineEquiv.vaddConst k b = { toEquiv := Equiv.vaddConst b, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.vaddConst_symm_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b p' : P₁) :

(vaddConst k b).symm p' = p' -ᵥ b

source

@[simp]

theorem AffineEquiv.linear_vaddConst (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) :

(vaddConst k b).linear = LinearEquiv.refl k V₁

source

@[simp]

theorem AffineEquiv.vaddConst_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) (v : V₁) :

(vaddConst k b) v = v +ᵥ b

source

def AffineEquiv.constVSub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) :

P₁ ≃ᵃ[k] V₁

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

Equations

AffineEquiv.constVSub k p = { toEquiv := Equiv.constVSub p, linear := LinearEquiv.neg k, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.coe_constVSub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) :

⇑(constVSub k p) = fun (x : P₁) => p -ᵥ x

source

@[simp]

theorem AffineEquiv.coe_constVSub_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) :

⇑(constVSub k p).symm = fun (v : V₁) => -v +ᵥ p

source

def AffineEquiv.constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [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

AffineEquiv.constVAdd k P₁ v = { toEquiv := Equiv.constVAdd P₁ v, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.linear_constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) :

(constVAdd k P₁ v).linear = LinearEquiv.refl k V₁

source

@[simp]

theorem AffineEquiv.constVAdd_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (x✝ : P₁) :

(constVAdd k P₁ v) x✝ = v +ᵥ x✝

source

@[simp]

theorem AffineEquiv.constVAdd_zero (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

constVAdd k P₁ 0 = refl k P₁

source

@[simp]

theorem AffineEquiv.constVAdd_add (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v w : V₁) :

constVAdd k P₁ (v + w) = (constVAdd k P₁ w).trans (constVAdd k P₁ v)

source

@[simp]

theorem AffineEquiv.constVAdd_symm (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) :

(constVAdd k P₁ v).symm = constVAdd k P₁ (-v)

source

def AffineEquiv.constVAddHom (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] :

Multiplicative V₁ →* P₁ ≃ᵃ[k] P₁

A more bundled version of AffineEquiv.constVAdd.

Equations

AffineEquiv.constVAddHom k P₁ = { toFun := fun (v : Multiplicative V₁) => AffineEquiv.constVAdd k P₁ (Multiplicative.toAdd v), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AffineEquiv.constVAddHom_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : Multiplicative V₁) :

(constVAddHom k P₁) v = constVAdd k P₁ (Multiplicative.toAdd v)

source

theorem AffineEquiv.constVAdd_nsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (n : ℕ) (v : V₁) :

constVAdd k P₁ (n • v) = constVAdd k P₁ v ^ n

source

theorem AffineEquiv.constVAdd_zsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (z : ℤ) (v : V₁) :

constVAdd k P₁ (z • v) = constVAdd k P₁ v ^ z

source

def AffineEquiv.homothetyUnitsMulHom {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) :

Rˣ →* P ≃ᵃ[R] 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.homothetyUnitsMulHom p = AffineEquiv.equivUnitsAffineMap.symm.toMonoidHom.comp (Units.map (AffineMap.homothetyHom p))

Instances For

source

@[simp]

theorem AffineEquiv.coe_homothetyUnitsMulHom_apply {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) (t : Rˣ) :

⇑((homothetyUnitsMulHom p) t) = ⇑(AffineMap.homothety p ↑t)

source

@[simp]

theorem AffineEquiv.coe_homothetyUnitsMulHom_apply_symm {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) (t : Rˣ) :

⇑((homothetyUnitsMulHom p) t).symm = ⇑(AffineMap.homothety p ↑t⁻¹)

source

@[simp]

theorem AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) :

toAffineMap ∘ ⇑(homothetyUnitsMulHom p) = ⇑(AffineMap.homothetyHom p) ∘ Units.val

source

def AffineEquiv.pointReflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :

P₁ ≃ᵃ[k] P₁

Point reflection in x as a permutation.

Equations

AffineEquiv.pointReflection k x = (AffineEquiv.constVSub k x).trans (AffineEquiv.vaddConst k x)

Instances For

source

@[simp]

theorem AffineEquiv.pointReflection_apply_eq_equivPointReflection_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x y : P₁) :

(pointReflection k x) y = (Equiv.pointReflection x) y

source

theorem AffineEquiv.pointReflection_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x y : P₁) :

(pointReflection k x) y = (x -ᵥ y) +ᵥ x

source

@[simp]

theorem AffineEquiv.pointReflection_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :

(pointReflection k x).symm = pointReflection k x

source

@[simp]

theorem AffineEquiv.toEquiv_pointReflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :

(pointReflection k x).toEquiv = Equiv.pointReflection x

source

theorem AffineEquiv.pointReflection_self (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :

(pointReflection k x) x = x

source

theorem AffineEquiv.pointReflection_involutive (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) :

Function.Involutive ⇑(pointReflection k x)

source

theorem AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {x y : P₁} (h : Function.Injective fun (x : V₁) => 2 • x) :

(pointReflection k 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.

source

theorem AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (h : Function.Injective fun (x : V₁) => 2 • x) (y : P₁) :

Function.Injective fun (x : P₁) => (pointReflection k x) y

source

theorem AffineEquiv.injective_pointReflection_left_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [Invertible 2] (y : P₁) :

Function.Injective fun (x : P₁) => (pointReflection k x) y

source

theorem AffineEquiv.pointReflection_fixed_iff_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [Invertible 2] {x y : P₁} :

(pointReflection k x) y = y ↔ y = x

source

def LinearEquiv.toAffineEquiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [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

source

@[simp]

theorem LinearEquiv.coe_toAffineEquiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] (e : V₁ ≃ₗ[k] V₂) :

⇑e.toAffineEquiv = ⇑e

source

theorem AffineMap.lineMap_vadd {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v v' : V₁) (p : P₁) (c : k) :

(lineMap v v') c +ᵥ p = (lineMap (v +ᵥ p) (v' +ᵥ p)) c

source

theorem AffineMap.lineMap_vsub {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k) :

(lineMap p₁ p₂) c -ᵥ p₃ = (lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c

source

theorem AffineMap.vsub_lineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k) :

p₁ -ᵥ (lineMap p₂ p₃) c = (lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c

source

theorem AffineMap.vadd_lineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (p₁ p₂ : P₁) (c : k) :

v +ᵥ (lineMap p₁ p₂) c = (lineMap (v +ᵥ p₁) (v +ᵥ p₂)) c

source

theorem AffineMap.homothety_neg_one_apply {P₁ : Type u_2} {V₁ : Type u_6} [AddCommGroup V₁] [AddTorsor V₁ P₁] {R' : Type u_10} [CommRing R'] [Module R' V₁] (c p : P₁) :

(homothety c (-1)) p = (AffineEquiv.pointReflection R' c) p

Documentation

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Affine equivalences #

Tags #