reflectsColimit_of_natIso — Mathlib

English

If F ≅ G and F has a limit of K, then G reflects the limit of K.

Русский

Если F ≅ G и F имеет предел для K, то G отражает этот предел.

LaTeX

$$$F \\cong G \\Rightarrow [\\mathrm{ReflectsLimit}\\,K\\,F] \\Rightarrow [\\mathrm{ReflectsLimit}\\,K\\,G]$$$

Lean4

/-- Transfer reflection of a colimit along a natural isomorphism in the functor. -/
theorem reflectsColimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimit K F] : ReflectsColimit K G
    where reflects t := ReflectsColimit.reflects (IsColimit.mapCoconeEquiv h.symm t)

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