preservesFiniteColimits_liftToFinset

English

A category with finite biproducts and finite limits is AB4* if it is AB5Star.

Русский

Категория с конечными бинпродуктами и конечными пределами AB4*, если она AB5Star.

LaTeX

$$$\\operatorname{AB4StarOfSize}(C) \\Leftarrow \\operatorname{AB5StarOfSize}(C) \\text{ и т.д.}$$$

Lean4

instance preservesFiniteColimits_liftToFinset : PreservesFiniteColimits (liftToFinset C α) :=
  preservesFiniteColimits_of_evaluation _ fun ⟨I⟩ =>
    letI : PreservesFiniteColimits (lim (J := Discrete I) (C := C)) :=
      preservesFiniteColimits_of_natIso HasBiproductsOfShape.colimIsoLim
    letI : PreservesFiniteColimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj (Discrete.functor fun x ↦ ↑x)) :=
      ⟨fun _ _ _ => inferInstance⟩
    letI :
      PreservesFiniteColimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj (Discrete.functor (·.val)) ⋙ lim) :=
      comp_preservesFiniteColimits _ _
    preservesFiniteColimits_of_natIso (liftToFinsetEvaluationIso _ _ I).symm

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