instLinear — Mathlib

English

There is a linear structure on the category TopModuleCat over S: Hom-sets are S-modules and composition is S-bilinear.

Русский

Существуют линейные структуры над S на категорию TopModuleCat: множества гомоморфизмов являются S-модулями, а композиция билинейна по обеим сторонам.

LaTeX

$$$ \text{TopModuleCat over } S \text{ is linear: } \forall f,g,h, (f \gg g) + (f \gg h) = f \gg (g + h) \wedge (f + g) \gg h = f \gg h + g \gg h $$$

Lean4

instance [CommRing S] : Linear S (TopModuleCat S)
    where
  smul_comp _ _ _ _ _ _ := ConcreteCategory.ext (ContinuousLinearMap.comp_smul _ _ _)
  comp_smul _ _ _ _ _ _ := ConcreteCategory.ext (ContinuousLinearMap.smul_comp _ _ _)

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