English
If J is filtered, then the morphism f(z) is epi in the presentable isomorphism framework.
Русский
Если J фильтрован, то отображение f(z) является эпиморфизмом в рамках презентируемой изоморфности.
LaTeX
$$$ [IsFiltered J] \Rightarrow Epi (f z) $$$
Lean4
theorem isIso_f [IsFiltered J] : IsIso (f z) :=
by
refine
((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
(MorphismProperty.of_isPullback ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)
· refine
Arrow.isoMk (Iso.refl _) (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isColimitConstCocone J X)) ?_
dsimp
ext j
rw [Category.id_comp, ι_colimMap_assoc, colimit.comp_coconePointUniqueUpToIso_hom, constCocone_ι, NatTrans.id_app,
Category.comp_id]
apply hf
· refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).2 (inferInstanceAs (IsIso (𝟙 c.pt)))
exact
Arrow.isoMk (IsColimit.coconePointUniqueUpToIso (colimit.isColimit Y) hc)
(IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isColimitConstCocone J c.pt))
