isCardinalFiltered_under — Mathlib

English

If J is κ-filtered for a regular cardinal κ, then for any object j0 in J, the comma/under category Under j0 inherits the κ-filtered property.

Русский

Пусть J — категория и κ — регулярный кардинал. Пусть J κ-фильтрована. Тогда для любого объекта j0∈J категория Under j0 тоже κ-фильтрована.

LaTeX

$$$\operatorname{IsCardinalFiltered}(\mathrm{Under}(j_0), \kappa)$$$

Lean4

instance isCardinalFiltered_under (J : Type u) [Category.{v} J] (κ : Cardinal.{w}) [Fact κ.IsRegular]
    [IsCardinalFiltered J κ] (j₀ : J) : IsCardinalFiltered (Under j₀) κ where
  nonempty_cocone {A _} F
    hA :=
    ⟨by
      have := isFiltered_of_isCardinalFiltered J κ
      let c := cocone (F ⋙ Under.forget j₀) hA
      let x (a : A) : j₀ ⟶ IsFiltered.max j₀ c.pt := (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
      have hκ' : HasCardinalLT A κ := hasCardinalLT_of_hasCardinalLT_arrow hA
      exact
        { pt := Under.mk (toCoeq x hκ')
          ι :=
            { app
                a :=
                Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ')
                  (by simpa [x] using coeq_condition x hκ' a)
              naturality a b
                f := by
                ext
                have := c.w f
                dsimp at this ⊢
                simp only [reassoc_of% this, Category.comp_id] } }⟩

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