instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat

English

A converse: if colimits commute with finite limits, then K is filtered.

Русский

Обратное: если колимиты коммутируют с конечными пределами, значит K — фильтрована.

LaTeX

$$$\text{If } (\forall J, [SmallCategory J][FinCategory J] (F : J ⥤ K ⥤ Type), Nonempty(\lim(\mathrm{colimit} F.flip) ⟶ \mathrm{colimit}(\lim F))) \Rightarrow IsFiltered(K)$$$

Lean4

instance [IsFilteredOrEmpty C] [∀ c, IsFilteredOrEmpty (F.obj c)] : IsFilteredOrEmpty (Grothendieck F) :=
  by
  refine ⟨?_, ?_⟩
  · rintro ⟨c, f⟩ ⟨d, g⟩
    exact
      ⟨⟨max c d, max ((F.map (leftToMax c d)).obj f) ((F.map (rightToMax c d)).obj g)⟩, ⟨leftToMax c d, leftToMax _ _⟩,
        ⟨rightToMax c d, rightToMax _ _⟩, trivial⟩
  · rintro ⟨c, f⟩ ⟨d, g⟩ ⟨u, x⟩ ⟨v, y⟩
    refine
      ⟨⟨coeq u v, coeq (eqToHom ?_ ≫ (F.map (coeqHom u v)).map x) ((F.map (coeqHom u v)).map y)⟩,
        ⟨coeqHom u v, coeqHom _ _⟩, ?_⟩
    · conv_rhs => rw [← Cat.comp_obj, ← F.map_comp, coeq_condition, F.map_comp, Cat.comp_obj]
    · apply Grothendieck.ext _ _ (coeq_condition u v)
      refine Eq.trans ?_ (eqToHom _ ≫= coeq_condition _ _)
      simp

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