well_copowered_costructuredArrow — Mathlib

English

Dually, if C is well-copowered and cocomplete and S preserves colimits, then CostructuredArrow S T is well-copowered.

Русский

Тот же факт для противоположной структуры: CostructuredArrow S T хорошо-порожденна.

LaTeX

$$$[\\text{WellPowered } (C^{op})] \\Rightarrow [\\text{WellPowered } (CostructuredArrow S T)^{op}].$$$

Lean4

/-- If `C` is well-copowered and cocomplete and `S` preserves colimits, then
    `CostructuredArrow S T` is well-copowered. -/
instance well_copowered_costructuredArrow [LocallySmall.{w} C] [WellPowered.{w} Cᵒᵖ] [HasFiniteColimits C]
    [PreservesFiniteColimits S] : WellPowered.{w} (CostructuredArrow S T)ᵒᵖ where
  subobject_small X := small_map (quotientEquiv (unop X)).toEquiv

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