isGrothendieckAbelian — Mathlib

English

ShrinkHoms(C) inherits Grothendieck abelian structure from C when C is abelian and Grothendieck.

Русский

ShrinkHoms(C) наследует Гротениджеву абелевость от C, если C абелева и Гротенджев абелев.

LaTeX

$$$\mathrm{IsGrothendieckAbelian}(\mathrm{ShrinkHoms}(C))$$$

Lean4

instance isGrothendieckAbelian [Abelian C] [IsGrothendieckAbelian.{w} C] :
    IsGrothendieckAbelian.{w, w} (ShrinkHoms C) :=
  IsGrothendieckAbelian.of_equivalence <| ShrinkHoms.equivalence C

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