coeLMₛₗ — Mathlib

English

There is a canonical linear map that forgets the σ-structure from ContinuousLinearMap to ContinuousLinearMap with identity ring homs, connecting σ₁₃ to R.

Русский

Существует каноническое линейное отображение, забывающее σ-структуру между типами ContinuousLinearMap и связанное через единичный морфизм кольца.

LaTeX

$$$$ \text{coeLM}_{R,S}(f) : M \toSL[σ_{13}] M_3 \; \mapsto \; f, $$$$

Lean4

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

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