Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

AffineEquiv structure

(k P₁ P₂ : Type*) {V₁ V₂ : Type*} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂]
  [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] extends P₁ ≃ P₂

Full source

/-- 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. -/
structure AffineEquiv (k P₁ P₂ : Type*) {V₁ V₂ : Type*} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂]
  [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] extends P₁ ≃ P₂ where
  linear : V₁ ≃ₗ[k] V₂
  map_vadd' : ∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p

Affine equivalence between affine spaces

Informal description

An affine equivalence between two affine spaces $P₁$ and $P₂$ over a ring $k$, denoted $P₁ \simeqᵃ[k] P₂$, is an equivalence such that both the forward and inverse maps are affine transformations. Here, $V₁$ and $V₂$ are the associated vector spaces of $P₁$ and $P₂$ respectively, with $P₁$ being an additive torsor over $V₁$ and $P₂$ an additive torsor over $V₂$.

term_≃ᵃ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 P₁ " ≃ᵃ[" k:25 "] " P₂:0 => AffineEquiv k P₁ P₂

Affine equivalence notation

Informal description

The notation `P₁ ≃ᵃ[k] P₂` represents the type of affine equivalences between affine spaces `P₁` and `P₂` over the ring `k`. An affine equivalence is a bijection between `P₁` and `P₂` where both the forward and inverse maps are affine transformations.

AffineEquiv.toAffineMap definition

(e : P₁ ≃ᵃ[k] P₂) : P₁ →ᵃ[k] P₂

Full source

/-- Reinterpret an `AffineEquiv` as an `AffineMap`. -/
@[coe]
def toAffineMap (e : P₁ ≃ᵃ[k] P₂) : P₁ →ᵃ[k] P₂ :=
  { e with }

Affine equivalence as affine map

Informal description

Given an affine equivalence $e : P₁ \simeqᵃ[k] P₂$ between two affine spaces $P₁$ and $P₂$ over a ring $k$, the function `toAffineMap` reinterprets $e$ as an affine map from $P₁$ to $P₂$.

AffineEquiv.toAffineMap_mk theorem

(f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂) (h) : toAffineMap (mk f f' h) = ⟨f, f', h⟩

Full source

@[simp]
theorem toAffineMap_mk (f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂) (h) :
    toAffineMap (mk f f' h) = ⟨f, f', h⟩ :=
  rfl

Affine Map Representation of Constructed Affine Equivalence

Informal description

Given a bijection $f : P_1 \to P_2$ between affine spaces, a linear equivalence $f' : V_1 \simeq_{k} V_2$ between their associated vector spaces, and a compatibility condition $h$, the affine map associated to the affine equivalence constructed from $f$, $f'$, and $h$ is equal to the affine map $\langle f, f', h \rangle$.

AffineEquiv.linear_toAffineMap theorem

(e : P₁ ≃ᵃ[k] P₂) : e.toAffineMap.linear = e.linear

Full source

@[simp]
theorem linear_toAffineMap (e : P₁ ≃ᵃ[k] P₂) : e.toAffineMap.linear = e.linear :=
  rfl

Equality of Linear Parts in Affine Equivalence Representation

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the linear map associated with the affine map representation of $e$ is equal to the linear part of $e$ itself. That is, $\text{linear}(e.\text{toAffineMap}) = e.\text{linear}$.

AffineEquiv.toAffineMap_injective theorem

: Injective (toAffineMap : (P₁ ≃ᵃ[k] P₂) → P₁ →ᵃ[k] P₂)

Full source

theorem toAffineMap_injective : Injective (toAffineMap : (P₁ ≃ᵃ[k] P₂) → P₁ →ᵃ[k] P₂) := by
  rintro ⟨e, el, h⟩ ⟨e', el', h'⟩ H
  simp_all

Injectivity of the Affine Equivalence to Affine Map Conversion

Informal description

The function `toAffineMap` from affine equivalences $P₁ \simeqᵃ[k] P₂$ to affine maps $P₁ →ᵃ[k] P₂$ is injective. That is, for any two affine equivalences $e, e' \colon P₁ \simeqᵃ[k] P₂$, if $e.\text{toAffineMap} = e'.\text{toAffineMap}$, then $e = e'$.

AffineEquiv.toAffineMap_inj theorem

{e e' : P₁ ≃ᵃ[k] P₂} : e.toAffineMap = e'.toAffineMap ↔ e = e'

Full source

@[simp]
theorem toAffineMap_inj {e e' : P₁ ≃ᵃ[k] P₂} : e.toAffineMap = e'.toAffineMap ↔ e = e' :=
  toAffineMap_injective.eq_iff

Affine Equivalence to Affine Map Conversion is Injective

Informal description

For any two affine equivalences $e, e' \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the affine maps associated with $e$ and $e'$ are equal if and only if $e = e'$. That is, $e.\text{toAffineMap} = e'.\text{toAffineMap} \leftrightarrow e = e'$.

AffineEquiv.equivLike instance

: EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂

Full source

instance equivLike : EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂ where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' _ _ h _ := toAffineMap_injective (DFunLike.coe_injective h)

Affine Equivalences as Type Equivalences

Informal description

For any affine equivalence $P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying map can be viewed as an equivalence (bijection) between the types $P₁$ and $P₂$.

AffineEquiv.instCoeOutEquiv instance

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

Full source

instance : CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂) :=
  ⟨AffineEquiv.toEquiv⟩

Affine Equivalence as Type Equivalence

Informal description

Every affine equivalence $P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$ can be naturally viewed as an equivalence $P₁ \simeq P₂$ (a bijection with inverse).

AffineEquiv.map_vadd theorem

(e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p

Full source

@[simp]
theorem map_vadd (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p :=
  e.map_vadd' p v

Affine Equivalence Preserves Vector Addition on Points

Informal description

Let $e \colon P₁ \simeqᵃ[k] P₂$ be an affine equivalence between affine spaces $P₁$ and $P₂$ over a ring $k$. For any point $p \in P₁$ and vector $v \in V₁$, the action of $e$ on the sum $v +ᵥ p$ is given by $e(v +ᵥ p) = e.linear(v) +ᵥ e(p)$, where $e.linear$ denotes the linear part of $e$.

AffineEquiv.coe_toEquiv theorem

(e : P₁ ≃ᵃ[k] P₂) : ⇑e.toEquiv = e

Full source

@[simp]
theorem coe_toEquiv (e : P₁ ≃ᵃ[k] P₂) : ⇑e.toEquiv = e :=
  rfl

Underlying Function of Affine Equivalence Matches the Equivalence

Informal description

For any affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying function of the equivalence $e.\text{toEquiv}$ is equal to $e$ itself.

AffineEquiv.instCoeAffineMap instance

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

Full source

instance : Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂) :=
  ⟨toAffineMap⟩

Affine Equivalence as Affine Map

Informal description

Every affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$ can be naturally interpreted as an affine map from $P₁$ to $P₂$.

AffineEquiv.coe_toAffineMap theorem

(e : P₁ ≃ᵃ[k] P₂) : (e.toAffineMap : P₁ → P₂) = (e : P₁ → P₂)

Full source

@[simp]
theorem coe_toAffineMap (e : P₁ ≃ᵃ[k] P₂) : (e.toAffineMap : P₁ → P₂) = (e : P₁ → P₂) :=
  rfl

Underlying Function of Affine Map from Affine Equivalence

Informal description

For any affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying function of the affine map $e.\text{toAffineMap}$ is equal to the underlying function of $e$ itself.

AffineEquiv.coe_coe theorem

(e : P₁ ≃ᵃ[k] P₂) : ((e : P₁ →ᵃ[k] P₂) : P₁ → P₂) = e

Full source

@[norm_cast, simp]
theorem coe_coe (e : P₁ ≃ᵃ[k] P₂) : ((e : P₁ →ᵃ[k] P₂) : P₁ → P₂) = e :=
  rfl

Coercion Consistency of Affine Equivalence to Point Function

Informal description

For any affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying point function obtained by first coercing $e$ to an affine map and then to a point function is equal to $e$ itself as a function.

AffineEquiv.coe_linear theorem

(e : P₁ ≃ᵃ[k] P₂) : (e : P₁ →ᵃ[k] P₂).linear = e.linear

Full source

@[simp]
theorem coe_linear (e : P₁ ≃ᵃ[k] P₂) : (e : P₁ →ᵃ[k] P₂).linear = e.linear :=
  rfl

Equality of Linear Parts in Affine Equivalence

Informal description

For any affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the linear part of the associated affine map $e \colon P₁ \toᵃ[k] P₂$ is equal to the linear part of $e$ itself.

AffineEquiv.ext theorem

{e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ x, e x = e' x) : e = e'

Full source

@[ext]
theorem ext {e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ x, e x = e' x) : e = e' :=
  DFunLike.ext _ _ h

Extensionality of Affine Equivalences

Informal description

For any two affine equivalences $e, e' \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, if $e(x) = e'(x)$ for all $x \in P₁$, then $e = e'$.

AffineEquiv.coeFn_injective theorem

: @Injective (P₁ ≃ᵃ[k] P₂) (P₁ → P₂) (⇑)

Full source

theorem coeFn_injective : @Injective (P₁ ≃ᵃ[k] P₂) (P₁ → P₂) (⇑) :=
  DFunLike.coe_injective

Injectivity of the Affine Equivalence to Function Map

Informal description

The canonical map from the type of affine equivalences $P₁ \simeqᵃ[k] P₂$ to the type of functions $P₁ \to P₂$ is injective. That is, if two affine equivalences $e, e' \colon P₁ \simeqᵃ[k] P₂$ satisfy $e(x) = e'(x)$ for all $x \in P₁$, then $e = e'$.

AffineEquiv.coeFn_inj theorem

{e e' : P₁ ≃ᵃ[k] P₂} : (e : P₁ → P₂) = e' ↔ e = e'

Full source

@[norm_cast]
theorem coeFn_inj {e e' : P₁ ≃ᵃ[k] P₂} : (e : P₁ → P₂) = e' ↔ e = e' := by simp

Equality of Affine Equivalences via Underlying Functions

Informal description

For any two affine equivalences $e, e' \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying functions $e, e' \colon P₁ \to P₂$ are equal if and only if the affine equivalences $e$ and $e'$ themselves are equal.

AffineEquiv.toEquiv_injective theorem

: Injective (toEquiv : (P₁ ≃ᵃ[k] P₂) → P₁ ≃ P₂)

Full source

theorem toEquiv_injective : Injective (toEquiv : (P₁ ≃ᵃ[k] P₂) → P₁ ≃ P₂) := fun _ _ H =>
  ext <| Equiv.ext_iff.1 H

Injectivity of the Underlying Equivalence Map for Affine Equivalences

Informal description

The map that takes an affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ to its underlying equivalence $e.\text{toEquiv} \colon P₁ \simeq P₂$ is injective. That is, if two affine equivalences have the same underlying equivalence, then they are equal.

AffineEquiv.toEquiv_inj theorem

{e e' : P₁ ≃ᵃ[k] P₂} : e.toEquiv = e'.toEquiv ↔ e = e'

Full source

@[simp]
theorem toEquiv_inj {e e' : P₁ ≃ᵃ[k] P₂} : e.toEquiv = e'.toEquiv ↔ e = e' :=
  toEquiv_injective.eq_iff

Equality of Affine Equivalences via Underlying Equivalences

Informal description

For any two affine equivalences $e, e' \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying equivalences $e.\text{toEquiv}$ and $e'.\text{toEquiv}$ are equal if and only if $e = e'$.

AffineEquiv.coe_mk theorem

(e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (h) : ((⟨e, e', h⟩ : P₁ ≃ᵃ[k] P₂) : P₁ → P₂) = e

Full source

@[simp]
theorem coe_mk (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (h) : ((⟨e, e', h⟩ : P₁ ≃ᵃ[k] P₂) : P₁ → P₂) = e :=
  rfl

Underlying Function of Affine Equivalence Construction

Informal description

Given an equivalence $e \colon P_1 \to P_2$ between affine spaces, a linear equivalence $e' \colon V_1 \simeq V_2$ between their associated vector spaces, and a condition $h$ ensuring compatibility, the underlying function of the affine equivalence $\langle e, e', h \rangle \colon P_1 \simeqᵃ[k] P_2$ is equal to $e$.

AffineEquiv.mk' definition

 (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ p' : P₁, e p' = e' (p' -ᵥ p) +ᵥ e p) : P₁ ≃ᵃ[k] P₂

Full source

/-- 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`. -/
def mk' (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ p' : P₁, e p' = e' (p' -ᵥ p) +ᵥ e p) :
    P₁ ≃ᵃ[k] P₂ where
  toFun := e
  invFun := fun q' : P₂ => e'.symm (q' -ᵥ e p) +ᵥ p
  left_inv p' := by simp [h p', vadd_vsub, vsub_vadd]
  right_inv q' := by simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), vadd_vsub, vsub_vadd]
  linear := e'
  map_vadd' p' v := by simp [h p', h (v +ᵥ p'), vadd_vsub_assoc, vadd_vadd]

Construction of affine equivalence from point condition

Informal description

Given a map $e \colon P_1 \to P_2$ between affine spaces, a linear equivalence $e' \colon V_1 \simeq V_2$ between their associated vector spaces, and a point $p \in P_1$ such that for every point $p' \in P_1$ the relation $e(p') = e'(p' - p) + e(p)$ holds, we can construct an affine equivalence between $P_1$ and $P_2$. Here, $P_1$ is an affine space over $V_1$ and $P_2$ is an affine space over $V_2$, both over a ring $k$. The inverse map is given by $q' \mapsto e'^{-1}(q' - e(p)) + p$, and the linear part of the affine equivalence is $e'$.

AffineEquiv.coe_mk' theorem

(e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p h) : ⇑(mk' e e' p h) = e

Full source

@[simp]
theorem coe_mk' (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p h) : ⇑(mk' e e' p h) = e :=
  rfl

Underlying Function of Constructed Affine Equivalence via `mk'`

Informal description

Given an equivalence $e \colon P_1 \to P_2$ between affine spaces, a linear equivalence $e' \colon V_1 \simeq V_2$ between their associated vector spaces, a point $p \in P_1$, and a condition $h$ ensuring compatibility, the underlying function of the affine equivalence constructed via `mk'` is equal to $e$.

AffineEquiv.linear_mk' theorem

(e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p h) : (mk' e e' p h).linear = e'

Full source

@[simp]
theorem linear_mk' (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p h) : (mk' e e' p h).linear = e' :=
  rfl

Linear Part of Constructed Affine Equivalence Equals Given Linear Equivalence

Informal description

Given an affine equivalence $e \colon P_1 \simeq P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, a linear equivalence $e' \colon V_1 \simeq V_2$ between their associated vector spaces, a point $p \in P_1$, and a condition $h$ ensuring the affine behavior of $e$, the linear part of the constructed affine equivalence $\text{mk'}(e, e', p, h)$ is equal to $e'$.

AffineEquiv.symm definition

(e : P₁ ≃ᵃ[k] P₂) : P₂ ≃ᵃ[k] P₁

Full source

/-- Inverse of an affine equivalence as an affine equivalence. -/
@[symm]
def symm (e : P₁ ≃ᵃ[k] P₂) : P₂ ≃ᵃ[k] P₁ where
  toEquiv := e.toEquiv.symm
  linear := e.linear.symm
  map_vadd' p v :=
    e.toEquiv.symm.apply_eq_iff_eq_symm_apply.2 <| by
      rw [Equiv.symm_symm, e.map_vadd' ((Equiv.symm e.toEquiv) p) ((LinearEquiv.symm e.linear) v),
        LinearEquiv.apply_symm_apply, Equiv.apply_symm_apply]

Inverse affine equivalence

Informal description

Given an affine equivalence $e : P₁ \simeqᵃ[k] P₂$ between two affine spaces $P₁$ and $P₂$ over a ring $k$, the inverse affine equivalence $e^{-1} : P₂ \simeqᵃ[k] P₁$ is defined by taking the inverse of the underlying equivalence and the inverse of the associated linear equivalence. This ensures that both the forward and inverse maps of $e^{-1}$ are affine transformations.

AffineEquiv.symm_toEquiv theorem

(e : P₁ ≃ᵃ[k] P₂) : e.toEquiv.symm = e.symm.toEquiv

Full source

@[simp]
theorem symm_toEquiv (e : P₁ ≃ᵃ[k] P₂) : e.toEquiv.symm = e.symm.toEquiv :=
  rfl

Inverse of Underlying Equivalence in Affine Equivalence

Informal description

For any affine equivalence $e : P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the inverse of the underlying equivalence $e.\text{toEquiv}$ is equal to the underlying equivalence of the inverse affine equivalence $e^{-1}.\text{toEquiv}$. In other words, $(e^{-1}).\text{toEquiv} = (e.\text{toEquiv})^{-1}$.

AffineEquiv.symm_linear theorem

(e : P₁ ≃ᵃ[k] P₂) : e.linear.symm = e.symm.linear

Full source

@[simp]
theorem symm_linear (e : P₁ ≃ᵃ[k] P₂) : e.linear.symm = e.symm.linear :=
  rfl

Inverse of Linear Map in Affine Equivalence

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the linear map associated to the inverse equivalence $e^{-1}$ is equal to the inverse of the linear map associated to $e$. In other words, $(e^{-1})_{\text{linear}} = (e_{\text{linear}})^{-1}$.

AffineEquiv.Simps.apply definition

(e : P₁ ≃ᵃ[k] P₂) : P₁ → P₂

Full source

/-- See Note [custom simps projection] -/
def Simps.apply (e : P₁ ≃ᵃ[k] P₂) : P₁ → P₂ :=
  e

Application of an affine equivalence

Informal description

The function that applies an affine equivalence $e : P₁ \simeqᵃ[k] P₂$ to a point in $P₁$, yielding a point in $P₂$.

AffineEquiv.Simps.symm_apply definition

(e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁ :=
  e.symm

Inverse application of an affine equivalence

Informal description

The function that applies the inverse of an affine equivalence $e : P₁ \simeqᵃ[k] P₂$ to a point in $P₂$, yielding a point in $P₁$.

AffineEquiv.bijective theorem

(e : P₁ ≃ᵃ[k] P₂) : Bijective e

Full source

protected theorem bijective (e : P₁ ≃ᵃ[k] P₂) : Bijective e :=
  e.toEquiv.bijective

Bijectivity of Affine Equivalences

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the underlying map $e \colon P_1 \to P_2$ is bijective.

AffineEquiv.surjective theorem

(e : P₁ ≃ᵃ[k] P₂) : Surjective e

Full source

protected theorem surjective (e : P₁ ≃ᵃ[k] P₂) : Surjective e :=
  e.toEquiv.surjective

Surjectivity of Affine Equivalences

Informal description

For any affine equivalence $e : P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying map $e : P₁ \to P₂$ is surjective.

AffineEquiv.injective theorem

(e : P₁ ≃ᵃ[k] P₂) : Injective e

Full source

protected theorem injective (e : P₁ ≃ᵃ[k] P₂) : Injective e :=
  e.toEquiv.injective

Injectivity of Affine Equivalences

Informal description

For any affine equivalence $e : P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the underlying map $e : P₁ \to P₂$ is injective.

AffineEquiv.ofBijective definition

{φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective φ) : P₁ ≃ᵃ[k] P₂

Full source

/-- Bijective affine maps are affine isomorphisms. -/
@[simps! linear apply]
noncomputable def ofBijective {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective φ) : P₁ ≃ᵃ[k] P₂ :=
  { Equiv.ofBijective _ hφ with
    linear := LinearEquiv.ofBijective φ.linear (φ.linear_bijective_iff.mpr hφ)
    map_vadd' := φ.map_vadd }

Affine equivalence from a bijective affine map

Informal description

Given a bijective affine map $\varphi : P₁ \to P₂$ between affine spaces over a ring $k$, the structure `AffineEquiv.ofBijective` constructs an affine equivalence $P₁ \simeqᵃ[k] P₂$ with $\varphi$ as the forward map and its inverse as the backward map. The linear part of this equivalence is constructed from the bijective linear map associated with $\varphi$.

AffineEquiv.ofBijective.symm_eq theorem

 {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective φ) : (ofBijective hφ).symm.toEquiv = (Equiv.ofBijective _ hφ).symm

Full source

theorem ofBijective.symm_eq {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective φ) :
    (ofBijective hφ).symm.toEquiv = (Equiv.ofBijective _ hφ).symm :=
  rfl

Inverse of Bijective Affine Equivalence Preserves Underlying Equivalence

Informal description

Given a bijective affine map $\varphi \colon P_1 \to P_2$ between affine spaces over a ring $k$, the underlying equivalence of the inverse affine equivalence $\text{ofBijective}(h_\varphi)^{-1}$ is equal to the inverse of the equivalence $\text{ofBijective}(\varphi)$ constructed from $\varphi$.

AffineEquiv.range_eq theorem

(e : P₁ ≃ᵃ[k] P₂) : range e = univ

Full source

theorem range_eq (e : P₁ ≃ᵃ[k] P₂) : range e = univ := by simp

Range of Affine Equivalence is Universal Set

Informal description

For any affine equivalence $e : P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, the range of $e$ is equal to the universal set of $P₂$.

AffineEquiv.apply_symm_apply theorem

(e : P₁ ≃ᵃ[k] P₂) (p : P₂) : e (e.symm p) = p

Full source

@[simp]
theorem apply_symm_apply (e : P₁ ≃ᵃ[k] P₂) (p : P₂) : e (e.symm p) = p :=
  e.toEquiv.apply_symm_apply p

Affine Equivalence Recovery: $e(e^{-1}(p)) = p$

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, and for any point $p \in P_2$, applying $e$ to the inverse image $e^{-1}(p)$ yields $p$, i.e., $e(e^{-1}(p)) = p$.

AffineEquiv.symm_apply_apply theorem

(e : P₁ ≃ᵃ[k] P₂) (p : P₁) : e.symm (e p) = p

Full source

@[simp]
theorem symm_apply_apply (e : P₁ ≃ᵃ[k] P₂) (p : P₁) : e.symm (e p) = p :=
  e.toEquiv.symm_apply_apply p

Inverse Affine Equivalence Recovers Original Point

Informal description

For any affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, and for any point $p \in P₁$, applying the inverse equivalence $e^{-1}$ to the image $e(p)$ recovers the original point $p$, i.e., $e^{-1}(e(p)) = p$.

AffineEquiv.apply_eq_iff_eq_symm_apply theorem

(e : P₁ ≃ᵃ[k] P₂) {p₁ p₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂

Full source

theorem apply_eq_iff_eq_symm_apply (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂ :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

Affine Equivalence Characterization: $e(p_1) = p_2 \leftrightarrow p_1 = e^{-1}(p_2)$

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, and for any points $p_1 \in P_1$ and $p_2 \in P_2$, the equality $e(p_1) = p_2$ holds if and only if $p_1 = e^{-1}(p_2)$.

AffineEquiv.apply_eq_iff_eq theorem

(e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} : e p₁ = e p₂ ↔ p₁ = p₂

Full source

theorem apply_eq_iff_eq (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} : e p₁ = e p₂ ↔ p₁ = p₂ := by simp

Affine equivalence preserves equality

Informal description

For any affine equivalence $e \colon P₁ \simeqᵃ[k] P₂$ between affine spaces $P₁$ and $P₂$ over a ring $k$, and for any points $p₁, p₂ \in P₁$, the images $e(p₁)$ and $e(p₂)$ are equal if and only if $p₁ = p₂$.

AffineEquiv.image_symm theorem

(f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : f.symm '' s = f ⁻¹' s

Full source

@[simp]
theorem image_symm (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : f.symm '' s = f ⁻¹' s :=
  f.symm.toEquiv.image_eq_preimage _

Image-Preimage Symmetry for Affine Equivalences

Informal description

For any affine equivalence $f \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, and for any subset $s \subseteq P_2$, the image of $s$ under the inverse affine equivalence $f^{-1}$ is equal to the preimage of $s$ under $f$, i.e., \[ f^{-1}(s) = f^{-1}(s). \]

AffineEquiv.preimage_symm theorem

(f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) : f.symm ⁻¹' s = f '' s

Full source

@[simp]
theorem preimage_symm (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) : f.symm ⁻¹' s = f '' s :=
  (f.symm.image_symm _).symm

Preimage-Image Symmetry for Affine Equivalences

Informal description

For any affine equivalence $f \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, and for any subset $s \subseteq P_1$, the preimage of $s$ under the inverse affine equivalence $f^{-1}$ is equal to the image of $s$ under $f$, i.e., \[ f^{-1}(s) = f(s). \]

AffineEquiv.refl definition

: P₁ ≃ᵃ[k] P₁

Full source

/-- Identity map as an `AffineEquiv`. -/
@[refl]
def refl : P₁ ≃ᵃ[k] P₁ where
  toEquiv := Equiv.refl P₁
  linear := LinearEquiv.refl k V₁
  map_vadd' _ _ := rfl

Identity affine equivalence

Informal description

The identity affine equivalence from an affine space $P_1$ to itself over a ring $k$, where the underlying equivalence is the identity map and the linear part is the identity linear equivalence on the associated vector space $V_1$.

AffineEquiv.coe_refl theorem

: ⇑(refl k P₁) = id

Full source

@[simp]
theorem coe_refl : ⇑(refl k P₁) = id :=
  rfl

Identity Affine Equivalence as Identity Function

Informal description

The underlying function of the identity affine equivalence $\mathrm{refl}_k P_1$ from an affine space $P_1$ to itself over a ring $k$ is equal to the identity function $\mathrm{id}$ on $P_1$.

AffineEquiv.coe_refl_to_affineMap theorem

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

Full source

@[simp]
theorem coe_refl_to_affineMap : ↑(refl k P₁) = AffineMap.id k P₁ :=
  rfl

Identity Affine Equivalence Coerces to Identity Affine Map

Informal description

The coercion of the identity affine equivalence $\text{refl}_k P_1$ to an affine map is equal to the identity affine map $\text{id}_k P_1$ on the affine space $P_1$ over the ring $k$.

AffineEquiv.refl_apply theorem

(x : P₁) : refl k P₁ x = x

Full source

@[simp]
theorem refl_apply (x : P₁) : refl k P₁ x = x :=
  rfl

Identity Affine Equivalence Acts as Identity Map

Informal description

For any point $x$ in the affine space $P_1$ over a ring $k$, the identity affine equivalence $\text{refl}_k P_1$ maps $x$ to itself, i.e., $\text{refl}_k P_1(x) = x$.

AffineEquiv.toEquiv_refl theorem

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

Full source

@[simp]
theorem toEquiv_refl : (refl k P₁).toEquiv = Equiv.refl P₁ :=
  rfl

Identity Affine Equivalence Yields Identity Underlying Equivalence

Informal description

The underlying equivalence of the identity affine equivalence from an affine space $P_1$ to itself over a ring $k$ is equal to the identity equivalence on $P_1$.

AffineEquiv.linear_refl theorem

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

Full source

@[simp]
theorem linear_refl : (refl k P₁).linear = LinearEquiv.refl k V₁ :=
  rfl

Linear Part of Identity Affine Equivalence is Identity Linear Equivalence

Informal description

The linear part of the identity affine equivalence from an affine space $P_1$ to itself over a ring $k$ is equal to the identity linear equivalence on the associated vector space $V_1$.

AffineEquiv.symm_refl theorem

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

Full source

@[simp]
theorem symm_refl : (refl k P₁).symm = refl k P₁ :=
  rfl

Inverse of Identity Affine Equivalence is Identity

Informal description

The inverse of the identity affine equivalence from an affine space $P_1$ to itself over a ring $k$ is equal to the identity affine equivalence.

AffineEquiv.trans definition

(e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : P₁ ≃ᵃ[k] P₃

Full source

/-- Composition of two `AffineEquiv`alences, applied left to right. -/
@[trans]
def trans (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : P₁ ≃ᵃ[k] P₃ where
  toEquiv := e.toEquiv.trans e'.toEquiv
  linear := e.linear.trans e'.linear
  map_vadd' p v := by
    simp only [LinearEquiv.trans_apply, coe_toEquiv, (· ∘ ·), Equiv.coe_trans, map_vadd]

Composition of affine equivalences

Informal description

Given two affine equivalences $e : P₁ \simeqᵃ[k] P₂$ and $e' : P₂ \simeqᵃ[k] P₃$, their composition $e \circ e'$ forms an affine equivalence $P₁ \simeqᵃ[k] P₃$. The underlying equivalence is the composition of the underlying equivalences of $e$ and $e'$, and the linear part is the composition of their linear parts.

AffineEquiv.coe_trans theorem

(e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ⇑(e.trans e') = e' ∘ e

Full source

@[simp]
theorem coe_trans (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ⇑(e.trans e') = e' ∘ e :=
  rfl

Composition of Affine Equivalences as Function Composition

Informal description

For any affine equivalences $e \colon P_1 \simeqᵃ[k] P_2$ and $e' \colon P_2 \simeqᵃ[k] P_3$ between affine spaces over a ring $k$, the underlying function of their composition $e \circ e'$ is equal to the composition of their underlying functions, i.e., $(e \circ e')(p) = e'(e(p))$ for all $p \in P_1$.

AffineEquiv.coe_trans_to_affineMap theorem

 (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : (e.trans e' : P₁ →ᵃ[k] P₃) = (e' : P₂ →ᵃ[k] P₃).comp e

Full source

@[simp]
theorem coe_trans_to_affineMap (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) :
    (e.trans e' : P₁ →ᵃ[k] P₃) = (e' : P₂ →ᵃ[k] P₃).comp e :=
  rfl

Composition of Affine Equivalences as Affine Map Composition

Informal description

Let $e : P₁ \simeqᵃ[k] P₂$ and $e' : P₂ \simeqᵃ[k] P₃$ be affine equivalences between affine spaces over a ring $k$. Then the affine map obtained by composing $e$ and $e'$ is equal to the composition of the underlying affine maps, i.e., $(e \circ e') = e' \circ e$ as affine maps from $P₁$ to $P₃$.

AffineEquiv.trans_apply theorem

(e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) : e.trans e' p = e' (e p)

Full source

@[simp]
theorem trans_apply (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) : e.trans e' p = e' (e p) :=
  rfl

Composition of Affine Equivalences Evaluated at a Point

Informal description

Let $P₁$, $P₂$, and $P₃$ be affine spaces over a ring $k$, and let $e : P₁ \simeqᵃ[k] P₂$ and $e' : P₂ \simeqᵃ[k] P₃$ be affine equivalences. For any point $p \in P₁$, the composition $e \circ e'$ evaluated at $p$ equals $e'$ evaluated at $e(p)$, i.e., $(e \circ e')(p) = e'(e(p))$.

AffineEquiv.trans_assoc theorem

 (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄) : (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)

Full source

theorem trans_assoc (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄) :
    (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃) :=
  ext fun _ => rfl

Associativity of Composition of Affine Equivalences

Informal description

For any affine equivalences $e₁ \colon P₁ \simeqᵃ[k] P₂$, $e₂ \colon P₂ \simeqᵃ[k] P₃$, and $e₃ \colon P₃ \simeqᵃ[k] P₄$ over a ring $k$, the composition of affine equivalences is associative, i.e., $(e₁ \circ e₂) \circ e₃ = e₁ \circ (e₂ \circ e₃)$.

AffineEquiv.trans_refl theorem

(e : P₁ ≃ᵃ[k] P₂) : e.trans (refl k P₂) = e

Full source

@[simp]
theorem trans_refl (e : P₁ ≃ᵃ[k] P₂) : e.trans (refl k P₂) = e :=
  ext fun _ => rfl

Right Identity Law for Affine Equivalence Composition

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the composition of $e$ with the identity affine equivalence on $P_2$ is equal to $e$ itself.

AffineEquiv.refl_trans theorem

(e : P₁ ≃ᵃ[k] P₂) : (refl k P₁).trans e = e

Full source

@[simp]
theorem refl_trans (e : P₁ ≃ᵃ[k] P₂) : (refl k P₁).trans e = e :=
  ext fun _ => rfl

Identity Affine Equivalence Acts as Left Identity under Composition

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the composition of the identity affine equivalence on $P_1$ with $e$ is equal to $e$ itself. That is, $\text{refl}_k P_1 \circ e = e$.

AffineEquiv.self_trans_symm theorem

(e : P₁ ≃ᵃ[k] P₂) : e.trans e.symm = refl k P₁

Full source

@[simp]
theorem self_trans_symm (e : P₁ ≃ᵃ[k] P₂) : e.trans e.symm = refl k P₁ :=
  ext e.symm_apply_apply

Composition of Affine Equivalence with Its Inverse Yields Identity

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity affine equivalence on $P_1$.

AffineEquiv.symm_trans_self theorem

(e : P₁ ≃ᵃ[k] P₂) : e.symm.trans e = refl k P₂

Full source

@[simp]
theorem symm_trans_self (e : P₁ ≃ᵃ[k] P₂) : e.symm.trans e = refl k P₂ :=
  ext e.apply_symm_apply

Inverse Composition Yields Identity: $e^{-1} \circ e = \text{id}$

Informal description

For any affine equivalence $e \colon P_1 \simeqᵃ[k] P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the composition of the inverse equivalence $e^{-1}$ with $e$ yields the identity affine equivalence on $P_2$, i.e., $e^{-1} \circ e = \text{id}_{P_2}$.

AffineEquiv.apply_lineMap theorem

(e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) : e (AffineMap.lineMap a b c) = AffineMap.lineMap (e a) (e b) c

Full source

@[simp]
theorem apply_lineMap (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :
    e (AffineMap.lineMap a b c) = AffineMap.lineMap (e a) (e b) c :=
  e.toAffineMap.apply_lineMap a b c

Affine Equivalence Preserves Affine Combinations

Informal description

Let $e \colon P_1 \simeqᵃ[k] P_2$ be an affine equivalence between affine spaces $P_1$ and $P_2$ over a ring $k$. For any points $a, b \in P_1$ and scalar $c \in k$, the image under $e$ of the affine combination $\text{lineMap}(a, b, c)$ equals the affine combination $\text{lineMap}(e(a), e(b), c)$ in $P_2$. That is, $$ e(\text{lineMap}(a, b, c)) = \text{lineMap}(e(a), e(b), c). $$

AffineEquiv.group instance

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

Full source

instance group : Group (P₁ ≃ᵃ[k] P₁) where
  one := refl k P₁
  mul e e' := e'.trans e
  inv := symm
  mul_assoc _ _ _ := trans_assoc _ _ _
  one_mul := trans_refl
  mul_one := refl_trans
  inv_mul_cancel := self_trans_symm

Group Structure on Affine Self-Equivalences

Informal description

The set of affine self-equivalences $P₁ \simeqᵃ[k] P₁$ of an affine space $P₁$ over a ring $k$ forms a group under composition of affine equivalences, with the identity affine equivalence as the neutral element and the inverse affine equivalence as the group inverse.

AffineEquiv.one_def theorem

: (1 : P₁ ≃ᵃ[k] P₁) = refl k P₁

Full source

theorem one_def : (1 : P₁ ≃ᵃ[k] P₁) = refl k P₁ :=
  rfl

Identity Element as Identity Affine Equivalence

Informal description

The identity element in the group of affine self-equivalences $P₁ \simeqᵃ[k] P₁$ is equal to the identity affine equivalence $\text{refl}_k P₁$.

AffineEquiv.coe_one theorem

: ⇑(1 : P₁ ≃ᵃ[k] P₁) = id

Full source

@[simp]
theorem coe_one : ⇑(1 : P₁ ≃ᵃ[k] P₁) = id :=
  rfl

Identity Affine Equivalence as Identity Function

Informal description

The underlying function of the identity affine equivalence $1 : P₁ \simeqᵃ[k] P₁$ is equal to the identity function $\text{id}$ on $P₁$.

AffineEquiv.mul_def theorem

(e e' : P₁ ≃ᵃ[k] P₁) : e * e' = e'.trans e

Full source

theorem mul_def (e e' : P₁ ≃ᵃ[k] P₁) : e * e' = e'.trans e :=
  rfl

Group Multiplication of Affine Self-Equivalences as Composition

Informal description

For any two affine self-equivalences $e$ and $e'$ of an affine space $P₁$ over a ring $k$, the group multiplication $e * e'$ is equal to the composition of $e'$ followed by $e$, i.e., $e * e' = e' \circ e$.

AffineEquiv.coe_mul theorem

(e e' : P₁ ≃ᵃ[k] P₁) : ⇑(e * e') = e ∘ e'

Full source

@[simp]
theorem coe_mul (e e' : P₁ ≃ᵃ[k] P₁) : ⇑(e * e') = e ∘ e' :=
  rfl

Composition of Affine Self-Equivalences as Function Composition

Informal description

For any two affine self-equivalences $e$ and $e'$ of an affine space $P₁$ over a ring $k$, the underlying function of their composition $e * e'$ is equal to the function composition $e \circ e'$.

AffineEquiv.inv_def theorem

(e : P₁ ≃ᵃ[k] P₁) : e⁻¹ = e.symm

Full source

theorem inv_def (e : P₁ ≃ᵃ[k] P₁) : e⁻¹ = e.symm :=
  rfl

Inverse of Affine Self-Equivalence Equals Its Symmetric

Informal description

For any affine self-equivalence $e : P₁ \simeqᵃ[k] P₁$ of an affine space $P₁$ over a ring $k$, the group inverse $e^{-1}$ is equal to the inverse affine equivalence $e^{-1} = e^{\text{symm}}$.

AffineEquiv.linearHom definition

: (P₁ ≃ᵃ[k] P₁) →* V₁ ≃ₗ[k] V₁

Full source

/-- `AffineEquiv.linear` on automorphisms is a `MonoidHom`. -/
@[simps]
def linearHom : (P₁ ≃ᵃ[k] P₁) →* V₁ ≃ₗ[k] V₁ where
  toFun := linear
  map_one' := rfl
  map_mul' _ _ := rfl

Monoid homomorphism from affine self-equivalences to linear equivalences

Informal description

The function `AffineEquiv.linearHom` is a monoid homomorphism from the group of affine self-equivalences of an affine space $P₁$ over a ring $k$ to the group of linear equivalences of its associated vector space $V₁$. Specifically, it maps each affine equivalence $e \colon P₁ \simeqᵃ[k] P₁$ to its underlying linear equivalence $e_{\text{linear}} \colon V₁ \simeqₗ[k] V₁$.

AffineEquiv.equivUnitsAffineMap definition

: (P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ

Full source

/-- The group of `AffineEquiv`s are equivalent to the group of units of `AffineMap`.

This is the affine version of `LinearMap.GeneralLinearGroup.generalLinearEquiv`. -/
@[simps]
def equivUnitsAffineMap : (P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ where
  toFun e :=
    { val := e, inv := e.symm,
      val_inv := congr_arg toAffineMap e.symm_trans_self
      inv_val := congr_arg toAffineMap e.self_trans_symm }
  invFun u :=
    { toFun := (u : P₁ →ᵃ[k] P₁)
      invFun := (↑u⁻¹ : P₁ →ᵃ[k] P₁)
      left_inv := AffineMap.congr_fun u.inv_mul
      right_inv := AffineMap.congr_fun u.mul_inv
      linear :=
        LinearMap.GeneralLinearGroup.generalLinearEquiv _ _ <| Units.map AffineMap.linearHom u
      map_vadd' := fun _ _ => (u : P₁ →ᵃ[k] P₁).map_vadd _ _ }
  left_inv _ := AffineEquiv.ext fun _ => rfl
  right_inv _ := Units.ext <| AffineMap.ext fun _ => rfl
  map_mul' _ _ := rfl

Multiplicative equivalence between affine self-equivalences and units of affine maps

Informal description

The group of affine self-equivalences $ P₁ \simeqᵃ[k] P₁ $ is multiplicatively equivalent to the group of units of the monoid of affine maps $ P₁ \toᵃ[k] P₁ $. More precisely, the equivalence maps each affine self-equivalence $ e $ to the unit $ \{ \text{val} := e, \text{inv} := e^{-1} \} $ in the group of units, where $ e^{-1} $ is the inverse affine equivalence. Conversely, it maps each unit $ u $ in the group of affine maps to the affine equivalence defined by the affine map $ u $ and its inverse $ u^{-1} $.

AffineEquiv.vaddConst definition

(b : P₁) : V₁ ≃ᵃ[k] P₁

Full source

/-- The map `v ↦ v +ᵥ b` as an affine equivalence between a module `V` and an affine space `P` with
tangent space `V`. -/
@[simps! linear apply symm_apply]
def vaddConst (b : P₁) : V₁ ≃ᵃ[k] P₁ where
  toEquiv := Equiv.vaddConst b
  linear := LinearEquiv.refl _ _
  map_vadd' _ _ := add_vadd _ _ _

Affine equivalence by translation

Informal description

For a point $b$ in an affine space $P₁$ over a ring $k$ with associated vector space $V₁$, the map $v \mapsto v +ᵥ b$ is an affine equivalence between $V₁$ and $P₁$. Here, $+ᵥ$ denotes the action of the vector space $V₁$ on the affine space $P₁$.

AffineEquiv.constVSub definition

(p : P₁) : P₁ ≃ᵃ[k] V₁

Full source

/-- `p' ↦ p -ᵥ p'` as an equivalence. -/
def constVSub (p : P₁) : P₁ ≃ᵃ[k] V₁ where
  toEquiv := Equiv.constVSub p
  linear := LinearEquiv.neg k
  map_vadd' p' v := by simp [vsub_vadd_eq_vsub_sub, neg_add_eq_sub]

Affine equivalence by vector subtraction from a fixed point

Informal description

For a point $p$ in an affine space $P₁$ over a ring $k$ with associated vector space $V₁$, the map $p' \mapsto p -ᵥ p'$ is an affine equivalence between $P₁$ and $V₁$, where $-ᵥ$ denotes the vector subtraction operation in the torsor structure. The inverse map is given by $v \mapsto -v +ᵥ p$.

AffineEquiv.coe_constVSub theorem

(p : P₁) : ⇑(constVSub k p) = (p -ᵥ ·)

Full source

@[simp]
theorem coe_constVSub (p : P₁) : ⇑(constVSub k p) = (p -ᵥ ·) :=
  rfl

Coefficient function of affine equivalence via vector subtraction from a fixed point

Informal description

For a fixed point $p$ in an affine space $P₁$ over a ring $k$ with associated vector space $V₁$, the underlying function of the affine equivalence $\text{constVSub}_k(p) : P₁ \simeqᵐ[k] V₁$ is given by the vector subtraction operation $p' \mapsto p -ᵥ p'$.

AffineEquiv.coe_constVSub_symm theorem

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

Full source

@[simp]
theorem coe_constVSub_symm (p : P₁) : ⇑(constVSub k p).symm = fun v : V₁ => -v +ᵥ p :=
  rfl

Inverse of affine equivalence via vector subtraction from a fixed point

Informal description

For a fixed point $p$ in an affine space $P₁$ over a ring $k$ with associated vector space $V₁$, the inverse of the affine equivalence $\text{constVSub}_k(p) : P₁ \simeqᵃ[k] V₁$ is given by the function $v \mapsto -v +ᵥ p$ for any vector $v \in V₁$.

AffineEquiv.constVAdd definition

(v : V₁) : P₁ ≃ᵃ[k] P₁

Full source

/-- 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 `•`. -/
@[simps! apply linear]
def constVAdd (v : V₁) : P₁ ≃ᵃ[k] P₁ where
  toEquiv := Equiv.constVAdd P₁ v
  linear := LinearEquiv.refl _ _
  map_vadd' _ _ := vadd_comm _ _ _

Translation by a vector as an affine automorphism

Informal description

For a fixed vector $v$ in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$, the map $p \mapsto v +ᵥ p$ defines an affine automorphism of $P₁$. Here, $+ᵥ$ denotes the action of the vector space on the affine space. This automorphism is always an equivalence, with its linear part being the identity map on $V₁$.

AffineEquiv.constVAdd_zero theorem

: constVAdd k P₁ 0 = AffineEquiv.refl _ _

Full source

@[simp]
theorem constVAdd_zero : constVAdd k P₁ 0 = AffineEquiv.refl _ _ :=
  ext <| zero_vadd _

Translation by Zero Vector is Identity Affine Equivalence

Informal description

The affine equivalence given by translation by the zero vector in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$ is equal to the identity affine equivalence on $P₁$. In other words, $\text{constVAdd}_k P₁ 0 = \text{refl}_k P₁$.

AffineEquiv.constVAdd_add theorem

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

Full source

@[simp]
theorem constVAdd_add (v w : V₁) :
    constVAdd k P₁ (v + w) = (constVAdd k P₁ w).trans (constVAdd k P₁ v) :=
  ext <| add_vadd _ _

Additivity of Translation Affine Equivalences: $t_{v+w} = t_w \circ t_v$

Informal description

For any vectors $v, w$ in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$, the affine equivalence given by translation by $v + w$ is equal to the composition of the affine equivalences given by translation by $w$ followed by translation by $v$. In other words, $t_{v+w} = t_w \circ t_v$, where $t_v$ denotes the translation map $p \mapsto v +ᵥ p$.

AffineEquiv.constVAdd_symm theorem

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

Full source

@[simp]
theorem constVAdd_symm (v : V₁) : (constVAdd k P₁ v).symm = constVAdd k P₁ (-v) :=
  ext fun _ => rfl

Inverse of Translation by $v$ is Translation by $-v$

Informal description

For any vector $v$ in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$, the inverse of the affine automorphism given by translation by $v$ is equal to the affine automorphism given by translation by $-v$. In other words, $(t_v)^{-1} = t_{-v}$, where $t_v$ denotes the translation map $p \mapsto v +ᵥ p$.

AffineEquiv.constVAddHom definition

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

Full source

/-- A more bundled version of `AffineEquiv.constVAdd`. -/
@[simps]
def constVAddHom : MultiplicativeMultiplicative V₁ →* P₁ ≃ᵃ[k] P₁ where
  toFun v := constVAdd k P₁ v.toAdd
  map_one' := constVAdd_zero _ _
  map_mul' := constVAdd_add _ P₁

Homomorphism from vector translations to affine automorphisms

Informal description

The function maps an element $ v $ of the multiplicative group of the vector space $ V_1 $ to the affine automorphism of $ P_1 $ given by translation by $ v $. This defines a monoid homomorphism from the multiplicative group of $ V_1 $ to the group of affine self-equivalences of $ P_1 $, where the group operation is composition of affine equivalences.

AffineEquiv.constVAdd_nsmul theorem

(n : ℕ) (v : V₁) : constVAdd k P₁ (n • v) = constVAdd k P₁ v ^ n

Full source

theorem constVAdd_nsmul (n : ℕ) (v : V₁) : constVAdd k P₁ (n • v) = constVAdd k P₁ v ^ n :=
  (constVAddHom k P₁).map_pow _ _

Translation by Scalar Multiple Equals Power of Translation: $t_{n \cdot v} = (t_v)^n$

Informal description

For any natural number $n$ and vector $v$ in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$, the affine automorphism given by translation by $n \cdot v$ is equal to the $n$-th power of the affine automorphism given by translation by $v$. In other words, $t_{n \cdot v} = (t_v)^n$, where $t_v$ denotes the translation map $p \mapsto v +ᵥ p$.

AffineEquiv.constVAdd_zsmul theorem

(z : ℤ) (v : V₁) : constVAdd k P₁ (z • v) = constVAdd k P₁ v ^ z

Full source

theorem constVAdd_zsmul (z : ℤ) (v : V₁) : constVAdd k P₁ (z • v) = constVAdd k P₁ v ^ z :=
  (constVAddHom k P₁).map_zpow _ _

Integer Scalar Multiplication of Translation Affine Automorphisms: $\text{constVAdd}_k P₁ (z \cdot v) = (\text{constVAdd}_k P₁ v)^z$

Informal description

For any integer $z$ and vector $v$ in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$, the affine automorphism given by translation by $z \cdot v$ is equal to the $z$-th power of the affine automorphism given by translation by $v$. In other words, $\text{constVAdd}_k P₁ (z \cdot v) = (\text{constVAdd}_k P₁ v)^z$.

AffineEquiv.homothetyUnitsMulHom definition

(p : P) : Rˣ →* P ≃ᵃ[R] P

Full source

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

Group homomorphism from units to affine self-equivalences via homothety

Informal description

Given a point $p$ in an affine space $P$ over a ring $R$, the function `homothetyUnitsMulHom` is a group homomorphism from the group of units $R^\times$ of $R$ to the group of affine self-equivalences $P \simeqᵃ[R] P$ of $P$. For each unit $t \in R^\times$, the corresponding affine equivalence is the homothety (scaling transformation) centered at $p$ with scaling factor $t$, i.e., the map $x \mapsto p + t \cdot (x - p)$. The inverse of this affine equivalence is the homothety centered at $p$ with scaling factor $t^{-1}$.

AffineEquiv.coe_homothetyUnitsMulHom_apply theorem

(p : P) (t : Rˣ) : (homothetyUnitsMulHom p t : P → P) = AffineMap.homothety p (t : R)

Full source

@[simp]
theorem coe_homothetyUnitsMulHom_apply (p : P) (t : Rˣ) :
    (homothetyUnitsMulHom p t : P → P) = AffineMap.homothety p (t : R) :=
  rfl

Underlying Function of Homothety Affine Equivalence via Units

Informal description

For a fixed point $p$ in an affine space $P$ over a ring $R$ and any unit $t \in R^\times$, the underlying function of the affine equivalence `homothetyUnitsMulHom p t` is equal to the homothety (scaling transformation) centered at $p$ with scaling factor $t$, i.e., the map $x \mapsto p + t \cdot (x - p)$.

AffineEquiv.coe_homothetyUnitsMulHom_apply_symm theorem

(p : P) (t : Rˣ) : ((homothetyUnitsMulHom p t).symm : P → P) = AffineMap.homothety p (↑t⁻¹ : R)

Full source

@[simp]
theorem coe_homothetyUnitsMulHom_apply_symm (p : P) (t : Rˣ) :
    ((homothetyUnitsMulHom p t).symm : P → P) = AffineMap.homothety p (↑t⁻¹ : R) :=
  rfl

Inverse of Homothety Affine Equivalence as Homothety with Inverse Scaling Factor

Informal description

For a point $p$ in an affine space $P$ over a ring $R$ and a unit $t \in R^\times$, the underlying function of the inverse affine equivalence $\text{homothetyUnitsMulHom}(p, t)^{-1} : P \to P$ is equal to the homothety (scaling transformation) centered at $p$ with scaling factor $t^{-1} \in R$.

AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe theorem

 (p : P) : ((↑) : (P ≃ᵃ[R] P) → P →ᵃ[R] P) ∘ homothetyUnitsMulHom p = AffineMap.homothetyHom p ∘ ((↑) : Rˣ → R)

Full source

@[simp]
theorem coe_homothetyUnitsMulHom_eq_homothetyHom_coe (p : P) :
    ((↑) : (P ≃ᵃ[R] P) → P →ᵃ[R] P) ∘ homothetyUnitsMulHom p =
      AffineMap.homothetyHomAffineMap.homothetyHom p ∘ ((↑) : Rˣ → R) :=
  funext fun _ => rfl

Commutative Diagram of Homothety Maps and Canonical Inclusions

Informal description

For a fixed point $p$ in an affine space $P$ over a ring $R$, the composition of the canonical inclusion map from affine self-equivalences $P \simeqᵃ[R] P$ to affine maps $P \toᵃ[R] P$ with the homothety group homomorphism $\text{homothetyUnitsMulHom}(p) : R^\times \to P \simeqᵃ[R] P$ equals the composition of the homothety affine map homomorphism $\text{homothetyHom}(p) : R \to P \toᵃ[R] P$ with the canonical inclusion map from units $R^\times$ to $R$.

AffineEquiv.pointReflection definition

(x : P₁) : P₁ ≃ᵃ[k] P₁

Full source

/-- Point reflection in `x` as a permutation. -/
def pointReflection (x : P₁) : P₁ ≃ᵃ[k] P₁ :=
  (constVSub k x).trans (vaddConst k x)

Point reflection in an affine space

Informal description

For a point $ x $ in an affine space $ P_1 $ over a ring $ k $ with associated vector space $ V_1 $, the point reflection in $ x $ is the affine equivalence $ P_1 \simeqᵃ[k] P_1 $ given by the composition of the affine equivalence $ p' \mapsto x -ᵥ p' $ (vector subtraction from $ x $) and the affine equivalence $ v \mapsto v +ᵥ x $ (translation by $ x $). Explicitly, it maps any point $ y $ to $ (x -ᵥ y) +ᵥ x $.

AffineEquiv.pointReflection_apply_eq_equivPointReflection_apply theorem

(x y : P₁) : pointReflection k x y = Equiv.pointReflection x y

Full source

@[simp] lemma pointReflection_apply_eq_equivPointReflection_apply (x y : P₁) :
    pointReflection k x y = Equiv.pointReflection x y :=
  rfl

Affine Point Reflection Equals Set-Theoretic Point Reflection

Informal description

For any points $x$ and $y$ in an affine space $P₁$ over a ring $k$, the point reflection of $y$ about $x$ as an affine equivalence equals the point reflection of $y$ about $x$ as a set-theoretic equivalence. That is, $\text{pointReflection}_k(x)(y) = \text{Equiv.pointReflection}(x)(y)$.

AffineEquiv.pointReflection_apply theorem

(x y : P₁) : pointReflection k x y = (x -ᵥ y) +ᵥ x

Full source

theorem pointReflection_apply (x y : P₁) : pointReflection k x y = (x -ᵥ y) +ᵥ x :=
  rfl

Point Reflection Formula in Affine Space

Informal description

For any points $x$ and $y$ in an affine space $P_1$ over a ring $k$, the point reflection of $y$ about $x$ is given by $(x -ᵥ y) +ᵥ x$, where $-ᵥ$ denotes the vector subtraction in the associated torsor and $+ᵥ$ denotes the translation action.

AffineEquiv.pointReflection_symm theorem

(x : P₁) : (pointReflection k x).symm = pointReflection k x

Full source

@[simp]
theorem pointReflection_symm (x : P₁) : (pointReflection k x).symm = pointReflection k x :=
  toEquiv_injective <| Equiv.pointReflection_symm x

Point reflection is self-inverse

Informal description

For any point $x$ in an affine space $P_1$ over a ring $k$, the inverse of the point reflection affine equivalence at $x$ is equal to itself, i.e., $(\text{pointReflection}_k\,x)^{-1} = \text{pointReflection}_k\,x$.

AffineEquiv.toEquiv_pointReflection theorem

(x : P₁) : (pointReflection k x).toEquiv = Equiv.pointReflection x

Full source

@[simp]
theorem toEquiv_pointReflection (x : P₁) :
    (pointReflection k x).toEquiv = Equiv.pointReflection x :=
  rfl

Underlying Equivalence of Point Reflection in Affine Space

Informal description

For any point $x$ in an affine space $P_1$ over a ring $k$, the underlying equivalence of the point reflection affine equivalence at $x$ is equal to the point reflection equivalence at $x$. That is, $\text{toEquiv}(\text{pointReflection}_k(x)) = \text{Equiv.pointReflection}(x)$.

AffineEquiv.pointReflection_self theorem

(x : P₁) : pointReflection k x x = x

Full source

theorem pointReflection_self (x : P₁) : pointReflection k x x = x :=
  vsub_vadd _ _

Fixed Point Property of Point Reflection

Informal description

For any point $x$ in an affine space $P_1$ over a ring $k$, the point reflection at $x$ maps $x$ to itself, i.e., $\text{pointReflection}_k(x)(x) = x$.

AffineEquiv.pointReflection_involutive theorem

(x : P₁) : Involutive (pointReflection k x : P₁ → P₁)

Full source

theorem pointReflection_involutive (x : P₁) : Involutive (pointReflection k x : P₁ → P₁) :=
  Equiv.pointReflection_involutive x

Point Reflection is Involutive

Informal description

For any point $x$ in an affine space $P_1$ over a ring $k$, the point reflection map $\text{pointReflection}_k(x) : P_1 \to P_1$ is involutive, i.e., $\text{pointReflection}_k(x)(\text{pointReflection}_k(x)(y)) = y$ for all $y \in P_1$.

AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul theorem

{x y : P₁} (h : Injective (2 • · : V₁ → V₁)) : pointReflection k x y = y ↔ y = x

Full source

/-- `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 pointReflection_fixed_iff_of_injective_two_nsmul {x y : P₁}
    (h : Injective (2 • · : V₁ → V₁)) : pointReflectionpointReflection k x y = y ↔ y = x :=
  Equiv.pointReflection_fixed_iff_of_injective_two_nsmul h

Fixed point characterization of point reflection in affine space

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$, and let $x, y \in P_1$. If the map $v \mapsto 2 \cdot v$ is injective on $V_1$, then the point reflection of $y$ about $x$ equals $y$ if and only if $y = x$. In other words, $x$ is the only fixed point of the point reflection map about $x$.

AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul theorem

(h : Injective (2 • · : V₁ → V₁)) (y : P₁) : Injective fun x : P₁ => pointReflection k x y

Full source

theorem injective_pointReflection_left_of_injective_two_nsmul
    (h : Injective (2 • · : V₁ → V₁)) (y : P₁) :
    Injective fun x : P₁ => pointReflection k x y :=
  Equiv.injective_pointReflection_left_of_injective_two_nsmul h y

Injectivity of Point Reflection Map under Scalar Multiplication Injectivity Condition

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$, and suppose the map $v \mapsto 2 \cdot v$ is injective on $V_1$. Then for any fixed point $y \in P_1$, the map $x \mapsto \text{pointReflection}_k(x)(y)$ is injective as a function from $P_1$ to $P_1$.

AffineEquiv.injective_pointReflection_left_of_module theorem

[Invertible (2 : k)] : ∀ y, Injective fun x : P₁ => pointReflection k x y

Full source

theorem injective_pointReflection_left_of_module [Invertible (2 : k)] :
    ∀ y, Injective fun x : P₁ => pointReflection k x y :=
  injective_pointReflection_left_of_injective_two_nsmul k fun x y h => by
    dsimp at h
    rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y,
      (isUnit_of_invertible (2 : k)).smul_left_cancel] at h

Injectivity of Point Reflection Map with Invertible Scalar 2

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$, and assume that $2$ is invertible in $k$. Then for any fixed point $y \in P_1$, the map $x \mapsto \text{pointReflection}_k(x)(y)$ is injective as a function from $P_1$ to $P_1$.

AffineEquiv.pointReflection_fixed_iff_of_module theorem

[Invertible (2 : k)] {x y : P₁} : pointReflection k x y = y ↔ y = x

Full source

theorem pointReflection_fixed_iff_of_module [Invertible (2 : k)] {x y : P₁} :
    pointReflectionpointReflection k x y = y ↔ y = x :=
  ((injective_pointReflection_left_of_module k y).eq_iff' (pointReflection_self k y)).trans eq_comm

Fixed Points of Point Reflection in Affine Space with Invertible 2

Informal description

Let $P_1$ be an affine space over a ring $k$ where $2$ is invertible. For any points $x, y \in P_1$, the point reflection of $y$ about $x$ equals $y$ if and only if $y = x$. In other words, $\text{pointReflection}_k(x)(y) = y \leftrightarrow y = x$.

LinearEquiv.toAffineEquiv definition

(e : V₁ ≃ₗ[k] V₂) : V₁ ≃ᵃ[k] V₂

Full source

/-- Interpret a linear equivalence between modules as an affine equivalence. -/
def toAffineEquiv (e : V₁ ≃ₗ[k] V₂) : V₁ ≃ᵃ[k] V₂ where
  toEquiv := e.toEquiv
  linear := e
  map_vadd' p v := e.map_add v p

Affine equivalence induced by a linear equivalence

Informal description

Given a linear equivalence $e : V₁ \simeqₗ[k] V₂$ between modules $V₁$ and $V₂$ over a ring $k$, this function constructs an affine equivalence $V₁ \simeqᵃ[k] V₂$ by interpreting $e$ as an affine map. The underlying equivalence is $e$ itself, and the linear part is also $e$. The map preserves the vector addition action, meaning $e(p + v) = e(p) + e(v)$ for any point $p \in V₁$ and vector $v \in V₁$.

LinearEquiv.coe_toAffineEquiv theorem

(e : V₁ ≃ₗ[k] V₂) : ⇑e.toAffineEquiv = e

Full source

@[simp]
theorem coe_toAffineEquiv (e : V₁ ≃ₗ[k] V₂) : ⇑e.toAffineEquiv = e :=
  rfl

Underlying Function of Affine Equivalence Induced by Linear Equivalence

Informal description

For any linear equivalence $e : V₁ \simeqₗ[k] V₂$ between modules $V₁$ and $V₂$ over a ring $k$, the underlying function of the induced affine equivalence $e.toAffineEquiv$ is equal to $e$ itself.

AffineMap.lineMap_vadd theorem

(v v' : V₁) (p : P₁) (c : k) : lineMap v v' c +ᵥ p = lineMap (v +ᵥ p) (v' +ᵥ p) c

Full source

theorem lineMap_vadd (v v' : V₁) (p : P₁) (c : k) :
    lineMaplineMap v v' c +ᵥ p = lineMap (v +ᵥ p) (v' +ᵥ p) c :=
  (vaddConst k p).apply_lineMap v v' c

Affine Combination Preserves Vector Action

Informal description

For any vectors $v, v'$ in the vector space $V₁$, any point $p$ in the affine space $P₁$, and any scalar $c$ in the ring $k$, the action of the affine combination $\text{lineMap}(v, v', c)$ on $p$ equals the affine combination of the actions of $v$ and $v'$ on $p$. That is, $$ \text{lineMap}(v, v', c) +ᵥ p = \text{lineMap}(v +ᵥ p, v' +ᵥ p, c). $$

AffineMap.lineMap_vsub theorem

(p₁ p₂ p₃ : P₁) (c : k) : lineMap p₁ p₂ c -ᵥ p₃ = lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) c

Full source

theorem lineMap_vsub (p₁ p₂ p₃ : P₁) (c : k) :
    lineMaplineMap p₁ p₂ c -ᵥ p₃ = lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) c :=
  (vaddConst k p₃).symm.apply_lineMap p₁ p₂ c

Affine Combination Preserves Vector Subtraction

Informal description

For any points $p_1, p_2, p_3$ in an affine space $P_1$ over a ring $k$ and any scalar $c \in k$, the vector subtraction of the affine combination $\text{lineMap}(p_1, p_2, c)$ and $p_3$ equals the affine combination of the vector differences $(p_1 -ᵥ p_3)$ and $(p_2 -ᵥ p_3)$ with the same scalar $c$. That is, $$ \text{lineMap}(p_1, p_2, c) -ᵥ p_3 = \text{lineMap}(p_1 -ᵥ p_3, p_2 -ᵥ p_3, c). $$

AffineMap.vsub_lineMap theorem

(p₁ p₂ p₃ : P₁) (c : k) : p₁ -ᵥ lineMap p₂ p₃ c = lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) c

Full source

theorem vsub_lineMap (p₁ p₂ p₃ : P₁) (c : k) :
    p₁ -ᵥ lineMap p₂ p₃ c = lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) c :=
  (constVSub k p₁).apply_lineMap p₂ p₃ c

Vector Subtraction of Affine Combination Equals Affine Combination of Vector Subtractions

Informal description

For any points $p_1, p_2, p_3$ in an affine space $P_1$ over a ring $k$ and any scalar $c \in k$, the vector subtraction of $p_1$ from the affine combination $\text{lineMap}(p_2, p_3, c)$ equals the affine combination of the vector subtractions $(p_1 -ᵥ p_2)$ and $(p_1 -ᵥ p_3)$ with the same scalar $c$. That is, $$ p_1 -ᵥ \text{lineMap}(p_2, p_3, c) = \text{lineMap}(p_1 -ᵥ p_2, p_1 -ᵥ p_3, c). $$

AffineMap.vadd_lineMap theorem

(v : V₁) (p₁ p₂ : P₁) (c : k) : v +ᵥ lineMap p₁ p₂ c = lineMap (v +ᵥ p₁) (v +ᵥ p₂) c

Full source

theorem vadd_lineMap (v : V₁) (p₁ p₂ : P₁) (c : k) :
    v +ᵥ lineMap p₁ p₂ c = lineMap (v +ᵥ p₁) (v +ᵥ p₂) c :=
  (constVAdd k P₁ v).apply_lineMap p₁ p₂ c

Vector Action Commutes with Affine Combination

Informal description

For any vector $v$ in the associated vector space $V₁$ of an affine space $P₁$ over a ring $k$, and for any points $p₁, p₂ \in P₁$ and scalar $c \in k$, the action of $v$ on the affine combination $\text{lineMap}(p₁, p₂, c)$ equals the affine combination of the translated points $\text{lineMap}(v +ᵥ p₁, v +ᵥ p₂, c)$. That is, $$ v +ᵥ \text{lineMap}(p₁, p₂, c) = \text{lineMap}(v +ᵥ p₁, v +ᵥ p₂, c). $$

AffineMap.homothety_neg_one_apply theorem

(c p : P₁) : homothety c (-1 : R') p = pointReflection R' c p

Full source

theorem homothety_neg_one_apply (c p : P₁) : homothety c (-1 : R') p = pointReflection R' c p := by
  simp [homothety_apply, Equiv.pointReflection_apply]

Homothety with Scaling Factor $-1$ Equals Point Reflection

Informal description

For any point $c$ in an affine space $P_1$ over a ring $R'$, the homothety centered at $c$ with scaling factor $-1$ applied to a point $p$ equals the point reflection of $p$ about $c$. That is, $$ \text{homothety}_c(-1)(p) = \text{pointReflection}_{R'}(c)(p). $$

Tags