of_equivalence — Mathlib

English

If C is abelian and Grothendieck abelian, then the Ind-category Ind(C) is Grothendieck abelian (refined).

Русский

Если C абелева и Гротенджевабелева, то Ind(C) — снова Гротенджеджабелева (уточнено).

LaTeX

$$$\mathrm{IsGrothendieckAbelian}(\mathrm{Ind}\,C)$$$

Lean4

theorem of_equivalence [Abelian C] [Abelian D] [IsGrothendieckAbelian.{w} C] (α : C ≌ D) :
    IsGrothendieckAbelian.{w} D :=
  by
  have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
    ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩
  refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
  · exact locallySmall_of_faithful α.inverse
  · refine ⟨fun _ _ _ => ?_⟩
    exact HasExactColimitsOfShape.of_codomain_equivalence _ α
  · exact HasSeparator.of_equivalence α

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