English
The total category Total P is filtered, provided each I j is filtered and each diag object is finitely presentable.
Русский
Общность Total P является фильтрованной, если каждый I j фильтрован и каждый диагональный объект презентируем.
LaTeX
$$$IsFiltered(Total P)$$$
Lean4
instance [IsFiltered J] [∀ j, IsFiltered (I j)] [∀ j i, IsFinitelyPresentable.{w} ((P j).diag.obj i)] :
IsFiltered (Total P)
where
cocone_objs k
l := by
let a := IsFiltered.max k.1 l.1
obtain ⟨a', f, hf⟩ := Total.exists_hom_of_hom (P := P) k.2 (IsFiltered.leftToMax k.1 l.1)
obtain ⟨b', g, hg⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.rightToMax k.1 l.1)
refine ⟨⟨a, IsFiltered.max a' b'⟩, ?_, ?_, trivial⟩
· exact f ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.leftToMax _ _) }
· exact g ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.rightToMax _ _) }
cocone_maps {k l} f
g := by
let a := IsFiltered.coeq f.base g.base
obtain ⟨a', u, hu⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.coeqHom f.base g.base)
have : (f.hom ≫ u.hom) ≫ (P _).ι.app _ = (g.hom ≫ u.hom) ≫ (P _).ι.app _ :=
by
simp only [Category.assoc, Functor.const_obj_obj, ← u.w, ← f.w_assoc, ← g.w_assoc]
rw [← Functor.map_comp, hu, IsFiltered.coeq_condition f.base g.base]
simp
obtain ⟨j, p, q, hpq⟩ := IsFinitelyPresentable.exists_eq_of_isColimit (P _).isColimit _ _ this
dsimp at p q
refine ⟨⟨a, IsFiltered.coeq p q⟩, u ≫ { base := 𝟙 _, hom := (P _).diag.map (p ≫ IsFiltered.coeqHom p q) }, ?_⟩
apply Total.Hom.ext
· simp [hu, IsFiltered.coeq_condition f.base g.base]
· rw [Category.assoc] at hpq
simp only [Functor.map_comp, comp_hom, reassoc_of% hpq]
simp [← Functor.map_comp, ← IsFiltered.coeq_condition]
