toBilinHom — Mathlib

English

For a fixed basis bm, Q ↦ Q.toBilin bm defines an S-linear map from QuadraticMap R M N to BilinMap R M N. In other words, Q ↦ Q.toBilin bm is linear over S.

Русский

Для фиксированной базы bm отображение Q ↦ Q.toBilin bm задаёт S- линейное отображение между QuadraticMap и BilinMap.

LaTeX

$$$ toBilinHom\\, bm : QuadraticMap\\ R\\ M\\ N \\to_{S} BilinMap\\ R\\ M\\ N$ с линейностью по S.$$

Lean4

/-- `QuadraticMap.toBilin` as an S-linear map -/
@[simps]
noncomputable def toBilinHom (bm : Basis ι R M) : QuadraticMap R M N →ₗ[S] BilinMap R M N
    where
  toFun Q := Q.toBilin bm
  map_add' := add_toBilin bm
  map_smul' := smul_toBilin S bm

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