instIsFilteredOrEmptyFullSubcategoryFilteredClosure

English

The Grothendieck construction preserves filteredness: if C is filtered and each (F.obj c).α is filtered, then Grothendieck F is filtered.

Русский

Конструкция Гротендика сохраняет фильтрованность: если C фильтрована и каждый (F.obj c).α фильтрован, то Grothendieck F фильтрована.

LaTeX

$$$[IsFiltered C] \land [\forall c, IsFiltered ((F.obj c).α)] \Rightarrow IsFiltered (Grothendieck F)$$$

Lean4

/-- The full subcategory induced by the filtered closure of a family of objects is filtered. -/
instance : IsFilteredOrEmpty (filteredClosure f).FullSubcategory
    where
  cocone_objs j j' := ⟨⟨max j.1 j'.1, filteredClosure.max j.2 j'.2⟩, leftToMax _ _, rightToMax _ _, trivial⟩
  cocone_maps {j j'} f
    f' := ⟨⟨coeq f f', filteredClosure.coeq j.2 j'.2 f f'⟩, coeqHom (C := C) f f', coeq_condition _ _⟩

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