reflectsLimits_of_isEquivalence — Mathlib

English

If E is an equivalence, E reflects limits; i.e., a diagram is a limit iff its image under E is a limit.

Русский

Если E — эквивалентность, она отражает пределы; тождество диаграммы является пределом тогда и только тогда, когда её образ E — предел.

LaTeX

$$$$ E \\text{ isEquivalence } \\Rightarrow \\mathrm{ReflectsLimitsOfSize}(E). $$$$

Lean4

noncomputable instance (priority := 100) _root_.CategoryTheory.Functor.reflectsLimits_of_isEquivalence (E : D ⥤ C)
    [E.IsEquivalence] : ReflectsLimitsOfSize.{v, u} E where
  reflectsLimitsOfShape :=
    {
      reflectsLimit :=
        { reflects := fun t => ⟨(isLimitOfPreserves E.inv t).mapConeEquiv E.asEquivalence.unitIso.symm⟩ } }
      -- see Note [lower instance priority]

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