instAlgebraEnd — Mathlib

English

If C is a linear category over R and F: D → C is a functor, then the induced category InducedCategory C F is linear over R.

Русский

Если C — линейная категория над R и F: D → C — функтор, то индуцированная категория InducedCategory C F линейна над R.

LaTeX

$$$\\operatorname{Linear}(R,\\operatorname{InducedCategory}(C,F)).$$$

Lean4

instance [CommSemiring R] [Linear R C] (X : C) : Algebra R (End X) :=
  Algebra.ofModule (fun _ _ _ => comp_smul _ _ _ _ _ _) fun _ _ _ => smul_comp _ _ _ _ _ _

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