fullSubcategoryInclusionLinear — Mathlib

English

If Z is an object property defining a full subcategory ι: Z → C, then the inclusion ι is an R-linear functor.

Русский

Если Z задаёт полную подпредставляющую подкатегорию ι: Z → C, тогда включение ι является R-линейным функтором.

LaTeX

$$$\\iota: Z \\hookrightarrow C \\text{ is } R\\text{-linear}. $$$

Lean4

instance fullSubcategoryInclusionLinear {C : Type*} [Category C] [Preadditive C] [CategoryTheory.Linear R C]
    (Z : ObjectProperty C) : Z.ι.Linear R where

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