reflectsLimitsOfShape_of_equiv — Mathlib

English

If J ≌ J' is an equivalence of shapes and F : C → D reflects limits of shape J, then F reflects limits of shape J'.

Русский

Если J ≌ J' — эквивалент форм диаграмм и F: C → D отражает предел по форме J, тогда F отражает предел по форме J'.

LaTeX

$$$e : J \\simeq J' \\;\\Rightarrow\\; [\\mathrm{ReflectsLimitsOfShape}\\,J\\,F] \\Rightarrow [\\mathrm{ReflectsLimitsOfShape}\\,J'\\,F]$$$

Lean4

/-- Transfer reflection of limits along an equivalence in the shape. -/
theorem reflectsLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J' F where
  reflectsLimit
    {K} :=
    {
      reflects := fun {c} t =>
        ⟨by
          apply IsLimit.ofWhiskerEquivalence e
          apply isLimitOfReflects F
          apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
          exact IsLimit.whiskerEquivalence t _⟩ }

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