coeLM — Mathlib

English

Let h: M₂ →SL[σ₂₃] M₃ be σ₂₃-semi-linear, and f: M →SL[σ₁₂] M₂ be σ₁₂-semi-linear. Then composition is compatible with scalar actions: the formula expresses how h.comp(c • f) relates to σ₂₃ c acting on h.comp f.

Русский

Пусть отображение h: M₂ →SL[σ₂₃] M₃ полулинейно, а f: M →SL[σ₁₂] M₂ также полулинейно. Тогда композиция совместима с действием скаляров: отношение h.comp(c • f) к σ₂₃ c действует на h.comp f.

LaTeX

$$$$ h \circ (c \cdot f) = (\sigma_{23} c) \cdot (h \circ f). $$$$

Lean4

/-- The coercion from `M →L[R] M₂` to `M →ₗ[R] M₂`, as a linear map. -/
@[simps]
def coeLM : (M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃ where
  toFun := (↑)
  map_add' f g := coe_add f g
  map_smul' c f := coe_smul c f

Похожие утверждения