mono_ι_app_of_isFiltered — Mathlib

English

Same as previous: mono inclusion in colimit cocone under filtered indices.

Русский

То же самое: моно включение в кокон колимита при фильтрованных индексах.

LaTeX

$$$\\text{Mono}(c.ι.app j_0)$ under hypotheses$$

Lean4

/-- Assume that a functor `X : J ⥤ C` maps any morphism to a monomorphism,
that `J` is filtered. Then the "inclusion" map `c.ι.app j₀` of a colimit cocone for `X`
is a monomorphism if `colim : (Under j₀ ⥤ C) ⥤ C` preserves monomorphisms
(e.g. when `C` satisfies AB5). -/
theorem mono_ι_app_of_isFiltered {X : J ⥤ C} [∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)] {c : Cocone X}
    (hc : IsColimit c) [IsFiltered J] (j₀ : J) [HasColimitsOfShape (Under j₀) C]
    [(colim : (Under j₀ ⥤ C) ⥤ C).PreservesMonomorphisms] : Mono (c.ι.app j₀) :=
  by
  let f : (Functor.const _).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
    { app j := X.map j.hom
      naturality _ _
        g := by
        dsimp
        simp only [Category.id_comp, ← X.map_comp, Under.w] }
  have := NatTrans.mono_of_mono_app f
  exact
    colim.map_mono' f (isColimitConstCocone _ _) ((Functor.Final.isColimitWhiskerEquiv _ _).symm hc) (c.ι.app j₀)
      (by cat_disch)

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