finitaryExtensive_of_preserves_and_reflects_isomorphism

English

If there exists an isomorphism making the given diagram universal, then the base category is finitary extensive.

Русский

Если существует изоморфизм, делающий данный диаграмм универсальным, то базовая категория — конечная расширяемая.

LaTeX

$$$FinitaryExtensive\; C$ if a certain universal isomorphism exists for diagrams.$$

Lean4

theorem finitaryExtensive_of_preserves_and_reflects_isomorphism (F : C ⥤ D) [FinitaryExtensive D]
    [HasFiniteCoproducts C] [HasPullbacks C] [PreservesLimitsOfShape WalkingCospan F]
    [PreservesColimitsOfShape (Discrete WalkingPair) F] [F.ReflectsIsomorphisms] : FinitaryExtensive C :=
  by
  haveI : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShape_of_reflectsIsomorphisms
  haveI : ReflectsColimitsOfShape (Discrete WalkingPair) F := reflectsColimitsOfShape_of_reflectsIsomorphisms
  exact finitaryExtensive_of_preserves_and_reflects F

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