preservesColimit — Mathlib

English

If a relative cell complex structure hf is built from a family I.homFamily with respect to a regular cardinal κ, then hf.F preserves the colimit of the coyoneda diagram at A.

Русский

Если структура hf — относительная клеточная комплексность, построенная из семейства I.homFamily относительно регулярного кардинала κ, то hf.F сохраняет колимит Coyoneda в позиции A.

LaTeX

$$$\\mathrm{PreservesColimit}\\, hf.F\\; (\\mathrm{coyoneda}.\\mathrm{obj}(\\mathrm{Opposite}.op\\, A))$$$

Lean4

theorem preservesColimit {A B X Y : C} (i : A ⟶ B) (hi : I i) (f : X ⟶ Y)
    (hf : RelativeCellComplex.{w} (fun (_ : κ.ord.toType) ↦ I.homFamily) f) :
    PreservesColimit hf.F (coyoneda.obj (Opposite.op A)) :=
  IsCardinalForSmallObjectArgument.preservesColimit i hi f hf

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