Mathlib.LinearAlgebra.AffineSpace.AffineMap

AffineMap structure

 (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*) [Ring k] [AddCommGroup V1] [Module k V1]
  [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2] [AffineSpace V2 P2]

Full source

/-- An `AffineMap k P1 P2` (notation: `P1 →ᵃ[k] P2`) is a map from `P1` to `P2` that
induces a corresponding linear map from `V1` to `V2`. -/
structure AffineMap (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*) [Ring k]
  [AddCommGroup V1] [Module k V1] [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2]
  [AffineSpace V2 P2] where
  toFun : P1 → P2
  linear : V1 →ₗ[k] V2
  map_vadd' : ∀ (p : P1) (v : V1), toFun (v +ᵥ p) = linear v +ᵥ toFun p

Affine Map

Informal description

An affine map between two affine spaces $P_1$ and $P_2$ over the same ring $k$ is a map $f \colon P_1 \to P_2$ that induces a corresponding linear map between the associated vector spaces $V_1$ and $V_2$ of $P_1$ and $P_2$, respectively. Here, $V_1$ and $V_2$ are modules over $k$ equipped with additive commutative group structures, and $P_1$ and $P_2$ are affine spaces over $V_1$ and $V_2$.

term_→ᵃ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- An `AffineMap k P1 P2` (notation: `P1 →ᵃ[k] P2`) is a map from `P1` to `P2` that
induces a corresponding linear map from `V1` to `V2`. -/
notation:25 P1 " →ᵃ[" k:25 "] " P2:0 => AffineMap k P1 P2

Affine map notation

Informal description

The notation `P1 →ᵐ[k] P2` represents the type of affine maps from an affine space `P1` to another affine space `P2` over the same ring `k`. An affine map is a function that induces a corresponding linear map between the associated vector spaces `V1` and `V2` of `P1` and `P2`, respectively.

AffineMap.instFunLike instance

 (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*) [Ring k] [AddCommGroup V1] [Module k V1]
  [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2] [AffineSpace V2 P2] : FunLike (P1 →ᵃ[k] P2) P1 P2

Full source

instance AffineMap.instFunLike (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*)
    [Ring k] [AddCommGroup V1] [Module k V1] [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2]
    [AffineSpace V2 P2] : FunLike (P1 →ᵃ[k] P2) P1 P2 where
  coe := AffineMap.toFun
  coe_injective' := fun ⟨f, f_linear, f_add⟩ ⟨g, g_linear, g_add⟩ => fun (h : f = g) => by
    obtain ⟨p⟩ := (AddTorsor.nonempty : Nonempty P1)
    congr with v
    apply vadd_right_cancel (f p)
    rw [← f_add, h, ← g_add]

Function-Like Structure on Affine Maps

Informal description

For any ring $k$, affine spaces $P_1$ and $P_2$ over $k$ with associated vector spaces $V_1$ and $V_2$ respectively, the type of affine maps $P_1 \toᵃ[k] P_2$ is equipped with a function-like structure that allows these maps to be treated as functions from $P_1$ to $P_2$.

LinearMap.toAffineMap definition

: V₁ →ᵃ[k] V₂

Full source

/-- Reinterpret a linear map as an affine map. -/
def toAffineMap : V₁ →ᵃ[k] V₂ where
  toFun := f
  linear := f
  map_vadd' p v := f.map_add v p

Affine map induced by a linear map

Informal description

Given a linear map $ f \colon V_1 \to V_2 $ between modules $ V_1 $ and $ V_2 $ over a ring $ k $, the affine map $ f \colon V_1 \to V_2 $ is defined by the same underlying function $ f $, with the linear part also given by $ f $. This map satisfies the property $ f(p + v) = f(p) + f(v) $ for any point $ p \in V_1 $ and vector $ v \in V_1 $.

LinearMap.coe_toAffineMap theorem

: ⇑f.toAffineMap = f

Full source

@[simp]
theorem coe_toAffineMap : ⇑f.toAffineMap = f :=
  rfl

Underlying Function of Affine Map Induced by Linear Map Equals Original Linear Map

Informal description

For any linear map $f \colon V_1 \to V_2$ between modules $V_1$ and $V_2$ over a ring $k$, the underlying function of the induced affine map $f \colon V_1 \to V_2$ is equal to $f$ itself.

LinearMap.toAffineMap_linear theorem

: f.toAffineMap.linear = f

Full source

@[simp]
theorem toAffineMap_linear : f.toAffineMap.linear = f :=
  rfl

Linear Part of Induced Affine Map Equals Original Linear Map

Informal description

For any linear map $f \colon V_1 \to V_2$ between modules over a ring $k$, the linear part of the induced affine map $f \colon V_1 \to V_2$ is equal to $f$ itself.

AffineMap.coe_mk theorem

(f : P1 → P2) (linear add) : ((mk f linear add : P1 →ᵃ[k] P2) : P1 → P2) = f

Full source

/-- Constructing an affine map and coercing back to a function
produces the same map. -/
@[simp]
theorem coe_mk (f : P1 → P2) (linear add) : ((mk f linear add : P1 →ᵃ[k] P2) : P1 → P2) = f :=
  rfl

Coercion of Constructed Affine Map Equals Original Function

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively. Given a function $f \colon P_1 \to P_2$, a linear map $\text{linear} \colon V_1 \to V_2$, and an additive condition $\text{add}$, the function obtained by coercing the affine map $\text{mk } f \text{ linear add} \colon P_1 \toᵃ[k] P_2$ back to a function equals $f$.

AffineMap.toFun_eq_coe theorem

(f : P1 →ᵃ[k] P2) : f.toFun = ⇑f

Full source

/-- `toFun` is the same as the result of coercing to a function. -/
@[simp]
theorem toFun_eq_coe (f : P1 →ᵃ[k] P2) : f.toFun = ⇑f :=
  rfl

Equality of Affine Map's Underlying Function and its Coercion

Informal description

For any affine map $f \colon P_1 \to_{k} P_2$ between affine spaces $P_1$ and $P_2$ over a ring $k$, the underlying function $f.\text{toFun}$ is equal to the function obtained by coercing $f$ to a function (denoted by $\uparrow f$).

AffineMap.map_vadd theorem

(f : P1 →ᵃ[k] P2) (p : P1) (v : V1) : f (v +ᵥ p) = f.linear v +ᵥ f p

Full source

/-- An affine map on the result of adding a vector to a point produces
the same result as the linear map applied to that vector, added to the
affine map applied to that point. -/
@[simp]
theorem map_vadd (f : P1 →ᵃ[k] P2) (p : P1) (v : V1) : f (v +ᵥ p) = f.linear v +ᵥ f p :=
  f.map_vadd' p v

Affine Map Action on Translated Points

Informal description

Let $f \colon P_1 \to P_2$ be an affine map between affine spaces over a ring $k$, with associated vector spaces $V_1$ and $V_2$ respectively. For any point $p \in P_1$ and vector $v \in V_1$, the action of $f$ on the translated point $v + p$ equals the action of the linear part of $f$ on $v$ plus the action of $f$ on $p$, i.e., $$ f(v + p) = f_{\text{linear}}(v) + f(p). $$

AffineMap.linearMap_vsub theorem

(f : P1 →ᵃ[k] P2) (p1 p2 : P1) : f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

Full source

/-- The linear map on the result of subtracting two points is the
result of subtracting the result of the affine map on those two
points. -/
@[simp]
theorem linearMap_vsub (f : P1 →ᵃ[k] P2) (p1 p2 : P1) : f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2 := by
  conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

Linear Part of Affine Map Preserves Vector Differences

Informal description

Let $f \colon P_1 \to P_2$ be an affine map between affine spaces over a ring $k$, with associated vector spaces $V_1$ and $V_2$ respectively. For any two points $p_1, p_2 \in P_1$, the linear part of $f$ applied to the vector difference $p_1 - p_2$ equals the vector difference of the images $f(p_1) - f(p_2)$, i.e., $$ f_{\text{linear}}(p_1 - p_2) = f(p_1) - f(p_2). $$

AffineMap.ext theorem

{f g : P1 →ᵃ[k] P2} (h : ∀ p, f p = g p) : f = g

Full source

/-- Two affine maps are equal if they coerce to the same function. -/
@[ext]
theorem ext {f g : P1 →ᵃ[k] P2} (h : ∀ p, f p = g p) : f = g :=
  DFunLike.ext _ _ h

Extensionality of Affine Maps

Informal description

Let $k$ be a ring, and let $P_1$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V_1$ and $V_2$ respectively. For any two affine maps $f, g \colon P_1 \to P_2$, if $f(p) = g(p)$ for all points $p \in P_1$, then $f = g$.

AffineMap.coeFn_injective theorem

: @Function.Injective (P1 →ᵃ[k] P2) (P1 → P2) (⇑)

Full source

theorem coeFn_injective : @Function.Injective (P1 →ᵃ[k] P2) (P1 → P2) (⇑) :=
  DFunLike.coe_injective

Injectivity of the Affine Map to Function Coercion

Informal description

The canonical map from the type of affine maps $P_1 \toᵃ[k] P_2$ to the type of functions $P_1 \to P_2$ is injective. That is, if two affine maps $f, g \colon P_1 \toᵃ[k] P_2$ satisfy $f(p) = g(p)$ for all $p \in P_1$, then $f = g$.

AffineMap.congr_arg theorem

(f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) : f x = f y

Full source

protected theorem congr_arg (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) : f x = f y :=
  congr_arg _ h

Affine Map Preserves Equality

Informal description

For any affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, and any points $x, y \in P_1$ such that $x = y$, we have $f(x) = f(y)$.

AffineMap.congr_fun theorem

{f g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) : f x = g x

Full source

protected theorem congr_fun {f g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) : f x = g x :=
  h ▸ rfl

Function Equality Implies Pointwise Equality for Affine Maps

Informal description

For any two affine maps $f, g \colon P_1 \to P_2$ over the same ring $k$, if $f = g$, then $f(x) = g(x)$ for all $x \in P_1$.

AffineMap.ext_linear theorem

{f g : P1 →ᵃ[k] P2} (h₁ : f.linear = g.linear) {p : P1} (h₂ : f p = g p) : f = g

Full source

/-- Two affine maps are equal if they have equal linear maps and are equal at some point. -/
theorem ext_linear {f g : P1 →ᵃ[k] P2} (h₁ : f.linear = g.linear) {p : P1} (h₂ : f p = g p) :
    f = g := by
  ext q
  have hgl : g.linear (q -ᵥ p) = toFuntoFun g ((q -ᵥ p) +ᵥ q) -ᵥ toFun g q := by simp
  have := f.map_vadd' q (q -ᵥ p)
  rw [h₁, hgl, toFun_eq_coe, map_vadd, linearMap_vsub, h₂] at this
  simpa

Equality of Affine Maps via Linear Part and Pointwise Equality

Informal description

Let $k$ be a ring, and let $P_1$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V_1$ and $V_2$ respectively. For any two affine maps $f, g \colon P_1 \to P_2$, if their associated linear maps are equal (i.e., $f_{\text{linear}} = g_{\text{linear}}$) and there exists a point $p \in P_1$ such that $f(p) = g(p)$, then $f = g$.

AffineMap.ext_linear_iff theorem

{f g : P1 →ᵃ[k] P2} : f = g ↔ (f.linear = g.linear) ∧ (∃ p, f p = g p)

Full source

/-- Two affine maps are equal if they have equal linear maps and are equal at some point. -/
theorem ext_linear_iff {f g : P1 →ᵃ[k] P2} : f = g ↔ (f.linear = g.linear) ∧ (∃ p, f p = g p) :=
  ⟨fun h ↦ ⟨congrArg _ h, by inhabit P1; exact default, by rw [h]⟩,
  fun h ↦ Exists.casesOn h.2 fun _ hp ↦ ext_linear h.1 hp⟩

Equivalence of Affine Map Equality via Linear Part and Pointwise Equality

Informal description

Let $k$ be a ring, and let $P_1$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V_1$ and $V_2$ respectively. For any two affine maps $f, g \colon P_1 \to P_2$, the following are equivalent: 1. $f = g$ as affine maps. 2. The associated linear maps $f_{\text{linear}}$ and $g_{\text{linear}}$ are equal, and there exists a point $p \in P_1$ such that $f(p) = g(p)$.

AffineMap.const definition

(p : P2) : P1 →ᵃ[k] P2

Full source

/-- The constant function as an `AffineMap`. -/
def const (p : P2) : P1 →ᵃ[k] P2 where
  toFun := Function.const P1 p
  linear := 0
  map_vadd' _ _ :=
    letI : AddAction V2 P2 := inferInstance
    by simp

Constant affine map

Informal description

The constant function from an affine space $ P_1 $ to another affine space $ P_2 $ over the same ring $ k $, which maps every point in $ P_1 $ to a fixed point $ p $ in $ P_2 $. The associated linear map is the zero map.

AffineMap.coe_const theorem

(p : P2) : ⇑(const k P1 p) = Function.const P1 p

Full source

@[simp]
theorem coe_const (p : P2) : ⇑(const k P1 p) = Function.const P1 p :=
  rfl

Coefficient of Constant Affine Map Equals Constant Function

Informal description

For any fixed point $p$ in an affine space $P_2$ over a ring $k$, the constant affine map from $P_1$ to $P_2$ that sends every point in $P_1$ to $p$ is equal to the constant function from $P_1$ to $P_2$ that also sends every point to $p$.

AffineMap.const_apply theorem

(p : P2) (q : P1) : (const k P1 p) q = p

Full source

@[simp]
theorem const_apply (p : P2) (q : P1) : (const k P1 p) q = p := rfl

Evaluation of Constant Affine Map: $(\text{const}_k P_1 p)(q) = p$

Informal description

For any fixed point $p$ in an affine space $P_2$ over a ring $k$, the constant affine map $\text{const}_k P_1 p$ from an affine space $P_1$ to $P_2$ satisfies $(\text{const}_k P_1 p)(q) = p$ for every point $q \in P_1$.

AffineMap.const_linear theorem

(p : P2) : (const k P1 p).linear = 0

Full source

@[simp]
theorem const_linear (p : P2) : (const k P1 p).linear = 0 :=
  rfl

Linear Part of Constant Affine Map is Zero

Informal description

For any fixed point $p$ in an affine space $P_2$ over a ring $k$, the linear part of the constant affine map from another affine space $P_1$ to $P_2$ (which sends every point in $P_1$ to $p$) is the zero linear map.

AffineMap.linear_eq_zero_iff_exists_const theorem

(f : P1 →ᵃ[k] P2) : f.linear = 0 ↔ ∃ q, f = const k P1 q

Full source

theorem linear_eq_zero_iff_exists_const (f : P1 →ᵃ[k] P2) :
    f.linear = 0 ↔ ∃ q, f = const k P1 q := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · use f (Classical.arbitrary P1)
    ext
    rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h,
      LinearMap.zero_apply]
  · rcases h with ⟨q, rfl⟩
    exact const_linear k P1 q

Characterization of Constant Affine Maps via Zero Linear Part

Informal description

Let $k$ be a ring, and let $P_1$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V_1$ and $V_2$ respectively. For any affine map $f \colon P_1 \to P_2$, the linear part of $f$ is the zero map if and only if $f$ is a constant affine map, i.e., there exists a point $q \in P_2$ such that $f$ equals the constant affine map $\text{const}_k P_1 q$.

AffineMap.nonempty instance

: Nonempty (P1 →ᵃ[k] P2)

Full source

instance nonempty : Nonempty (P1 →ᵃ[k] P2) :=
  (AddTorsor.nonempty : Nonempty P2).map <| const k P1

Nonempty Type of Affine Maps Between Affine Spaces

Informal description

For any affine spaces $P_1$ and $P_2$ over the same ring $k$, the type of affine maps from $P_1$ to $P_2$ is nonempty.

AffineMap.mk' definition

(f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ p' : P1, f p' = f' (p' -ᵥ p) +ᵥ f p) : P1 →ᵃ[k] P2

Full source

/-- Construct an affine map by verifying the relation between the map and its linear part at one
base point. Namely, this function takes a map `f : P₁ → P₂`, a linear map `f' : V₁ →ₗ[k] V₂`, and
a point `p` such that for any other point `p'` we have `f p' = f' (p' -ᵥ p) +ᵥ f p`. -/
def mk' (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ p' : P1, f p' = f' (p' -ᵥ p) +ᵥ f p) :
    P1 →ᵃ[k] P2 where
  toFun := f
  linear := f'
  map_vadd' p' v := by rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]

Construction of an affine map from point and linear part

Informal description

Given a map $f \colon P_1 \to P_2$ between affine spaces, a linear map $f' \colon V_1 \to V_2$ between their associated vector spaces, and a point $p \in P_1$ such that for any other point $p' \in P_1$, the relation $f(p') = f'(p' - p) + f(p)$ holds, then this data defines an affine map from $P_1$ to $P_2$. Here, $V_1$ and $V_2$ are the vector spaces associated with the affine spaces $P_1$ and $P_2$ respectively, and $p' - p$ denotes the vector difference in the affine space.

AffineMap.coe_mk' theorem

(f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : ⇑(mk' f f' p h) = f

Full source

@[simp]
theorem coe_mk' (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : ⇑(mk' f f' p h) = f :=
  rfl

Underlying Function of Constructed Affine Map Equals Original Function

Informal description

Given a map $f \colon P_1 \to P_2$ between affine spaces, a linear map $f' \colon V_1 \to V_2$ between their associated vector spaces, a point $p \in P_1$, and a proof $h$ that for all $p' \in P_1$, $f(p') = f'(p' - p) + f(p)$, the underlying function of the affine map constructed via `mk'` is equal to $f$.

AffineMap.mk'_linear theorem

(f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : (mk' f f' p h).linear = f'

Full source

@[simp]
theorem mk'_linear (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : (mk' f f' p h).linear = f' :=
  rfl

Linear Part of Constructed Affine Map Equals Given Linear Map

Informal description

Given an affine map constructed via `AffineMap.mk'` from a point map $f \colon P_1 \to P_2$, a linear map $f' \colon V_1 \to V_2$, a base point $p \in P_1$, and a proof $h$ that $f(p') = f'(p' - p) + f(p)$ for all $p' \in P_1$, the linear part of the resulting affine map is equal to $f'$.

AffineMap.mulAction instance

: MulAction R (P1 →ᵃ[k] V2)

Full source

/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain. -/
instance mulAction : MulAction R (P1 →ᵃ[k] V2) where
  smul c f := ⟨c • ⇑f, c • f.linear, fun p v => by simp [smul_add]⟩
  one_smul _ := ext fun _ => one_smul _ _
  mul_smul _ _ _ := ext fun _ => mul_smul _ _ _

Multiplicative Action on Affine Maps to a Module

Informal description

The space of affine maps from an affine space $P_1$ to a module $V_2$ over a ring $k$ inherits a multiplicative action from the action on $V_2$. Specifically, for any scalar $r \in R$ and affine map $f \colon P_1 \to V_2$, the action is defined pointwise as $(r \cdot f)(p) = r \cdot f(p)$ for all $p \in P_1$.

AffineMap.coe_smul theorem

(c : R) (f : P1 →ᵃ[k] V2) : ⇑(c • f) = c • ⇑f

Full source

@[simp, norm_cast]
theorem coe_smul (c : R) (f : P1 →ᵃ[k] V2) : ⇑(c • f) = c • ⇑f :=
  rfl

Pointwise Scalar Multiplication of Affine Maps

Informal description

For any scalar $c$ in a ring $R$ and any affine map $f \colon P_1 \to V_2$ from an affine space $P_1$ to a module $V_2$ over $k$, the function representation of the scalar multiple $c \cdot f$ is equal to the pointwise scalar multiplication of $c$ with the function representation of $f$, i.e., $(c \cdot f)(p) = c \cdot f(p)$ for all $p \in P_1$.

AffineMap.smul_linear theorem

(t : R) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.linear

Full source

@[simp]
theorem smul_linear (t : R) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.linear :=
  rfl

Linear Part of Scaled Affine Map: $(t \cdot f).\text{linear} = t \cdot f.\text{linear}$

Informal description

For any scalar $t \in R$ and any affine map $f \colon P_1 \to V_2$ over a ring $k$, the linear part of the scaled affine map $t \cdot f$ is equal to the scalar multiple $t \cdot (f.\text{linear})$ of the linear part of $f$.

AffineMap.isCentralScalar instance

[DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] : IsCentralScalar R (P1 →ᵃ[k] V2)

Full source

instance isCentralScalar [DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] :
  IsCentralScalar R (P1 →ᵃ[k] V2) where
    op_smul_eq_smul _r _x := ext fun _ => op_smul_eq_smul _ _

Central Scalar Action on Affine Maps to a Module

Informal description

For any ring $k$, affine space $P_1$ over $k$ with associated vector space $V_1$, and module $V_2$ over $k$ equipped with a distributive multiplicative action by $R$ and its multiplicative opposite $R^\text{op}$, if $V_2$ has a central scalar action by $R$, then the space of affine maps $P_1 \toᵃ[k] V_2$ also has a central scalar action by $R$.

AffineMap.instZero instance

: Zero (P1 →ᵃ[k] V2)

Full source

instance : Zero (P1 →ᵃ[k] V2) where zero := ⟨0, 0, fun _ _ => (zero_vadd _ _).symm⟩

Zero Affine Map

Informal description

For affine spaces $P_1$ and $P_2$ over the same ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively, the type of affine maps $P_1 \to P_2$ has a zero element. This zero affine map sends every point in $P_1$ to the origin of $V_2$ (considered as an affine space over itself).

AffineMap.instAdd instance

: Add (P1 →ᵃ[k] V2)

Full source

instance : Add (P1 →ᵃ[k] V2) where
  add f g := ⟨f + g, f.linear + g.linear, fun p v => by simp [add_add_add_comm]⟩

Addition of Affine Maps

Informal description

For affine spaces $P_1$ and $P_2$ over the same ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively, the type of affine maps $P_1 \toᵃ[k] P_2$ has an addition operation. Given two affine maps $f, g \colon P_1 \to P_2$, their sum $f + g$ is the affine map defined by $(f + g)(x) = f(x) + g(x)$ for all $x \in P_1$.

AffineMap.instSub instance

: Sub (P1 →ᵃ[k] V2)

Full source

instance : Sub (P1 →ᵃ[k] V2) where
  sub f g := ⟨f - g, f.linear - g.linear, fun p v => by simp [sub_add_sub_comm]⟩

Subtraction Operation on Affine Maps

Informal description

For affine spaces $P_1$ and $P_2$ over the same ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively, the type of affine maps $P_1 \to P_2$ is equipped with a subtraction operation.

AffineMap.instNeg instance

: Neg (P1 →ᵃ[k] V2)

Full source

instance : Neg (P1 →ᵃ[k] V2) where
  neg f := ⟨-f, -f.linear, fun p v => by simp [add_comm, map_vadd f]⟩

Negation Operation on Affine Maps to Vector Spaces

Informal description

For any affine space $P_1$ over a ring $k$ with associated vector space $V_1$, and any vector space $V_2$ over $k$, the type of affine maps $P_1 \toᵃ[k] V_2$ is equipped with a negation operation.

AffineMap.coe_zero theorem

: ⇑(0 : P1 →ᵃ[k] V2) = 0

Full source

@[simp, norm_cast]
theorem coe_zero : ⇑(0 : P1 →ᵃ[k] V2) = 0 :=
  rfl

Zero Affine Map is the Zero Function

Informal description

For affine spaces $P_1$ over a ring $k$ with associated vector space $V_1$, and $V_2$ considered as an affine space over itself, the zero affine map $0 \colon P_1 \to V_2$ is equal to the zero function, i.e., $0(p) = 0$ for all $p \in P_1$.

AffineMap.coe_add theorem

(f g : P1 →ᵃ[k] V2) : ⇑(f + g) = f + g

Full source

@[simp, norm_cast]
theorem coe_add (f g : P1 →ᵃ[k] V2) : ⇑(f + g) = f + g :=
  rfl

Pointwise Sum of Affine Maps Equals Sum of Functions

Informal description

For any two affine maps $f, g \colon P_1 \to V_2$ between an affine space $P_1$ and a vector space $V_2$ over the same ring $k$, the underlying function of their sum $f + g$ is equal to the pointwise sum of the underlying functions of $f$ and $g$. That is, $(f + g)(p) = f(p) + g(p)$ for all $p \in P_1$.

AffineMap.coe_neg theorem

(f : P1 →ᵃ[k] V2) : ⇑(-f) = -f

Full source

@[simp, norm_cast]
theorem coe_neg (f : P1 →ᵃ[k] V2) : ⇑(-f) = -f :=
  rfl

Negation of Affine Maps is Pointwise Negation

Informal description

For any affine map $f \colon P_1 \to V_2$ from an affine space $P_1$ to a vector space $V_2$ over a ring $k$, the negation of $f$ (as an affine map) is equal to the pointwise negation of $f$ as a function, i.e., $(-f)(p) = -f(p)$ for all $p \in P_1$.

AffineMap.coe_sub theorem

(f g : P1 →ᵃ[k] V2) : ⇑(f - g) = f - g

Full source

@[simp, norm_cast]
theorem coe_sub (f g : P1 →ᵃ[k] V2) : ⇑(f - g) = f - g :=
  rfl

Pointwise Difference of Affine Maps

Informal description

For any two affine maps $f, g \colon P_1 \to V_2$ between an affine space $P_1$ and its associated vector space $V_2$ over a ring $k$, the underlying function of the difference $f - g$ is equal to the pointwise difference of the underlying functions of $f$ and $g$, i.e., $(f - g)(x) = f(x) - g(x)$ for all $x \in P_1$.

AffineMap.zero_linear theorem

: (0 : P1 →ᵃ[k] V2).linear = 0

Full source

@[simp]
theorem zero_linear : (0 : P1 →ᵃ[k] V2).linear = 0 :=
  rfl

Zero Affine Map Has Zero Linear Part

Informal description

For the zero affine map $0 \colon P_1 \to V_2$ between an affine space $P_1$ and its associated vector space $V_2$ over a ring $k$, the underlying linear map is the zero linear map, i.e., $0.\text{linear} = 0$.

AffineMap.add_linear theorem

(f g : P1 →ᵃ[k] V2) : (f + g).linear = f.linear + g.linear

Full source

@[simp]
theorem add_linear (f g : P1 →ᵃ[k] V2) : (f + g).linear = f.linear + g.linear :=
  rfl

Linearity of Sum of Affine Maps

Informal description

For any two affine maps $f, g \colon P_1 \to V_2$ between an affine space $P_1$ and its associated vector space $V_2$ over a ring $k$, the linear part of their sum is equal to the sum of their linear parts, i.e., $(f + g).\text{linear} = f.\text{linear} + g.\text{linear}$.

AffineMap.sub_linear theorem

(f g : P1 →ᵃ[k] V2) : (f - g).linear = f.linear - g.linear

Full source

@[simp]
theorem sub_linear (f g : P1 →ᵃ[k] V2) : (f - g).linear = f.linear - g.linear :=
  rfl

Linear Part of Difference of Affine Maps

Informal description

For any two affine maps $f, g \colon P_1 \to V_2$ between an affine space $P_1$ and its associated vector space $V_2$ over a ring $k$, the linear part of their difference $f - g$ is equal to the difference of their linear parts, i.e., $(f - g).\text{linear} = f.\text{linear} - g.\text{linear}$.

AffineMap.neg_linear theorem

(f : P1 →ᵃ[k] V2) : (-f).linear = -f.linear

Full source

@[simp]
theorem neg_linear (f : P1 →ᵃ[k] V2) : (-f).linear = -f.linear :=
  rfl

Negation of Affine Map's Linear Part

Informal description

For any affine map $f \colon P_1 \to V_2$ between an affine space $P_1$ over a ring $k$ and a vector space $V_2$ over $k$, the linear part of the negation of $f$ is equal to the negation of the linear part of $f$, i.e., $(-f)_{\text{linear}} = -f_{\text{linear}}$.

AffineMap.instAddCommGroup instance

: AddCommGroup (P1 →ᵃ[k] V2)

Full source

/-- The set of affine maps to a vector space is an additive commutative group. -/
instance : AddCommGroup (P1 →ᵃ[k] V2) :=
  coeFn_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => coe_smul _ _)
    fun _ _ => coe_smul _ _

Additive Commutative Group Structure on Affine Maps to a Vector Space

Informal description

For any affine space $P_1$ over a ring $k$ with associated vector space $V_1$, and any vector space $V_2$ over $k$, the set of affine maps $P_1 \to V_2$ forms an additive commutative group under pointwise addition. The group operation is defined by $(f + g)(p) = f(p) + g(p)$, the zero element is the constant zero map, and the inverse of $f$ is given by $(-f)(p) = -f(p)$ for all $p \in P_1$.

AffineMap.instAddTorsor instance

: AffineSpace (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2)

Full source

/-- The space of affine maps from `P1` to `P2` is an affine space over the space of affine maps
from `P1` to the vector space `V2` corresponding to `P2`. -/
instance : AffineSpace (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2) where
  vadd f g :=
    ⟨fun p => f p +ᵥ g p, f.linear + g.linear,
      fun p v => by simp [vadd_vadd, add_right_comm]⟩
  zero_vadd f := ext fun p => zero_vadd _ (f p)
  add_vadd f₁ f₂ f₃ := ext fun p => add_vadd (f₁ p) (f₂ p) (f₃ p)
  vsub f g :=
    ⟨fun p => f p -ᵥ g p, f.linear - g.linear, fun p v => by
      simp [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub, sub_add_eq_add_sub]⟩
  vsub_vadd' f g := ext fun p => vsub_vadd (f p) (g p)
  vadd_vsub' f g := ext fun p => vadd_vsub (f p) (g p)

Affine Space Structure on Affine Maps Between Affine Spaces

Informal description

For any affine spaces $P_1$ and $P_2$ over the same ring $k$, the space of affine maps $P_1 \to P_2$ forms an affine space over the space of affine maps $P_1 \to V_2$, where $V_2$ is the vector space associated to $P_2$. This means that the difference between any two affine maps $f, g \colon P_1 \to P_2$ is an affine map $P_1 \to V_2$, and for any affine map $h \colon P_1 \to V_2$ and any affine map $f \colon P_1 \to P_2$, the sum $h + f$ is well-defined as an affine map $P_1 \to P_2$.

AffineMap.vadd_apply theorem

(f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) : (f +ᵥ g) p = f p +ᵥ g p

Full source

@[simp]
theorem vadd_apply (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) : (f +ᵥ g) p = f p +ᵥ g p :=
  rfl

Evaluation of Vector Addition of Affine Maps

Informal description

For any affine map $f \colon P_1 \to V_2$ and any affine map $g \colon P_1 \to P_2$ over a ring $k$, and for any point $p \in P_1$, the evaluation of the vector addition $f +ᵥ g$ at $p$ equals the vector addition of $f(p)$ and $g(p)$, i.e., $(f +ᵥ g)(p) = f(p) +ᵥ g(p)$.

AffineMap.vsub_apply theorem

(f g : P1 →ᵃ[k] P2) (p : P1) : (f -ᵥ g : P1 →ᵃ[k] V2) p = f p -ᵥ g p

Full source

@[simp]
theorem vsub_apply (f g : P1 →ᵃ[k] P2) (p : P1) : (f -ᵥ g : P1 →ᵃ[k] V2) p = f p -ᵥ g p :=
  rfl

Evaluation of Difference of Affine Maps at a Point

Informal description

For any affine maps $f, g \colon P_1 \to P_2$ between affine spaces over a ring $k$, and any point $p \in P_1$, the evaluation of the difference map $(f - g) \colon P_1 \to V_2$ at $p$ is equal to the difference of the evaluations $f(p) - g(p)$ in the vector space $V_2$ associated to $P_2$.

AffineMap.fst definition

: P1 × P2 →ᵃ[k] P1

Full source

/-- `Prod.fst` as an `AffineMap`. -/
def fst : P1 × P2P1 × P2 →ᵃ[k] P1 where
  toFun := Prod.fst
  linear := LinearMap.fst k V1 V2
  map_vadd' _ _ := rfl

First projection affine map

Informal description

The affine map that projects the first component of a pair $(p_1, p_2) \in P_1 \times P_2$ to $p_1 \in P_1$, where $P_1$ and $P_2$ are affine spaces over the same ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively. The underlying linear map of this affine map is the first projection linear map from $V_1 \times V_2$ to $V_1$.

AffineMap.coe_fst theorem

: ⇑(fst : P1 × P2 →ᵃ[k] P1) = Prod.fst

Full source

@[simp]
theorem coe_fst : ⇑(fst : P1 × P2P1 × P2 →ᵃ[k] P1) = Prod.fst :=
  rfl

First Projection Affine Map Equals Standard First Projection

Informal description

The underlying function of the first projection affine map from the product affine space $P_1 \times P_2$ to $P_1$ is equal to the standard first projection function $\mathrm{Prod.fst} \colon P_1 \times P_2 \to P_1$.

AffineMap.fst_linear theorem

: (fst : P1 × P2 →ᵃ[k] P1).linear = LinearMap.fst k V1 V2

Full source

@[simp]
theorem fst_linear : (fst : P1 × P2P1 × P2 →ᵃ[k] P1).linear = LinearMap.fst k V1 V2 :=
  rfl

Linear Map of First Projection Affine Map Equals First Projection Linear Map

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively. The linear map associated with the first projection affine map $\text{fst} : P_1 \times P_2 \to P_1$ is equal to the first projection linear map $\text{LinearMap.fst} : V_1 \times V_2 \to V_1$.

AffineMap.snd definition

: P1 × P2 →ᵃ[k] P2

Full source

/-- `Prod.snd` as an `AffineMap`. -/
def snd : P1 × P2P1 × P2 →ᵃ[k] P2 where
  toFun := Prod.snd
  linear := LinearMap.snd k V1 V2
  map_vadd' _ _ := rfl

Second projection affine map

Informal description

The affine map from the product affine space $P_1 \times P_2$ to $P_2$ that projects onto the second component. The underlying linear map of this affine map is the second projection linear map from the product vector space $V_1 \times V_2$ to $V_2$.

AffineMap.coe_snd theorem

: ⇑(snd : P1 × P2 →ᵃ[k] P2) = Prod.snd

Full source

@[simp]
theorem coe_snd : ⇑(snd : P1 × P2P1 × P2 →ᵃ[k] P2) = Prod.snd :=
  rfl

Coefficient of Second Projection Affine Map Equals Standard Projection

Informal description

The underlying function of the second projection affine map from the product affine space $P_1 \times P_2$ to $P_2$ is equal to the standard second projection function $\text{Prod.snd} \colon P_1 \times P_2 \to P_2$.

AffineMap.snd_linear theorem

: (snd : P1 × P2 →ᵃ[k] P2).linear = LinearMap.snd k V1 V2

Full source

@[simp]
theorem snd_linear : (snd : P1 × P2P1 × P2 →ᵃ[k] P2).linear = LinearMap.snd k V1 V2 :=
  rfl

Linear Map of Second Projection Affine Map Equals Second Projection Linear Map

Informal description

The linear map associated with the second projection affine map from the product affine space $P_1 \times P_2$ to $P_2$ is equal to the second projection linear map from the product vector space $V_1 \times V_2$ to $V_2$.

AffineMap.id definition

: P1 →ᵃ[k] P1

Full source

/-- Identity map as an affine map. -/
nonrec def id : P1 →ᵃ[k] P1 where
  toFun := id
  linear := LinearMap.id
  map_vadd' _ _ := rfl

Identity affine map

Informal description

The identity map from an affine space $ P_1 $ to itself, considered as an affine map. This map sends each point $ p \in P_1 $ to itself and its associated linear map is the identity linear map on the corresponding vector space $ V_1 $.

AffineMap.coe_id theorem

: ⇑(id k P1) = _root_.id

Full source

/-- The identity affine map acts as the identity. -/
@[simp, norm_cast]
theorem coe_id : ⇑(id k P1) = _root_.id :=
  rfl

Identity Affine Map Equals Standard Identity Function

Informal description

The identity affine map from an affine space $P_1$ to itself, denoted as $\text{id}_k P_1$, is equal to the standard identity function $\text{id}$ on $P_1$.

AffineMap.id_linear theorem

: (id k P1).linear = LinearMap.id

Full source

@[simp]
theorem id_linear : (id k P1).linear = LinearMap.id :=
  rfl

Identity Affine Map's Linear Part is Identity

Informal description

The linear map associated with the identity affine map from an affine space $P_1$ to itself is the identity linear map on the corresponding vector space $V_1$.

AffineMap.id_apply theorem

(p : P1) : id k P1 p = p

Full source

/-- The identity affine map acts as the identity. -/
theorem id_apply (p : P1) : id k P1 p = p :=
  rfl

Identity Affine Map Acts as Identity on Points

Informal description

For any point $p$ in an affine space $P_1$ over a ring $k$, the identity affine map evaluated at $p$ is equal to $p$, i.e., $\text{id}_k P_1(p) = p$.

AffineMap.instInhabited instance

: Inhabited (P1 →ᵃ[k] P1)

Full source

instance : Inhabited (P1 →ᵃ[k] P1) :=
  ⟨id k P1⟩

Inhabited Type of Affine Self-Maps

Informal description

For any affine space $P_1$ over a ring $k$, the type of affine maps from $P_1$ to itself is inhabited.

AffineMap.comp definition

(f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : P1 →ᵃ[k] P3

Full source

/-- Composition of affine maps. -/
def comp (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : P1 →ᵃ[k] P3 where
  toFun := f ∘ g
  linear := f.linear.comp g.linear
  map_vadd' := by
    intro p v
    rw [Function.comp_apply, g.map_vadd, f.map_vadd]
    rfl

Composition of affine maps

Informal description

The composition of two affine maps $f \colon P_2 \to P_3$ and $g \colon P_1 \to P_2$ over the same ring $k$ is an affine map $f \circ g \colon P_1 \to P_3$ whose underlying function is the composition of the underlying functions of $f$ and $g$, and whose linear part is the composition of the linear parts of $f$ and $g$.

AffineMap.coe_comp theorem

(f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : ⇑(f.comp g) = f ∘ g

Full source

/-- Composition of affine maps acts as applying the two functions. -/
@[simp]
theorem coe_comp (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : ⇑(f.comp g) = f ∘ g :=
  rfl

Composition of Affine Maps as Function Composition

Informal description

For any affine maps $f \colon P_2 \to P_3$ and $g \colon P_1 \to P_2$ over the same ring $k$, the underlying function of their composition $f \circ g \colon P_1 \to P_3$ is equal to the composition of the underlying functions of $f$ and $g$, i.e., $(f \circ g)(p) = f(g(p))$ for all $p \in P_1$.

AffineMap.comp_apply theorem

(f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1) : f.comp g p = f (g p)

Full source

/-- Composition of affine maps acts as applying the two functions. -/
theorem comp_apply (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1) : f.comp g p = f (g p) :=
  rfl

Evaluation of Composition of Affine Maps

Informal description

For affine maps $f \colon P_2 \to P_3$ and $g \colon P_1 \to P_2$ over a ring $k$, and any point $p \in P_1$, the composition $f \circ g$ evaluated at $p$ equals $f$ evaluated at $g(p)$, i.e., $(f \circ g)(p) = f(g(p))$.

AffineMap.comp_id theorem

(f : P1 →ᵃ[k] P2) : f.comp (id k P1) = f

Full source

@[simp]
theorem comp_id (f : P1 →ᵃ[k] P2) : f.comp (id k P1) = f :=
  ext fun _ => rfl

Right Identity Law for Composition of Affine Maps

Informal description

For any affine map $f \colon P_1 \to P_2$ over a ring $k$, the composition of $f$ with the identity affine map on $P_1$ equals $f$, i.e., $f \circ \text{id}_{P_1} = f$.

AffineMap.id_comp theorem

(f : P1 →ᵃ[k] P2) : (id k P2).comp f = f

Full source

@[simp]
theorem id_comp (f : P1 →ᵃ[k] P2) : (id k P2).comp f = f :=
  ext fun _ => rfl

Identity Affine Map is Left Identity for Composition

Informal description

For any affine map $f \colon P_1 \to P_2$ over a ring $k$, the composition of the identity affine map on $P_2$ with $f$ is equal to $f$ itself.

AffineMap.comp_assoc theorem

 (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2) : (f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)

Full source

theorem comp_assoc (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2) :
    (f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂) :=
  rfl

Associativity of Affine Map Composition

Informal description

For any affine maps $f_{34} \colon P_3 \to P_4$, $f_{23} \colon P_2 \to P_3$, and $f_{12} \colon P_1 \to P_2$ over the same ring $k$, the composition of affine maps is associative, i.e., $(f_{34} \circ f_{23}) \circ f_{12} = f_{34} \circ (f_{23} \circ f_{12})$.

AffineMap.instMonoid instance

: Monoid (P1 →ᵃ[k] P1)

Full source

instance : Monoid (P1 →ᵃ[k] P1) where
  one := id k P1
  mul := comp
  one_mul := id_comp
  mul_one := comp_id
  mul_assoc := comp_assoc

Monoid Structure on Affine Endomorphisms

Informal description

For any affine space $P_1$ over a ring $k$, the set of affine maps from $P_1$ to itself forms a monoid under composition. The identity element is the identity affine map, and the multiplication operation is given by composition of affine maps.

AffineMap.coe_mul theorem

(f g : P1 →ᵃ[k] P1) : ⇑(f * g) = f ∘ g

Full source

@[simp]
theorem coe_mul (f g : P1 →ᵃ[k] P1) : ⇑(f * g) = f ∘ g :=
  rfl

Composition of Affine Endomorphisms as Function Composition

Informal description

For any two affine endomorphisms $f$ and $g$ of an affine space $P_1$ over a ring $k$, the underlying function of their composition $f * g$ is equal to the function composition $f \circ g$.

AffineMap.coe_one theorem

: ⇑(1 : P1 →ᵃ[k] P1) = _root_.id

Full source

@[simp]
theorem coe_one : ⇑(1 : P1 →ᵃ[k] P1) = _root_.id :=
  rfl

Identity Affine Map is the Identity Function

Informal description

The identity affine map $1 \colon P_1 \toᵃ[k] P_1$ is equal to the identity function $\mathrm{id} \colon P_1 \to P_1$.

AffineMap.linearHom definition

: (P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1

Full source

/-- `AffineMap.linear` on endomorphisms is a `MonoidHom`. -/
@[simps]
def linearHom : (P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1 where
  toFun := linear
  map_one' := rfl
  map_mul' _ _ := rfl

Monoid homomorphism from affine endomorphisms to linear endomorphisms

Informal description

The function `AffineMap.linearHom` is a monoid homomorphism from the monoid of affine endomorphisms of an affine space $P_1$ over a ring $k$ to the monoid of linear endomorphisms of the associated vector space $V_1$. It maps each affine map $f \colon P_1 \to P_1$ to its linear part $f_{\text{linear}} \colon V_1 \to V_1$, preserving the monoid structure (i.e., it maps the identity affine map to the identity linear map and preserves composition).

AffineMap.linear_injective_iff theorem

(f : P1 →ᵃ[k] P2) : Function.Injective f.linear ↔ Function.Injective f

Full source

@[simp]
theorem linear_injective_iff (f : P1 →ᵃ[k] P2) :
    Function.InjectiveFunction.Injective f.linear ↔ Function.Injective f := by
  obtain ⟨p⟩ := (inferInstance : Nonempty P1)
  have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p := by
    ext v
    simp [f.map_vadd, vadd_vsub_assoc]
  rw [h, Equiv.comp_injective, Equiv.injective_comp]

Injectivity of Affine Map and Its Linear Part

Informal description

Let $f \colon P_1 \to P_2$ be an affine map between affine spaces over a ring $k$. The linear part $f_{\text{linear}} \colon V_1 \to V_2$ of $f$ is injective if and only if $f$ itself is injective.

AffineMap.linear_surjective_iff theorem

(f : P1 →ᵃ[k] P2) : Function.Surjective f.linear ↔ Function.Surjective f

Full source

@[simp]
theorem linear_surjective_iff (f : P1 →ᵃ[k] P2) :
    Function.SurjectiveFunction.Surjective f.linear ↔ Function.Surjective f := by
  obtain ⟨p⟩ := (inferInstance : Nonempty P1)
  have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p := by
    ext v
    simp [f.map_vadd, vadd_vsub_assoc]
  rw [h, Equiv.comp_surjective, Equiv.surjective_comp]

Surjectivity of Affine Map and Its Linear Part

Informal description

For an affine map $f \colon P_1 \to P_2$ between affine spaces over a ring $k$, the linear part $f_{\text{linear}} \colon V_1 \to V_2$ is surjective if and only if $f$ itself is surjective.

AffineMap.linear_bijective_iff theorem

(f : P1 →ᵃ[k] P2) : Function.Bijective f.linear ↔ Function.Bijective f

Full source

@[simp]
theorem linear_bijective_iff (f : P1 →ᵃ[k] P2) :
    Function.BijectiveFunction.Bijective f.linear ↔ Function.Bijective f :=
  and_congr f.linear_injective_iff f.linear_surjective_iff

Bijectivity of Affine Map and Its Linear Part

Informal description

Let $f \colon P_1 \to P_2$ be an affine map between affine spaces over a ring $k$. The linear part $f_{\text{linear}} \colon V_1 \to V_2$ of $f$ is bijective if and only if $f$ itself is bijective.

AffineMap.image_vsub_image theorem

{s t : Set P1} (f : P1 →ᵃ[k] P2) : f '' s -ᵥ f '' t = f.linear '' (s -ᵥ t)

Full source

theorem image_vsub_image {s t : Set P1} (f : P1 →ᵃ[k] P2) :
    f '' sf '' s -ᵥ f '' t = f.linear '' (s -ᵥ t) := by
  ext v
  simp only [Set.mem_vsub, Set.mem_image,
    exists_exists_and_eq_and, exists_and_left, ← f.linearMap_vsub]
  constructor
  · rintro ⟨x, hx, y, hy, hv⟩
    exact ⟨x -ᵥ y, ⟨x, hx, y, hy, rfl⟩, hv⟩
  · rintro ⟨-, ⟨x, hx, y, hy, rfl⟩, rfl⟩
    exact ⟨x, hx, y, hy, rfl⟩

Image of Vector Difference under Affine Map Equals Linear Part Applied to Vector Difference

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$ with associated vector spaces $V_1$ and $V_2$ respectively, and let $f \colon P_1 \to P_2$ be an affine map. For any subsets $s, t \subseteq P_1$, the vector difference of the images $f(s) - f(t)$ equals the image under the linear part $f_{\text{linear}}$ of the vector difference $s - t$, i.e., $$ f(s) - f(t) = f_{\text{linear}}(s - t). $$

AffineMap.lineMap definition

(p₀ p₁ : P1) : k →ᵃ[k] P1

Full source

/-- The affine map from `k` to `P1` sending `0` to `p₀` and `1` to `p₁`. -/
def lineMap (p₀ p₁ : P1) : k →ᵃ[k] P1 :=
  ((LinearMap.id : k →ₗ[k] k).smulRight (p₁ -ᵥ p₀)).toAffineMap +ᵥ const k k p₀

Affine line map between two points

Informal description

Given two points $ p_0 $ and $ p_1 $ in an affine space $ P_1 $ over a ring $ k $, the affine map $ \text{lineMap} $ from $ k $ to $ P_1 $ is defined such that it sends $ 0 $ to $ p_0 $ and $ 1 $ to $ p_1 $. For any $ c \in k $, the map is given by $ c \mapsto c \cdot (p_1 - p_0) + p_0 $, where $ p_1 - p_0 $ denotes the vector difference between $ p_1 $ and $ p_0 $.

AffineMap.coe_lineMap theorem

(p₀ p₁ : P1) : (lineMap p₀ p₁ : k → P1) = fun c => c • (p₁ -ᵥ p₀) +ᵥ p₀

Full source

theorem coe_lineMap (p₀ p₁ : P1) : (lineMap p₀ p₁ : k → P1) = fun c => c • (p₁ -ᵥ p₀) +ᵥ p₀ :=
  rfl

Coefficient Form of Affine Line Map: $\text{lineMap}_{p_0,p_1}(c) = c \cdot (p_1 - p_0) + p_0$

Informal description

For any two points $p_0$ and $p_1$ in an affine space $P_1$ over a ring $k$, the affine line map $\text{lineMap}_{p_0,p_1} \colon k \to P_1$ is given by the function $$ c \mapsto c \cdot (p_1 - p_0) + p_0, $$ where $p_1 - p_0$ denotes the vector difference between $p_1$ and $p_0$, and $+$ denotes the action of this vector on the point $p_0$.

AffineMap.lineMap_apply theorem

(p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c = c • (p₁ -ᵥ p₀) +ᵥ p₀

Full source

theorem lineMap_apply (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c = c • (p₁ -ᵥ p₀) +ᵥ p₀ :=
  rfl

Affine Line Map Formula: $\text{lineMap}_{p_0,p_1}(c) = c \cdot (p_1 - p_0) + p_0$

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$. For any two points $p_0, p_1 \in P_1$ and any scalar $c \in k$, the affine line map $\text{lineMap}_{p_0,p_1}$ satisfies \[ \text{lineMap}_{p_0,p_1}(c) = c \cdot (p_1 - p_0) + p_0, \] where $p_1 - p_0$ denotes the vector difference between $p_1$ and $p_0$, and $+$ denotes the action of this vector on the point $p_0$.

AffineMap.lineMap_apply_module' theorem

(p₀ p₁ : V1) (c : k) : lineMap p₀ p₁ c = c • (p₁ - p₀) + p₀

Full source

theorem lineMap_apply_module' (p₀ p₁ : V1) (c : k) : lineMap p₀ p₁ c = c • (p₁ - p₀) + p₀ :=
  rfl

Affine Line Map Formula in Module

Informal description

Let $V_1$ be a module over a ring $k$, and let $p_0, p_1 \in V_1$. For any scalar $c \in k$, the affine line map evaluated at $c$ is given by $\text{lineMap}(p_0, p_1)(c) = c \cdot (p_1 - p_0) + p_0$.

AffineMap.lineMap_apply_module theorem

(p₀ p₁ : V1) (c : k) : lineMap p₀ p₁ c = (1 - c) • p₀ + c • p₁

Full source

theorem lineMap_apply_module (p₀ p₁ : V1) (c : k) : lineMap p₀ p₁ c = (1 - c) • p₀ + c • p₁ := by
  simp [lineMap_apply_module', smul_sub, sub_smul]; abel

Affine Line Map Formula in Module: $\text{lineMap}(p_0, p_1, c) = (1 - c) \cdot p_0 + c \cdot p_1$

Informal description

Let $V_1$ be a module over a ring $k$, and let $p_0, p_1 \in V_1$. For any $c \in k$, the affine line map $\text{lineMap}$ satisfies \[ \text{lineMap}(p_0, p_1, c) = (1 - c) \cdot p_0 + c \cdot p_1. \]

AffineMap.lineMap_apply_ring' theorem

(a b c : k) : lineMap a b c = c * (b - a) + a

Full source

theorem lineMap_apply_ring' (a b c : k) : lineMap a b c = c * (b - a) + a :=
  rfl

Affine Line Map Formula in Ring: $\text{lineMap}(a, b)(c) = c(b - a) + a$

Informal description

For any elements $a, b, c$ in a ring $k$, the affine line map evaluated at $c$ satisfies $\text{lineMap}(a, b)(c) = c \cdot (b - a) + a$.

AffineMap.lineMap_apply_ring theorem

(a b c : k) : lineMap a b c = (1 - c) * a + c * b

Full source

theorem lineMap_apply_ring (a b c : k) : lineMap a b c = (1 - c) * a + c * b :=
  lineMap_apply_module a b c

Affine Line Map Formula in Ring: $\text{lineMap}(a, b)(c) = (1 - c)a + c b$

Informal description

For any elements $a, b, c$ in a ring $k$, the affine line map evaluated at $c$ satisfies \[ \text{lineMap}(a, b)(c) = (1 - c) \cdot a + c \cdot b. \]

AffineMap.lineMap_vadd_apply theorem

(p : P1) (v : V1) (c : k) : lineMap p (v +ᵥ p) c = c • v +ᵥ p

Full source

theorem lineMap_vadd_apply (p : P1) (v : V1) (c : k) : lineMap p (v +ᵥ p) c = c • v +ᵥ p := by
  rw [lineMap_apply, vadd_vsub]

Affine Line Map Formula for Vector Translation: $\text{lineMap}(p, v + p)(c) = c v + p$

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$. For any point $p \in P_1$, any vector $v \in V_1$, and any scalar $c \in k$, the affine line map from $p$ to $v + p$ evaluated at $c$ satisfies \[ \text{lineMap}(p, v + p)(c) = c \cdot v + p. \]

AffineMap.lineMap_linear theorem

(p₀ p₁ : P1) : (lineMap p₀ p₁ : k →ᵃ[k] P1).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀)

Full source

@[simp]
theorem lineMap_linear (p₀ p₁ : P1) :
    (lineMap p₀ p₁ : k →ᵃ[k] P1).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀) :=
  add_zero _

Linear Part of Affine Line Map as Scaled Identity

Informal description

For any two points $p_0$ and $p_1$ in an affine space $P_1$ over a ring $k$, the linear part of the affine line map $\text{lineMap}\, p_0\, p_1 \colon k \to P_1$ is equal to the linear map obtained by scaling the identity map on $k$ by the vector difference $p_1 - p_0$. In other words, the linear part is given by $(\text{id}_k) \cdot (p_1 - p_0)$.

AffineMap.lineMap_same_apply theorem

(p : P1) (c : k) : lineMap p p c = p

Full source

theorem lineMap_same_apply (p : P1) (c : k) : lineMap p p c = p := by
  simp [lineMap_apply]

Fixed Point Property of Affine Line Map

Informal description

For any point $p$ in an affine space $P_1$ over a ring $k$ and any scalar $c \in k$, the affine line map from $p$ to $p$ evaluated at $c$ returns $p$, i.e., $\text{lineMap}(p, p)(c) = p$.

AffineMap.lineMap_same theorem

(p : P1) : lineMap p p = const k k p

Full source

@[simp]
theorem lineMap_same (p : P1) : lineMap p p = const k k p :=
  ext <| lineMap_same_apply p

Affine Line Map Coincides with Constant Map for Identical Points

Informal description

For any point $p$ in an affine space $P_1$ over a ring $k$, the affine line map from $p$ to $p$ is equal to the constant affine map that sends every element of $k$ to $p$.

AffineMap.lineMap_apply_zero theorem

(p₀ p₁ : P1) : lineMap p₀ p₁ (0 : k) = p₀

Full source

@[simp]
theorem lineMap_apply_zero (p₀ p₁ : P1) : lineMap p₀ p₁ (0 : k) = p₀ := by
  simp [lineMap_apply]

Affine Line Map at Zero: $\text{lineMap}(p_0, p_1)(0) = p_0$

Informal description

For any two points $p_0$ and $p_1$ in an affine space $P_1$ over a ring $k$, the affine line map evaluated at $0$ returns $p_0$, i.e., $\text{lineMap}(p_0, p_1)(0) = p_0$.

AffineMap.lineMap_apply_one theorem

(p₀ p₁ : P1) : lineMap p₀ p₁ (1 : k) = p₁

Full source

@[simp]
theorem lineMap_apply_one (p₀ p₁ : P1) : lineMap p₀ p₁ (1 : k) = p₁ := by
  simp [lineMap_apply]

Affine Line Map Evaluates to Second Point at One

Informal description

For any two points $p₀$ and $p₁$ in an affine space $P₁$ over a ring $k$, the affine line map evaluated at $1$ yields $p₁$, i.e., $\text{lineMap}(p₀, p₁)(1) = p₁$.

AffineMap.lineMap_eq_lineMap_iff theorem

 [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k} : lineMap p₀ p₁ c₁ = lineMap p₀ p₁ c₂ ↔ p₀ = p₁ ∨ c₁ = c₂

Full source

@[simp]
theorem lineMap_eq_lineMap_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k} :
    lineMaplineMap p₀ p₁ c₁ = lineMap p₀ p₁ c₂ ↔ p₀ = p₁ ∨ c₁ = c₂ := by
  rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]

Equality of Affine Line Maps: $\text{lineMap}_{p_0,p_1}(c_1) = \text{lineMap}_{p_0,p_1}(c_2) \iff p_0 = p_1 \lor c_1 = c_2$

Informal description

Let $k$ be a ring and $V_1$ be a module over $k$ with no zero scalar multiplication divisors. For any two points $p_0, p_1$ in an affine space $P_1$ over $V_1$, and any scalars $c_1, c_2 \in k$, the affine line maps satisfy \[ \text{lineMap}_{p_0,p_1}(c_1) = \text{lineMap}_{p_0,p_1}(c_2) \] if and only if either $p_0 = p_1$ or $c_1 = c_2$.

AffineMap.lineMap_eq_left_iff theorem

[NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} : lineMap p₀ p₁ c = p₀ ↔ p₀ = p₁ ∨ c = 0

Full source

@[simp]
theorem lineMap_eq_left_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} :
    lineMaplineMap p₀ p₁ c = p₀ ↔ p₀ = p₁ ∨ c = 0 := by
  rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]

Affine Line Map Equals First Point: $\text{lineMap}(p_0, p_1)(c) = p_0 \iff p_0 = p_1 \lor c = 0$

Informal description

Let $k$ be a ring and $V_1$ a module over $k$ with no zero scalar multiplication divisors. For any two points $p_0, p_1$ in an affine space $P_1$ over $V_1$ and any scalar $c \in k$, the affine line map satisfies \[ \text{lineMap}(p_0, p_1)(c) = p_0 \] if and only if either $p_0 = p_1$ or $c = 0$.

AffineMap.lineMap_eq_right_iff theorem

[NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} : lineMap p₀ p₁ c = p₁ ↔ p₀ = p₁ ∨ c = 1

Full source

@[simp]
theorem lineMap_eq_right_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} :
    lineMaplineMap p₀ p₁ c = p₁ ↔ p₀ = p₁ ∨ c = 1 := by
  rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]

Affine Line Map Evaluates to Second Point if and only if Points Coincide or Parameter is One

Informal description

Let $k$ be a ring and $V_1$ be a module over $k$ with no zero scalar multiplication divisors. For any two points $p_0, p_1$ in an affine space $P_1$ over $V_1$, and any scalar $c \in k$, the affine line map satisfies \[ \text{lineMap}(p_0, p_1)(c) = p_1 \] if and only if either $p_0 = p_1$ or $c = 1$.

AffineMap.lineMap_injective theorem

[NoZeroSMulDivisors k V1] {p₀ p₁ : P1} (h : p₀ ≠ p₁) : Function.Injective (lineMap p₀ p₁ : k → P1)

Full source

theorem lineMap_injective [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} (h : p₀ ≠ p₁) :
    Function.Injective (lineMap p₀ p₁ : k → P1) := fun _c₁ _c₂ hc =>
  (lineMap_eq_lineMap_iff.mp hc).resolve_left h

Injectivity of Affine Line Map for Distinct Points

Informal description

Let $k$ be a ring and $V_1$ be a module over $k$ with no zero scalar multiplication divisors. For any two distinct points $p_0, p_1$ in an affine space $P_1$ over $V_1$, the affine line map $\text{lineMap}_{p_0,p_1} \colon k \to P_1$ is injective. That is, for any $c_1, c_2 \in k$, if $\text{lineMap}_{p_0,p_1}(c_1) = \text{lineMap}_{p_0,p_1}(c_2)$, then $c_1 = c_2$.

AffineMap.apply_lineMap theorem

(f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) : f (lineMap p₀ p₁ c) = lineMap (f p₀) (f p₁) c

Full source

@[simp]
theorem apply_lineMap (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) :
    f (lineMap p₀ p₁ c) = lineMap (f p₀) (f p₁) c := by
  simp [lineMap_apply]

Affine Map Preserves Affine Combination

Informal description

Let $f \colon P_1 \to P_2$ be an affine map between affine spaces over a ring $k$, and let $p_0, p_1 \in P_1$ be two points. For any scalar $c \in k$, the image of the affine combination $\text{lineMap}(p_0, p_1)(c) = (1-c) \cdot p_0 + c \cdot p_1$ under $f$ equals the affine combination of the images $f(p_0)$ and $f(p_1)$ with the same coefficient $c$, i.e., $$ f\big(\text{lineMap}(p_0, p_1)(c)\big) = \text{lineMap}(f(p_0), f(p_1))(c). $$

AffineMap.comp_lineMap theorem

(f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) : f.comp (lineMap p₀ p₁) = lineMap (f p₀) (f p₁)

Full source

@[simp]
theorem comp_lineMap (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) :
    f.comp (lineMap p₀ p₁) = lineMap (f p₀) (f p₁) :=
  ext <| f.apply_lineMap p₀ p₁

Composition of Affine Map with Line Map Preserves Linearity

Informal description

Let $f \colon P_1 \to P_2$ be an affine map between affine spaces over a ring $k$, and let $p_0, p_1 \in P_1$. The composition of $f$ with the affine line map $\text{lineMap}(p_0, p_1) \colon k \to P_1$ equals the affine line map between $f(p_0)$ and $f(p_1)$, i.e., $$ f \circ \text{lineMap}(p_0, p_1) = \text{lineMap}(f(p_0), f(p_1)). $$

AffineMap.fst_lineMap theorem

(p₀ p₁ : P1 × P2) (c : k) : (lineMap p₀ p₁ c).1 = lineMap p₀.1 p₁.1 c

Full source

@[simp]
theorem fst_lineMap (p₀ p₁ : P1 × P2) (c : k) : (lineMap p₀ p₁ c).1 = lineMap p₀.1 p₁.1 c :=
  fst.apply_lineMap p₀ p₁ c

First Component of Affine Combination in Product Space

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $p_0 = (p_{01}, p_{02})$, $p_1 = (p_{11}, p_{12})$ be points in $P_1 \times P_2$. For any scalar $c \in k$, the first component of the affine combination $\text{lineMap}(p_0, p_1)(c)$ equals the affine combination of the first components $\text{lineMap}(p_{01}, p_{11})(c)$. In other words, $$ \big(\text{lineMap}(p_0, p_1)(c)\big)_1 = \text{lineMap}(p_{01}, p_{11})(c). $$

AffineMap.snd_lineMap theorem

(p₀ p₁ : P1 × P2) (c : k) : (lineMap p₀ p₁ c).2 = lineMap p₀.2 p₁.2 c

Full source

@[simp]
theorem snd_lineMap (p₀ p₁ : P1 × P2) (c : k) : (lineMap p₀ p₁ c).2 = lineMap p₀.2 p₁.2 c :=
  snd.apply_lineMap p₀ p₁ c

Second Component of Affine Combination in Product Space

Informal description

Let $P_1$ and $P_2$ be affine spaces over a ring $k$, and let $p_0 = (p_0^1, p_0^2)$ and $p_1 = (p_1^1, p_1^2)$ be points in the product affine space $P_1 \times P_2$. For any scalar $c \in k$, the second component of the affine combination $\text{lineMap}(p_0, p_1)(c)$ is equal to the affine combination of the second components $\text{lineMap}(p_0^2, p_1^2)(c)$. In other words, $$ \big(\text{lineMap}(p_0, p_1)(c)\big)_2 = \text{lineMap}(p_0^2, p_1^2)(c). $$

AffineMap.lineMap_symm theorem

(p₀ p₁ : P1) : lineMap p₀ p₁ = (lineMap p₁ p₀).comp (lineMap (1 : k) (0 : k))

Full source

theorem lineMap_symm (p₀ p₁ : P1) :
    lineMap p₀ p₁ = (lineMap p₁ p₀).comp (lineMap (1 : k) (0 : k)) := by
  rw [comp_lineMap]
  simp

Symmetry of Affine Line Map: $\text{lineMap}(p_0, p_1) = \text{lineMap}(p_1, p_0) \circ \text{lineMap}(1, 0)$

Informal description

For any two points $p_0$ and $p_1$ in an affine space $P_1$ over a ring $k$, the affine line map from $p_0$ to $p_1$ is equal to the composition of the affine line map from $p_1$ to $p_0$ with the affine line map from $1$ to $0$ in $k$. In other words, \[ \text{lineMap}(p_0, p_1) = \text{lineMap}(p_1, p_0) \circ \text{lineMap}(1, 0). \]

AffineMap.lineMap_apply_one_sub theorem

(p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ (1 - c) = lineMap p₁ p₀ c

Full source

theorem lineMap_apply_one_sub (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ (1 - c) = lineMap p₁ p₀ c := by
  rw [lineMap_symm p₀, comp_apply]
  congr
  simp [lineMap_apply]

Affine Line Map Symmetry: $\text{lineMap}(p_0, p_1)(1 - c) = \text{lineMap}(p_1, p_0)(c)$

Informal description

For any points $p_0, p_1$ in an affine space $P_1$ over a ring $k$, and any scalar $c \in k$, the affine combination $\text{lineMap}(p_0, p_1)(1 - c)$ equals the affine combination $\text{lineMap}(p_1, p_0)(c)$. In other words, \[ \text{lineMap}(p_0, p_1)(1 - c) = \text{lineMap}(p_1, p_0)(c). \]

AffineMap.lineMap_vsub_left theorem

(p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c -ᵥ p₀ = c • (p₁ -ᵥ p₀)

Full source

@[simp]
theorem lineMap_vsub_left (p₀ p₁ : P1) (c : k) : lineMaplineMap p₀ p₁ c -ᵥ p₀ = c • (p₁ -ᵥ p₀) :=
  vadd_vsub _ _

Vector difference property of affine line map: $\text{lineMap}(p_0, p_1)(c) - p_0 = c \cdot (p_1 - p_0)$

Informal description

For any points $p_0, p_1$ in an affine space $P_1$ over a ring $k$, and any scalar $c \in k$, the vector difference between the point $\text{lineMap}(p_0, p_1)(c)$ and $p_0$ is equal to $c$ times the vector difference between $p_1$ and $p_0$, i.e., \[ \text{lineMap}(p_0, p_1)(c) - p_0 = c \cdot (p_1 - p_0). \]

AffineMap.left_vsub_lineMap theorem

(p₀ p₁ : P1) (c : k) : p₀ -ᵥ lineMap p₀ p₁ c = c • (p₀ -ᵥ p₁)

Full source

@[simp]
theorem left_vsub_lineMap (p₀ p₁ : P1) (c : k) : p₀ -ᵥ lineMap p₀ p₁ c = c • (p₀ -ᵥ p₁) := by
  rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]

Left Vector Difference Property of Affine Line Map: $p_0 - \text{lineMap}(p_0, p_1)(c) = c \cdot (p_0 - p_1)$

Informal description

For any points $p_0, p_1$ in an affine space $P_1$ over a ring $k$, and any scalar $c \in k$, the vector difference between $p_0$ and the point $\text{lineMap}(p_0, p_1)(c)$ is equal to $c$ times the vector difference between $p_0$ and $p_1$, i.e., \[ p_0 - \text{lineMap}(p_0, p_1)(c) = c \cdot (p_0 - p_1). \]

AffineMap.lineMap_vsub_right theorem

(p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)

Full source

@[simp]
theorem lineMap_vsub_right (p₀ p₁ : P1) (c : k) : lineMaplineMap p₀ p₁ c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁) := by
  rw [← lineMap_apply_one_sub, lineMap_vsub_left]

Right Vector Difference Property of Affine Line Map: $\text{lineMap}(p_0, p_1)(c) - p_1 = (1 - c) \cdot (p_0 - p_1)$

Informal description

For any points $p_0, p_1$ in an affine space $P_1$ over a ring $k$, and any scalar $c \in k$, the vector difference between the point $\text{lineMap}(p_0, p_1)(c)$ and $p_1$ is equal to $(1 - c)$ times the vector difference between $p_0$ and $p_1$, i.e., \[ \text{lineMap}(p_0, p_1)(c) - p_1 = (1 - c) \cdot (p_0 - p_1). \]

AffineMap.right_vsub_lineMap theorem

(p₀ p₁ : P1) (c : k) : p₁ -ᵥ lineMap p₀ p₁ c = (1 - c) • (p₁ -ᵥ p₀)

Full source

@[simp]
theorem right_vsub_lineMap (p₀ p₁ : P1) (c : k) : p₁ -ᵥ lineMap p₀ p₁ c = (1 - c) • (p₁ -ᵥ p₀) := by
  rw [← lineMap_apply_one_sub, left_vsub_lineMap]

Right Vector Difference Property of Affine Line Map: $p_1 - \text{lineMap}(p_0, p_1)(c) = (1 - c) \cdot (p_1 - p_0)$

Informal description

For any points $p_0, p_1$ in an affine space $P_1$ over a ring $k$, and any scalar $c \in k$, the vector difference between $p_1$ and the point $\text{lineMap}(p_0, p_1)(c)$ is equal to $(1 - c)$ times the vector difference between $p_1$ and $p_0$, i.e., \[ p_1 - \text{lineMap}(p_0, p_1)(c) = (1 - c) \cdot (p_1 - p_0). \]

AffineMap.lineMap_vadd_lineMap theorem

 (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k) : lineMap v₁ v₂ c +ᵥ lineMap p₁ p₂ c = lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂) c

Full source

theorem lineMap_vadd_lineMap (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k) :
    lineMaplineMap v₁ v₂ c +ᵥ lineMap p₁ p₂ c = lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂) c :=
  ((fst : V1 × P1 →ᵃ[k] V1) +ᵥ (snd : V1 × P1 →ᵃ[k] P1)).apply_lineMap (v₁, p₁) (v₂, p₂) c

Linearity of Affine Combination Under Vector Translation: $\text{lineMap}(v_1, v_2)(c) + \text{lineMap}(p_1, p_2)(c) = \text{lineMap}(v_1 + p_1, v_2 + p_2)(c)$

Informal description

Let $V_1$ be a vector space and $P_1$ an affine space over a ring $k$, with $v_1, v_2 \in V_1$ and $p_1, p_2 \in P_1$. For any scalar $c \in k$, the sum of the vector line map $\text{lineMap}(v_1, v_2)(c)$ and the point line map $\text{lineMap}(p_1, p_2)(c)$ equals the line map of the translated points $\text{lineMap}(v_1 + p_1, v_2 + p_2)(c)$. In other words, $$ \text{lineMap}(v_1, v_2)(c) + \text{lineMap}(p_1, p_2)(c) = \text{lineMap}(v_1 + p_1, v_2 + p_2)(c). $$

AffineMap.lineMap_vsub_lineMap theorem

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

Full source

theorem lineMap_vsub_lineMap (p₁ p₂ p₃ p₄ : P1) (c : k) :
    lineMaplineMap p₁ p₂ c -ᵥ lineMap p₃ p₄ c = lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄) c :=
  ((fst : P1 × P1 →ᵃ[k] P1) -ᵥ (snd : P1 × P1 →ᵃ[k] P1)).apply_lineMap (_, _) (_, _) c

Vector Difference of Affine Line Maps Equals Affine Combination of Vector Differences

Informal description

Let $P_1$ be an affine space over a ring $k$, and let $p_1, p_2, p_3, p_4 \in P_1$. For any $c \in k$, the vector difference between the affine combinations $\text{lineMap}(p_1, p_2)(c)$ and $\text{lineMap}(p_3, p_4)(c)$ is equal to the affine combination of the vector differences $p_1 - p_3$ and $p_2 - p_4$ with the same coefficient $c$. That is, $$ \text{lineMap}(p_1, p_2)(c) - \text{lineMap}(p_3, p_4)(c) = \text{lineMap}(p_1 - p_3, p_2 - p_4)(c). $$

AffineMap.lineMap_lineMap_right theorem

(p₀ p₁ : P1) (c d : k) : lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c)

Full source

@[simp] lemma lineMap_lineMap_right (p₀ p₁ : P1) (c d : k) :
    lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c) := by simp [lineMap_apply, mul_smul]

Composition Property of Affine Line Maps: $\text{lineMap}(p_0, \text{lineMap}(p_0, p_1, c), d) = \text{lineMap}(p_0, p_1, d \cdot c)$

Informal description

Let $P_1$ be an affine space over a ring $k$, and let $p_0, p_1 \in P_1$. For any $c, d \in k$, the composition of the affine line maps satisfies $$ \text{lineMap}(p_0, \text{lineMap}(p_0, p_1, c), d) = \text{lineMap}(p_0, p_1, d \cdot c). $$ Here, $\text{lineMap}(p_0, p_1, t)$ denotes the affine map from $k$ to $P_1$ that sends $0$ to $p_0$ and $1$ to $p_1$, and is given by $t \mapsto t \cdot (p_1 - p_0) + p_0$ for any $t \in k$.

AffineMap.lineMap_lineMap_left theorem

(p₀ p₁ : P1) (c d : k) : lineMap (lineMap p₀ p₁ c) p₁ d = lineMap p₀ p₁ (1 - (1 - d) * (1 - c))

Full source

@[simp] lemma lineMap_lineMap_left (p₀ p₁ : P1) (c d : k) :
    lineMap (lineMap p₀ p₁ c) p₁ d = lineMap p₀ p₁ (1 - (1 - d) * (1 - c)) := by
  simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]

Left Composition Property of Affine Line Maps: $\text{lineMap}(\text{lineMap}(p_0, p_1, c), p_1, d) = \text{lineMap}(p_0, p_1, 1 - (1 - d)(1 - c))$

Informal description

Let $P_1$ be an affine space over a ring $k$, and let $p_0, p_1 \in P_1$. For any $c, d \in k$, the composition of affine line maps satisfies \[ \text{lineMap}(\text{lineMap}(p_0, p_1, c), p_1, d) = \text{lineMap}(p_0, p_1, 1 - (1 - d)(1 - c)). \] Here, $\text{lineMap}(p_0, p_1, t)$ denotes the affine map from $k$ to $P_1$ that sends $0$ to $p_0$ and $1$ to $p_1$, given by $t \mapsto t \cdot (p_1 - p_0) + p_0$ for any $t \in k$.

AffineMap.decomp theorem

(f : V1 →ᵃ[k] V2) : (f : V1 → V2) = ⇑f.linear + fun _ => f 0

Full source

/-- Decomposition of an affine map in the special case when the point space and vector space
are the same. -/
theorem decomp (f : V1 →ᵃ[k] V2) : (f : V1 → V2) = ⇑f.linear + fun _ => f 0 := by
  ext x
  calc
    f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
    _ = (f.linear + fun _ : V1 => f 0) x := rfl

Decomposition of an Affine Map into Linear and Constant Parts

Informal description

Let $f \colon V_1 \to V_2$ be an affine map between vector spaces over a ring $k$. Then $f$ can be decomposed as the sum of its linear part $f_{\text{linear}} \colon V_1 \to V_2$ and a constant function with value $f(0)$, i.e., $$ f(v) = f_{\text{linear}}(v) + f(0) \quad \text{for all } v \in V_1. $$

AffineMap.decomp' theorem

(f : V1 →ᵃ[k] V2) : (f.linear : V1 → V2) = ⇑f - fun _ => f 0

Full source

/-- Decomposition of an affine map in the special case when the point space and vector space
are the same. -/
theorem decomp' (f : V1 →ᵃ[k] V2) : (f.linear : V1 → V2) = ⇑f - fun _ => f 0 := by
  rw [decomp]
  simp only [LinearMap.map_zero, Pi.add_apply, add_sub_cancel_right, zero_add]

Linear Part of Affine Map as Difference from Constant Part

Informal description

Let $f \colon V_1 \to V_2$ be an affine map between vector spaces over a ring $k$. Then the linear part of $f$ can be expressed as the difference between $f$ itself and the constant function with value $f(0)$, i.e., $$ f_{\text{linear}}(v) = f(v) - f(0) \quad \text{for all } v \in V_1. $$

AffineMap.image_uIcc theorem

 {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] (f : k →ᵃ[k] k) (a b : k) :
  f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Full source

theorem image_uIcc {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k]
    (f : k →ᵃ[k] k) (a b : k) :
    f '' Set.uIcc a b = Set.uIcc (f a) (f b) := by
  have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) := by
    ext x
    change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
    rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
    simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
  rw [this, Set.image_comp]
  simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]

Affine Maps Preserve Closed Intervals: $f([a, b]) = [f(a), f(b)]$

Informal description

Let $k$ be a linearly ordered field with a strict ordered ring structure. For any affine map $f \colon k \to k$ and any two elements $a, b \in k$, the image of the closed interval $[a, b]$ under $f$ is equal to the closed interval $[f(a), f(b)]$. In other words: $$ f\big([a, b]\big) = [f(a), f(b)]. $$

AffineMap.proj definition

(i : ι) : (∀ i : ι, P i) →ᵃ[k] P i

Full source

/-- Evaluation at a point as an affine map. -/
def proj (i : ι) : (∀ i : ι, P i) →ᵃ[k] P i where
  toFun f := f i
  linear := @LinearMap.proj k ι _ V _ _ i
  map_vadd' _ _ := rfl

Projection affine map

Informal description

For each index $i$ in the index set $\iota$, the projection map $\text{proj}_i$ is an affine map from the product space $\prod_{i \in \iota} P_i$ to the component space $P_i$. Specifically, $\text{proj}_i$ evaluates a function $f$ at the index $i$, i.e., $\text{proj}_i(f) = f(i)$. The associated linear map of this affine map is the projection linear map $\text{proj}_i$ from the product space $\prod_{i \in \iota} V_i$ to the component space $V_i$, where $V_i$ is the vector space associated with the affine space $P_i$.

AffineMap.proj_apply theorem

(i : ι) (f : ∀ i, P i) : @proj k _ ι V P _ _ _ i f = f i

Full source

@[simp]
theorem proj_apply (i : ι) (f : ∀ i, P i) : @proj k _ ι V P _ _ _ i f = f i :=
  rfl

Projection affine map evaluation: $\text{proj}_i(f) = f(i)$

Informal description

Let $k$ be a ring, $\iota$ an index set, and for each $i \in \iota$, let $P_i$ be an affine space over a vector space $V_i$ with $V_i$ being a module over $k$. For any $i \in \iota$ and any function $f \in \prod_{i \in \iota} P_i$, the projection affine map $\text{proj}_i$ satisfies $\text{proj}_i(f) = f(i)$.

AffineMap.proj_linear theorem

(i : ι) : (@proj k _ ι V P _ _ _ i).linear = @LinearMap.proj k ι _ V _ _ i

Full source

@[simp]
theorem proj_linear (i : ι) : (@proj k _ ι V P _ _ _ i).linear = @LinearMap.proj k ι _ V _ _ i :=
  rfl

Linear Part of Affine Projection Equals Linear Projection

Informal description

For any index $i$ in the index set $\iota$, the linear part of the affine projection map $\text{proj}_i$ from the product affine space $\prod_{i \in \iota} P_i$ to $P_i$ is equal to the linear projection map $\text{proj}_i$ from the product vector space $\prod_{i \in \iota} V_i$ to $V_i$.

AffineMap.pi_lineMap_apply theorem

(f g : ∀ i, P i) (c : k) (i : ι) : lineMap f g c i = lineMap (f i) (g i) c

Full source

theorem pi_lineMap_apply (f g : ∀ i, P i) (c : k) (i : ι) :
    lineMap f g c i = lineMap (f i) (g i) c :=
  (proj i : (∀ i, P i) →ᵃ[k] P i).apply_lineMap f g c

Componentwise Affine Combination of Product Space Points

Informal description

Let $k$ be a ring, $\iota$ an index set, and for each $i \in \iota$, let $P_i$ be an affine space over a vector space $V_i$ with $V_i$ being a module over $k$. For any two points $f, g \in \prod_{i \in \iota} P_i$ and any scalar $c \in k$, the $i$-th component of the affine combination $\text{lineMap}(f, g)(c)$ is equal to the affine combination of the $i$-th components $\text{lineMap}(f(i), g(i))(c)$. In other words, for each $i \in \iota$, $$ \big(\text{lineMap}(f, g)(c)\big)_i = \text{lineMap}(f(i), g(i))(c). $$

AffineMap.distribMulAction instance

: DistribMulAction R (P1 →ᵃ[k] V2)

Full source

/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain. -/
instance distribMulAction : DistribMulAction R (P1 →ᵃ[k] V2) where
  smul_add _ _ _ := ext fun _ => smul_add _ _ _
  smul_zero _ := ext fun _ => smul_zero _

Distributive Multiplicative Action on Affine Maps to a Module

Informal description

The space of affine maps from an affine space $P_1$ to a module $V_2$ over a ring $k$ forms a distributive multiplicative action structure. Specifically, for any scalar $r \in R$ and affine map $f \colon P_1 \to V_2$, the action is defined pointwise as $(r \cdot f)(p) = r \cdot f(p)$ for all $p \in P_1$, and this action distributes over addition of affine maps and scalar multiplication.

AffineMap.instModule instance

: Module R (P1 →ᵃ[k] V2)

Full source

/-- The space of affine maps taking values in an `R`-module is an `R`-module. -/
instance : Module R (P1 →ᵃ[k] V2) :=
  { AffineMap.distribMulAction with
    add_smul := fun _ _ _ => ext fun _ => add_smul _ _ _
    zero_smul := fun _ => ext fun _ => zero_smul _ _ }

Module Structure on Affine Maps to a Vector Space

Informal description

For any ring $R$ and affine space $P_1$ over a vector space $V_1$ with a module structure over a ring $k$, the space of affine maps from $P_1$ to a vector space $V_2$ (also a module over $k$) forms an $R$-module. The module operations are defined pointwise: for affine maps $f, g \colon P_1 \to V_2$ and scalar $r \in R$, we have $(f + g)(p) = f(p) + g(p)$ and $(r \cdot f)(p) = r \cdot f(p)$ for all $p \in P_1$.

AffineMap.toConstProdLinearMap definition

: (V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] V2)

Full source

/-- The space of affine maps between two modules is linearly equivalent to the product of the
domain with the space of linear maps, by taking the value of the affine map at `(0 : V1)` and the
linear part.

See note [bundled maps over different rings] -/
@[simps]
def toConstProdLinearMap : (V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] V2) where
  toFun f := ⟨f 0, f.linear⟩
  invFun p := p.2.toAffineMap + const k V1 p.1
  left_inv f := by
    ext
    rw [f.decomp]
    simp [const_apply]
  right_inv := by
    rintro ⟨v, f⟩
    ext <;> simp [const_apply, const_linear]
  map_add' := by simp
  map_smul' := by simp

Linear equivalence between affine maps and constant-linear pairs

Informal description

The space of affine maps from a vector space $V_1$ to another vector space $V_2$ over the same ring $k$ is linearly equivalent to the product of $V_2$ with the space of linear maps from $V_1$ to $V_2$. The equivalence is given by evaluating the affine map at the zero vector (to obtain the constant term) and taking its linear part.

AffineMap.pi definition

(f : (i : ι) → (P1 →ᵃ[k] φp i)) : P1 →ᵃ[k] ((i : ι) → φp i)

Full source

/-- `pi` construction for affine maps. From a family of affine maps it produces an affine
map into a family of affine spaces.

This is the affine version of `LinearMap.pi`.
-/
def pi (f : (i : ι) → (P1 →ᵃ[k] φp i)) : P1 →ᵃ[k] ((i : ι) → φp i) where
  toFun m a := f a m
  linear := LinearMap.pi (fun a ↦ (f a).linear)
  map_vadd' _ _ := funext fun _ ↦ map_vadd _ _ _

Affine map into a product space

Informal description

Given a family of affine maps $ f_i \colon P_1 \to \varphi_i $ indexed by $ i \in \iota $, the function `AffineMap.pi` constructs an affine map from $ P_1 $ to the product space $ \prod_{i \in \iota} \varphi_i $, defined by $ m \mapsto (f_i(m))_{i \in \iota} $. The associated linear map is constructed using the linear parts of each $ f_i $.

AffineMap.pi_apply theorem

(c : P1) (i : ι) : pi fp c i = fp i c

Full source

@[simp]
theorem pi_apply (c : P1) (i : ι) : pi fp c i = fp i c :=
  rfl

Componentwise Evaluation of Affine Map Product

Informal description

For any point $c$ in an affine space $P_1$ and any index $i$ in the index set $\iota$, the $i$-th component of the affine map $\text{pi}(f)(c)$ is equal to the evaluation of the $i$-th affine map $f_i$ at $c$, i.e., $(\text{pi}(f)(c))_i = f_i(c)$.

AffineMap.pi_comp theorem

(g : P3 →ᵃ[k] P1) : (pi fp).comp g = pi (fun i => (fp i).comp g)

Full source

theorem pi_comp (g : P3 →ᵃ[k] P1) : (pi fp).comp g = pi (fun i => (fp i).comp g) :=
  rfl

Composition of Product Affine Maps with a Common Map

Informal description

Let $P_1$, $P_2$, and $P_3$ be affine spaces over a ring $k$, with associated vector spaces $V_1$, $V_2$, and $V_3$ respectively. Given a family of affine maps $(f_i \colon P_1 \to P_2)_{i \in \iota}$ and an affine map $g \colon P_3 \to P_1$, the composition of the product affine map $\prod_{i} f_i$ with $g$ equals the product of the compositions $(f_i \circ g)_{i \in \iota}$. In other words, $(\prod_{i} f_i) \circ g = \prod_{i} (f_i \circ g)$.

AffineMap.pi_eq_zero theorem

: pi fv = 0 ↔ ∀ i, fv i = 0

Full source

theorem pi_eq_zero : pipi fv = 0 ↔ ∀ i, fv i = 0 := by
  simp only [AffineMap.ext_iff, funext_iff, pi_apply]
  exact forall_comm

$\pi f = 0$ if and only if all $f_i = 0$

Informal description

For a family of affine maps $f_i \colon P_1 \to V_2$ indexed by $i \in \iota$, the affine map $\pi f$ constructed from this family is the zero map if and only if each $f_i$ is the zero map.

AffineMap.pi_zero theorem

: pi (fun _ ↦ 0 : (i : ι) → P1 →ᵃ[k] φv i) = 0

Full source

theorem pi_zero : pi (fun _ ↦ 0 : (i : ι) → P1 →ᵃ[k] φv i) = 0 := by
  ext; rfl

Zero Family Yields Zero Affine Map in Product Space

Informal description

For any index set $\iota$ and any family of affine maps $f_i \colon P_1 \to \varphi_i$ that are identically zero for all $i \in \iota$, the affine map $\pi(f)$ constructed from this family is equal to the zero affine map.

AffineMap.proj_pi theorem

(i : ι) : (proj i).comp (pi fp) = fp i

Full source

theorem proj_pi (i : ι) : (proj i).comp (pi fp) = fp i :=
  ext fun _ => rfl

Projection-Pi Composition Equals Component Affine Map

Informal description

For any index $i$ in the index set $\iota$, the composition of the projection affine map $\text{proj}_i$ with the affine map $\text{pi} \, fp$ (where $fp$ is a family of affine maps indexed by $\iota$) equals the $i$-th affine map $fp_i$ in the family.

AffineMap.pi_ext_zero theorem

(h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) (h₂ : f 0 = g 0) : f = g

Full source

/-- Two affine maps from a Pi-type of modules `(i : ι) → φv i` are equal if they are equal in their
  operation on `Pi.single` and at zero. Analogous to `LinearMap.pi_ext`. See also `pi_ext_nonempty`,
  which instead of agreement at zero requires `Nonempty ι`. -/
theorem pi_ext_zero (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) (h₂ : f 0 = g 0) :
    f = g := by
  apply ext_linear
  · apply LinearMap.pi_ext
    intro i x
    have s₁ := h i x
    have s₂ := f.map_vadd 0 (Pi.single i x)
    have s₃ := g.map_vadd 0 (Pi.single i x)
    rw [vadd_eq_add, add_zero] at s₂ s₃
    replace h₂ := h i 0
    simp only [Pi.single_zero] at h₂
    rwa [s₂, s₃, h₂, vadd_right_cancel_iff] at s₁
  · exact h₂

Extensionality of Affine Maps on Product Space via Single Components and Zero

Informal description

Let $k$ be a ring, $\iota$ a finite index set, and $\{\varphi_i\}_{i \in \iota}$ a family of modules over $k$ with affine spaces $P_1$ and $\prod_{i \in \iota} \varphi_i$. For two affine maps $f, g \colon P_1 \to \prod_{i \in \iota} \varphi_i$, if for every $i \in \iota$ and every $x \in \varphi_i$ we have $f(\text{single}_i(x)) = g(\text{single}_i(x))$, where $\text{single}_i(x)$ is the element with $x$ in the $i$-th coordinate and zero elsewhere, and additionally $f(0) = g(0)$, then $f = g$.

AffineMap.pi_ext_nonempty theorem

[Nonempty ι] (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) : f = g

Full source

/-- Two affine maps from a Pi-type of modules `(i : ι) → φv i` are equal if they are equal in their
  operation on `Pi.single` and `ι` is nonempty.  Analogous to `LinearMap.pi_ext`. See also
  `pi_ext_zero`, which instead of `Nonempty ι` requires agreement at 0. -/
theorem pi_ext_nonempty [Nonempty ι] (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) :
    f = g := by
  apply pi_ext_zero h
  inhabit ι
  rw [← Pi.single_zero default]
  apply h

Extensionality of Affine Maps on Product Space via Single Components (Nonempty Case)

Informal description

Let $\iota$ be a nonempty index set and $\{\varphi_i\}_{i \in \iota}$ a family of modules over a ring $k$. For two affine maps $f, g \colon P_1 \to \prod_{i \in \iota} \varphi_i$, if for every $i \in \iota$ and every $x \in \varphi_i$ we have $f(\text{single}_i(x)) = g(\text{single}_i(x))$, where $\text{single}_i(x)$ is the element with $x$ in the $i$-th coordinate and zero elsewhere, then $f = g$.

AffineMap.pi_ext_nonempty' theorem

 [Nonempty ι] (h : ∀ i, f.comp (LinearMap.single _ _ i).toAffineMap = g.comp (LinearMap.single _ _ i).toAffineMap) :
  f = g

Full source

/-- This is used as the ext lemma instead of `AffineMap.pi_ext_nonempty` for reasons explained in
note [partially-applied ext lemmas]. Analogous to `LinearMap.pi_ext'` -/
@[ext (iff := false)]
theorem pi_ext_nonempty' [Nonempty ι] (h : ∀ i, f.comp (LinearMap.single _ _ i).toAffineMap =
    g.comp (LinearMap.single _ _ i).toAffineMap) : f = g := by
  refine pi_ext_nonempty fun i x => ?_
  convert AffineMap.congr_fun (h i) x

Extensionality of Affine Maps via Componentwise Composition with Linear Embeddings (Nonempty Case)

Informal description

Let $\iota$ be a nonempty index set and $k$ a ring. For two affine maps $f, g \colon P_1 \to \prod_{i \in \iota} \varphi_i$ (where each $\varphi_i$ is a module over $k$), if for every $i \in \iota$ the composition $f \circ \text{single}_i$ equals $g \circ \text{single}_i$ (where $\text{single}_i \colon \varphi_i \to \prod_{j \in \iota} \varphi_j$ is the canonical linear embedding), then $f = g$.

AffineMap.homothety definition

(c : P1) (r : k) : P1 →ᵃ[k] P1

Full source

/-- `homothety c r` is the homothety (also known as dilation) about `c` with scale factor `r`. -/
def homothety (c : P1) (r : k) : P1 →ᵃ[k] P1 :=
  r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c

Homothety (Dilation) in an Affine Space

Informal description

Given a point $ c $ in an affine space $ P_1 $ over a ring $ k $ and a scalar $ r \in k $, the homothety (or dilation) centered at $ c $ with scaling factor $ r $ is the affine map $ P_1 \to P_1 $ defined by $ p \mapsto r \cdot (p - c) + c $, where $ p - c $ denotes the vector from $ c $ to $ p $ in the associated vector space $ V_1 $.

AffineMap.homothety_def theorem

(c : P1) (r : k) : homothety c r = r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c

Full source

theorem homothety_def (c : P1) (r : k) :
    homothety c r = r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c :=
  rfl

Homothety as Linear Combination of Affine Maps: $\text{homothety}_c(r) = r \cdot (\text{id} - \text{const}_c) + \text{const}_c$

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$. For any point $c \in P_1$ and scalar $r \in k$, the homothety (scaling transformation) centered at $c$ with scaling factor $r$ can be expressed as: \[ \text{homothety}(c, r) = r \cdot (\text{id}_{P_1} - \text{const}_c) + \text{const}_c \] where $\text{id}_{P_1}$ is the identity affine map on $P_1$, $\text{const}_c$ is the constant affine map sending all points to $c$, and $-$ denotes the subtraction of affine maps (yielding an affine map to $V_1$).

AffineMap.homothety_apply theorem

(c : P1) (r : k) (p : P1) : homothety c r p = r • (p -ᵥ c : V1) +ᵥ c

Full source

theorem homothety_apply (c : P1) (r : k) (p : P1) : homothety c r p = r • (p -ᵥ c : V1) +ᵥ c :=
  rfl

Homothety Transformation Formula: $\text{homothety}(c, r)(p) = r \cdot (p - c) + c$

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$. For any point $c \in P_1$, scalar $r \in k$, and point $p \in P_1$, the homothety (scaling transformation) centered at $c$ with scaling factor $r$ maps $p$ to $r \cdot (p - c) + c$, where $p - c$ denotes the vector from $c$ to $p$ in $V_1$.

AffineMap.homothety_eq_lineMap theorem

(c : P1) (r : k) (p : P1) : homothety c r p = lineMap c p r

Full source

theorem homothety_eq_lineMap (c : P1) (r : k) (p : P1) : homothety c r p = lineMap c p r :=
  rfl

Homothety as Affine Line Map: $\text{homothety}_c(r)(p) = \text{lineMap}(c, p)(r)$

Informal description

Let $P_1$ be an affine space over a ring $k$ with associated vector space $V_1$. For any point $c \in P_1$, scalar $r \in k$, and point $p \in P_1$, the homothety (dilation) centered at $c$ with scaling factor $r$ applied to $p$ equals the affine line map from $c$ to $p$ evaluated at $r$, i.e., \[ \text{homothety}_c(r)(p) = \text{lineMap}(c, p)(r). \]

AffineMap.homothety_one theorem

(c : P1) : homothety c (1 : k) = id k P1

Full source

@[simp]
theorem homothety_one (c : P1) : homothety c (1 : k) = id k P1 := by
  ext p
  simp [homothety_apply]

Homothety with Scaling Factor One is Identity

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, the homothety centered at $c$ with scaling factor $1$ is equal to the identity affine map on $P_1$.

AffineMap.homothety_apply_same theorem

(c : P1) (r : k) : homothety c r c = c

Full source

@[simp]
theorem homothety_apply_same (c : P1) (r : k) : homothety c r c = c :=
  lineMap_same_apply c r

Fixed Point Property of Homothety: $\text{homothety}_c(r)(c) = c$

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$ and any scalar $r \in k$, the homothety (dilation) centered at $c$ with scaling factor $r$ maps $c$ to itself, i.e., $\text{homothety}_c(r)(c) = c$.

AffineMap.homothety_mul_apply theorem

(c : P1) (r₁ r₂ : k) (p : P1) : homothety c (r₁ * r₂) p = homothety c r₁ (homothety c r₂ p)

Full source

theorem homothety_mul_apply (c : P1) (r₁ r₂ : k) (p : P1) :
    homothety c (r₁ * r₂) p = homothety c r₁ (homothety c r₂ p) := by
  simp only [homothety_apply, mul_smul, vadd_vsub]

Composition Property of Homothety: $\text{homothety}_c(r_1 r_2)(p) = \text{homothety}_c(r_1)(\text{homothety}_c(r_2)(p))$

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, and for any scalars $r_1, r_2 \in k$, the homothety centered at $c$ with scaling factor $r_1 \cdot r_2$ applied to a point $p \in P_1$ is equal to the homothety with scaling factor $r_1$ applied to the result of the homothety with scaling factor $r_2$ applied to $p$. In other words: \[ \text{homothety}_c(r_1 \cdot r_2)(p) = \text{homothety}_c(r_1)(\text{homothety}_c(r_2)(p)) \]

AffineMap.homothety_mul theorem

(c : P1) (r₁ r₂ : k) : homothety c (r₁ * r₂) = (homothety c r₁).comp (homothety c r₂)

Full source

theorem homothety_mul (c : P1) (r₁ r₂ : k) :
    homothety c (r₁ * r₂) = (homothety c r₁).comp (homothety c r₂) :=
  ext <| homothety_mul_apply c r₁ r₂

Composition of Homotheties: $\text{homothety}_c(r_1 r_2) = \text{homothety}_c(r_1) \circ \text{homothety}_c(r_2)$

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, and for any scalars $r_1, r_2 \in k$, the homothety centered at $c$ with scaling factor $r_1 \cdot r_2$ is equal to the composition of the homothety with scaling factor $r_1$ and the homothety with scaling factor $r_2$, both centered at $c$. In other words: \[ \text{homothety}_c(r_1 \cdot r_2) = \text{homothety}_c(r_1) \circ \text{homothety}_c(r_2) \]

AffineMap.homothety_zero theorem

(c : P1) : homothety c (0 : k) = const k P1 c

Full source

@[simp]
theorem homothety_zero (c : P1) : homothety c (0 : k) = const k P1 c := by
  ext p
  simp [homothety_apply]

Homothety with Zero Scaling Factor is Constant Map

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, the homothety centered at $c$ with scaling factor $0$ is equal to the constant affine map that sends every point in $P_1$ to $c$.

AffineMap.homothety_add theorem

(c : P1) (r₁ r₂ : k) : homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂

Full source

@[simp]
theorem homothety_add (c : P1) (r₁ r₂ : k) :
    homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂ := by
  simp only [homothety_def, add_smul, vadd_vadd]

Additivity of Homothety with Respect to Scaling Factor

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, and any scalars $r_1, r_2 \in k$, the homothety centered at $c$ with scaling factor $r_1 + r_2$ is equal to the sum of the homothety centered at $c$ with scaling factor $r_2$ and the scalar multiple $r_1$ applied to the affine map $\text{id}_{k P_1} - \text{const}_{k P_1} c$. Here, $\text{id}_{k P_1}$ denotes the identity affine map on $P_1$, $\text{const}_{k P_1} c$ is the constant affine map sending every point in $P_1$ to $c$, and $+ᵥ$ denotes the addition operation in the affine space of affine maps.

AffineMap.homothetyHom definition

(c : P1) : k →* P1 →ᵃ[k] P1

Full source

/-- `homothety` as a multiplicative monoid homomorphism. -/
def homothetyHom (c : P1) : k →* P1 →ᵃ[k] P1 where
  toFun := homothety c
  map_one' := homothety_one c
  map_mul' := homothety_mul c

Homothety as a multiplicative monoid homomorphism

Informal description

For a fixed point $ c $ in an affine space $ P_1 $ over a ring $ k $, the function $ \text{homothetyHom} $ maps each scalar $ r \in k $ to the homothety (scaling transformation) centered at $ c $ with scaling factor $ r $. This function is a multiplicative monoid homomorphism from the multiplicative monoid of $ k $ to the monoid of affine endomorphisms of $ P_1 $, meaning it preserves the multiplicative identity and the operation of multiplication. Specifically: - The multiplicative identity $ 1 \in k $ is mapped to the identity affine map on $ P_1 $. - The product $ r_1 \cdot r_2 $ is mapped to the composition of the homotheties with scaling factors $ r_1 $ and $ r_2 $.

AffineMap.coe_homothetyHom theorem

(c : P1) : ⇑(homothetyHom c : k →* _) = homothety c

Full source

@[simp]
theorem coe_homothetyHom (c : P1) : ⇑(homothetyHom c : k →* _) = homothety c :=
  rfl

Underlying Function of Homothety Monoid Homomorphism Equals Homothety Function

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, the underlying function of the monoid homomorphism $\text{homothetyHom}\, c \colon k \to (P_1 \to P_1)$ is equal to the homothety function centered at $c$. That is, for any scalar $r \in k$, we have $(\text{homothetyHom}\, c)(r) = \text{homothety}\, c\, r$.

AffineMap.homothetyAffine definition

(c : P1) : k →ᵃ[k] P1 →ᵃ[k] P1

Full source

/-- `homothety` as an affine map. -/
def homothetyAffine (c : P1) : k →ᵃ[k] P1 →ᵃ[k] P1 :=
  ⟨homothety c, (LinearMap.lsmul k _).flip (id k P1 -ᵥ const k P1 c),
    Function.swap (homothety_add c)⟩

Homothety as an affine map

Informal description

Given a point $ c $ in an affine space $ P_1 $ over a ring $ k $, the map $ \text{homothetyAffine} $ sends each scalar $ r \in k $ to the affine map $ \text{homothety} \, c \, r \colon P_1 \to P_1 $, which is the homothety (scaling transformation) centered at $ c $ with scaling factor $ r $. The associated linear map is the flip of the scalar multiplication bilinear map applied to the identity map minus the constant map at $ c $.

AffineMap.coe_homothetyAffine theorem

(c : P1) : ⇑(homothetyAffine c : k →ᵃ[k] _) = homothety c

Full source

@[simp]
theorem coe_homothetyAffine (c : P1) : ⇑(homothetyAffine c : k →ᵃ[k] _) = homothety c :=
  rfl

Underlying Function of Homothety Affine Map Equals Homothety Function

Informal description

For any point $c$ in an affine space $P_1$ over a ring $k$, the underlying function of the affine map $\text{homothetyAffine}\, c \colon k \to (P_1 \to P_1)$ is equal to the homothety function centered at $c$, i.e., for any scalar $r \in k$, we have $(\text{homothetyAffine}\, c)(r) = \text{homothety}\, c\, r$.

Convex.combo_affine_apply theorem

{x y : E} {a b : 𝕜} {f : E →ᵃ[𝕜] F} (h : a + b = 1) : f (a • x + b • y) = a • f x + b • f y

Full source

/-- Applying an affine map to an affine combination of two points yields an affine combination of
the images. -/
theorem Convex.combo_affine_apply {x y : E} {a b : 𝕜} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
    f (a • x + b • y) = a • f x + b • f y := by
  simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]
  exact f.apply_lineMap _ _ _

Affine Map Preserves Affine Combination

Informal description

Let $E$ and $F$ be affine spaces over a field $\mathbb{k}$, and let $f \colon E \to F$ be an affine map. For any points $x, y \in E$ and scalars $a, b \in \mathbb{k}$ such that $a + b = 1$, the image of the affine combination $a \cdot x + b \cdot y$ under $f$ is equal to the affine combination of the images with the same coefficients, i.e., $$ f(a \cdot x + b \cdot y) = a \cdot f(x) + b \cdot f(y). $$

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Main definitions

Notations

Implementation notes

References