English
If C has colimits and G preserves them, and G reflects isomorphisms, then G reflects colimits of shape J.
Русский
Если в C существуют колимиты, и G сохраняет их, и G отражает изоморфизмы, то G отражает колимиты формы J.
LaTeX
$$$\\text{HasColimitsOfShape } J\\; C \\land\\text{PreservesColimitsOfShape } J\\, G \\land\\text{ReflectsIsomorphisms } G \\Rightarrow \\text{ReflectsColimitsOfShape } J\\, G$$$
Lean4
/-- If the colimit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it
reflects the colimit of `F`.
-/ -- Porting note: previous behavior of apply pushed instance holes into hypotheses, this errors
theorem reflectsColimit_of_reflectsIsomorphisms (F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms] [HasColimit F]
[PreservesColimit F G] : ReflectsColimit F G where
reflects {c}
t :=
by
suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from ⟨by apply IsColimit.ofPointIso (colimit.isColimit F)⟩
change IsIso ((Cocones.forget _).map ((colimit.isColimit F).descCoconeMorphism c))
suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by apply (Cocones.forget F).map_isIso _
suffices IsIso ((Cocones.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c)) from by
apply isIso_of_reflects_iso _ (Cocones.functoriality F G)
exact (isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _
