English
If f : P2 → P3 and g : P1 → P2 are affines, then f ∘ g is an affine map with toFun = f ∘ g, linear = f.linear ∘ g.linear, and the compatibility with vadd holds.
Русский
Если f: P2 → P3 и g: P1 → P2 — аффинные отображения, то их композиция f ∘ g — аффинное отображение с toFun = f ∘ g, линейной частью = f.linear ∘ g.linear, и соблюдением правила d по vadd.
LaTeX
$$$\\text{comp}(f,g): P1 \\to^a_k P3$ с $\\text{toFun} = f \\circ g$, $\\text{linear} = f.linear \\circ g.linear$, и $\\text{map\_vadd}'$ выполняется.$$
Lean4
/-- Composition of affine maps. -/
@[simps linear]
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
