reflectsColimit_of_iso_diagram — Mathlib

English

If K₁ ≅ K₂ and F reflects a colimit for K₁, then F reflects a colimit for K₂.

Русский

Если K₁ ≅ K₂ и F отражает колимит для K₁, то F отражает колимит для K₂.

LaTeX

$$$F \\text{ reflects }\\mathrm{Colimit}\\,K_1 \\Rightarrow F \\text{ reflects }\\mathrm{Colimit}\\,K_2 \\text{ when } K_1 \\cong K_2$$$

Lean4

/-- Transfer reflection of colimits along a natural isomorphism in the diagram. -/
theorem reflectsColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsColimit K₁ F] :
    ReflectsColimit K₂ F where
  reflects {c}
    t :=
    ⟨by
      apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
      apply ((IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h F :) _).symm t).ofIsoColimit _
      exact Cocones.ext (Iso.refl _)⟩

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