Affine equivalences

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

We define the following equivalences:

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

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

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

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

Tags

affine space, affine equivalence

structure AffineEquiv (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] extends Equiv : 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₂
• map_vadd' : ∀ (p : P₁) (v : V₁), self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p

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

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.

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

Reinterpret an AffineEquiv as an AffineMap.

Equations

• ↑e = { toFun := e.toFun, linear := ↑e.linear, map_vadd' := ⋯ }

@[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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p) : ↑{ toEquiv := f, linear := f', map_vadd' := h } = { toFun := ⇑f, linear := ↑f', map_vadd' := h }

@[simp]

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

theorem AffineEquiv.toAffineMap_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Function.Injective AffineEquiv.toAffineMap

@[simp]

theorem AffineEquiv.toAffineMap_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} : ↑e = ↑e' ↔ e = e'

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

Equations

• AffineEquiv.equivLike = { coe := fun (f : P₁ ≃ᵃ[k] P₂) => f.toFun, inv := fun (f : P₁ ≃ᵃ[k] P₂) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance AffineEquiv.instCoeFunForall {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : CoeFun (P₁ ≃ᵃ[k] P₂) fun (x : P₁ ≃ᵃ[k] P₂) => P₁ → P₂

Equations

• AffineEquiv.instCoeFunForall = DFunLike.hasCoeToFun

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

Equations

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

@[simp]

theorem AffineEquiv.map_vadd {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p

@[simp]

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

instance AffineEquiv.instCoeAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem AffineEquiv.coeFn_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Function.Injective DFunLike.coe

theorem AffineEquiv.coeFn_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} : ⇑e = ⇑e' ↔ e = e'

theorem AffineEquiv.toEquiv_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Function.Injective AffineEquiv.toEquiv

@[simp]

theorem AffineEquiv.toEquiv_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} : e.toEquiv = e'.toEquiv ↔ e = e'

@[simp]

theorem AffineEquiv.coe_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p) : ⇑{ toEquiv := e, linear := e', map_vadd' := h } = ⇑e

def AffineEquiv.mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) : P₁ ≃ᵃ[k] P₂

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

Equations

• AffineEquiv.mk' e e' p h = { toFun := e, invFun := fun (q' : P₂) => e'.symm (q' -ᵥ e p) +ᵥ p, left_inv := ⋯, right_inv := ⋯, linear := e', map_vadd' := ⋯ }

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

@[simp]

theorem AffineEquiv.linear_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) : (AffineEquiv.mk' (⇑e) e' p h).linear = e'

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

Inverse of an affine equivalence as an affine equivalence.

Equations

• e.symm = { toEquiv := e.symm, linear := e.linear.symm, map_vadd' := ⋯ }

@[simp]

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

@[simp]

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

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

See Note [custom simps projection]

Equations

• AffineEquiv.Simps.apply e = ⇑e

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

See Note [custom simps projection]

Equations

• AffineEquiv.Simps.symm_apply e = ⇑e.symm

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

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

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

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

@[simp]

theorem AffineEquiv.linear_ofBijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) : (AffineEquiv.ofBijective hφ).linear = LinearEquiv.ofBijective φ.linear ⋯

noncomputable def AffineEquiv.ofBijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) : P₁ ≃ᵃ[k] P₂

Bijective affine maps are affine isomorphisms.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem AffineEquiv.image_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : ⇑f.symm '' s = ⇑f ⁻¹' s

@[simp]

theorem AffineEquiv.preimage_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) : ⇑f.symm ⁻¹' s = ⇑f '' s

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

@[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₁] : ⇑(AffineEquiv.refl k P₁) = id

@[simp]

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

@[simp]

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

@[simp]

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

@[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₁] : (AffineEquiv.refl k P₁).linear = LinearEquiv.refl k V₁

@[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₁] : (AffineEquiv.refl k P₁).symm = AffineEquiv.refl k P₁

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

Composition of two AffineEquivalences, applied left to right.

Equations

• e.trans e' = { toEquiv := e.trans e'.toEquiv, linear := e.linear.trans e'.linear, map_vadd' := ⋯ }

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

@[simp]

theorem AffineEquiv.coe_trans_to_affineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ↑(e.trans e') = (↑e').comp ↑e

@[simp]

theorem AffineEquiv.trans_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) : (e.trans e') p = e' (e p)

theorem AffineEquiv.trans_assoc {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄) : (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• AffineEquiv.group = Group.mk ⋯

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 = AffineEquiv.refl k P₁

@[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

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 : P₁ ≃ᵃ[k] P₁) (e' : P₁ ≃ᵃ[k] P₁) : e * e' = e'.trans e

@[simp]

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

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

@[simp]

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

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

@[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₁) : (AffineEquiv.equivUnitsAffineMap.symm u).invFun a = ↑u⁻¹ a

@[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₁)ˣ) : (AffineEquiv.equivUnitsAffineMap.symm u).linear = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u)

@[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₁) : (AffineEquiv.equivUnitsAffineMap.symm u).symm a = ↑u⁻¹ a

@[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₁) : ↑(AffineEquiv.equivUnitsAffineMap e) = ↑e

@[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₁) : (AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a

@[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₁) : ↑(AffineEquiv.equivUnitsAffineMap e)⁻¹ = ↑e.symm

@[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₁) : (AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a

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.

@[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₁) : (AffineEquiv.vaddConst k b) v = v +ᵥ b

@[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₁) : (AffineEquiv.vaddConst k b).linear = LinearEquiv.refl k V₁

@[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' : P₁) : (AffineEquiv.vaddConst k b).symm p' = p' -ᵥ b

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' := ⋯ }

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' := ⋯ }

@[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₁) : ⇑(AffineEquiv.constVSub k p) = fun (x : P₁) => p -ᵥ x

@[simp]

theorem AffineEquiv.coe_constVSub_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) : ⇑(AffineEquiv.constVSub k p).symm = fun (v : V₁) => -v +ᵥ p

@[simp]

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

@[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₁), (AffineEquiv.constVAdd k P₁ v) x = v +ᵥ x

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

@[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₁] : AffineEquiv.constVAdd k P₁ 0 = AffineEquiv.refl k P₁

@[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 : V₁) (w : V₁) : AffineEquiv.constVAdd k P₁ (v + w) = (AffineEquiv.constVAdd k P₁ w).trans (AffineEquiv.constVAdd k P₁ v)

@[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₁) : (AffineEquiv.constVAdd k P₁ v).symm = AffineEquiv.constVAdd k P₁ (-v)

@[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₁) : (AffineEquiv.constVAddHom k P₁) v = AffineEquiv.constVAdd k P₁ (Multiplicative.toAdd v)

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' := ⋯ }

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₁) : AffineEquiv.constVAdd k P₁ (n • v) = AffineEquiv.constVAdd k P₁ v ^ n

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₁) : AffineEquiv.constVAdd k P₁ (z • v) = AffineEquiv.constVAdd k P₁ v ^ z

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))

@[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ˣ) : ⇑((AffineEquiv.homothetyUnitsMulHom p) t) = ⇑(AffineMap.homothety p ↑t)

@[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ˣ) : ⇑((AffineEquiv.homothetyUnitsMulHom p) t).symm = ⇑(AffineMap.homothety p ↑t⁻¹)

@[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) : AffineEquiv.toAffineMap ∘ ⇑(AffineEquiv.homothetyUnitsMulHom p) = ⇑(AffineMap.homothetyHom p) ∘ Units.val

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)

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 : P₁) (y : P₁) : (AffineEquiv.pointReflection k x) y = x -ᵥ y +ᵥ x

@[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₁) : (AffineEquiv.pointReflection k x).symm = AffineEquiv.pointReflection k x

@[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₁) : (AffineEquiv.pointReflection k x).toEquiv = Equiv.pointReflection x

@[simp]

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₁) : (AffineEquiv.pointReflection k x) x = x

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 ⇑(AffineEquiv.pointReflection k x)

theorem AffineEquiv.pointReflection_fixed_iff_of_injective_bit0 (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {x : P₁} {y : P₁} (h : Function.Injective bit0) : (AffineEquiv.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.

theorem AffineEquiv.injective_pointReflection_left_of_injective_bit0 (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 bit0) (y : P₁) : Function.Injective fun (x : P₁) => (AffineEquiv.pointReflection k x) y

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₁) => (AffineEquiv.pointReflection k x) y

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 : P₁} {y : P₁} : (AffineEquiv.pointReflection k x) y = y ↔ y = x

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

@[simp]

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

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

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

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

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

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