English
If f: M2 →ₛₗ[σ23] M3 and g: M1 →ₛₗ[σ12] M2 are semilinear maps, then their composition f ∘ g is a semilinear map M1 →ₛₗ[σ13] M3, i.e., the composition of two semilinear maps is again semilinear.
Русский
Если f: M2 →ₛₗ[σ23] M3 и g: M1 →ₛₗ[σ12] M2 — полулинейные отображения, то их композиция f ∘ g является полулинейным отображением M1 →ₛₗ[σ13] M3; то есть композиция двух полилинейных отображений снова полилинейна.
LaTeX
$$$\forall f:\ M_2 \to_{\sigma_{23}} M_3\,\forall g:\ M_1 \to_{\sigma_{12}} M_2:\; (f \circ g): M_1 \to_{\sigma_{13}} M_3.$$$
Lean4
/-- Composition of two linear maps is a linear map -/
def comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₃] M₃
where
toFun := f ∘ g
map_add' := by
simp only [map_add, forall_const, Function.comp_apply]
-- Note that https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` to `map_smulₛₗ _`
map_smul' r x := by simp only [Function.comp_apply, map_smulₛₗ _, RingHomCompTriple.comp_apply]
