English
The operation vadd from P1 →ᵃ[k] V2 and P1 →ᵃ[k] P2 defines an additive action on the fiber-wise additions.
Русский
Операция vadd из аффинных отображений задает аддитивное действие на волокнистых сложениях по точкам.
LaTeX
$$$f \,+_V\, g := \langle p \mapsto f(p) +_V g(p), \; f_{linear}+g_{linear}, \; \cdots \rangle$$$
Lean4
/-- 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, 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)
