English
There is a linear equivalence between the space of affine maps and the product of the codomain with the space of linear maps, sending f to (f(0), f.linear).
Русский
Существует линейное биективное соответствие между пространством аффинных отображений и произведением кодомого пространства на пространство линейных отображений; переход осуществляется по f ↦ (f(0), f.linear).
LaTeX
$$$ toConstProdLinearMap : (V_1 \\toᵃ[k] V_2) \\simeqₗ[R] V_2 \\times (V_1 \\toₗ[k] V_2) $$$
Lean4
/-- 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
right_inv := by
rintro ⟨v, f⟩
ext <;> simp [const_linear]
map_add' := by simp
map_smul' := by simp
