reflectsLimit_of_iso_diagram — Mathlib

English

If F ≅ G and F reflects a limit of K, then G reflects that limit as well.

Русский

Если F изоморфен G и F отражает предел для диаграммы K, то и G отражает этот предел.

LaTeX

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

Lean4

/-- Transfer reflection of limits along a natural isomorphism in the diagram. -/
theorem reflectsLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [ReflectsLimit K₁ F] : ReflectsLimit K₂ F
    where
  reflects {c}
    t :=
    ⟨by
      apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)
      apply ((IsLimit.postcomposeInvEquiv (Functor.isoWhiskerRight h F :) _).symm t).ofIsoLimit _
      exact Cones.ext (Iso.refl _)⟩

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