id_reflectsLimits — Mathlib

English

The identity functor preserves and reflects limits of size; hence reflects limits of shape 0.

Русский

Идентичный функтор сохраняет и отражает предельные свойства; в частности отражает пределы формы.

LaTeX

$$$ \\text{ReflectsLimitsOfSize}^{(\\mathrm{id})}(\\mathrm{Id}_C). $$$

Lean4

instance id_reflectsLimits : ReflectsLimitsOfSize.{w, w'} (𝟭 C) where
  reflectsLimitsOfShape {J}
    𝒥 :=
    {
      reflectsLimit := fun {K} =>
        ⟨fun {c} h =>
          ⟨fun s => h.lift ⟨s.pt, fun j => s.π.app j, fun _ _ f => s.π.naturality f⟩, by cases K;
            rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j, by cases K; rcases c with ⟨_, _, _⟩;
            intro s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ }

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