preservesColimit_coyoneda_obj_of_mono

English

In the surjectivity construction, the object F(z) is an isomorphism object; i.e., F(z) is invertible.

Русский

В конструировании сюръективности F(z) является изоморфным объектом; то есть F(z) обратим.

LaTeX

$$$\text{IsIso}(F(z))$$$

Lean4

/-- If `X` is an object in a Grothendieck abelian category, then
the functor `coyoneda.obj (op X)` commutes with colimits corresponding
to diagrams of monomorphisms indexed by `κ`-filtered categories
for a big enough regular cardinal `κ`. -/
theorem preservesColimit_coyoneda_obj_of_mono (Y : J ⥤ C) {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
    [IsCardinalFiltered J κ] (hXκ : HasCardinalLT (Subobject X) κ) [∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)] :
    PreservesColimit Y ((coyoneda.obj (op X))) where
  preserves {c}
    hc :=
    ⟨by
      have := isFiltered_of_isCardinalFiltered J κ
      exact Types.FilteredColimit.isColimitOf' _ _ (surjectivity hc hXκ) (injectivity hc hXκ)⟩

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