id_preservesLimitsOfSize — Mathlib

English

The identity functor preserves all limits of all sizes; i.e., PreservesLimitsOfSize (Id_C) for every size.

Русский

Тождественный функтор сохраняет все пределы всех размеров; то есть PreservesLimitsOfSize (Id_C) для любого размера.

LaTeX

$$$$\text{PreservesLimitsOfSize}((\mathrm{Id}_C))\text{ for all sizes.}$$$$

Lean4

instance id_preservesLimitsOfSize : PreservesLimitsOfSize.{w', w} (𝟭 C) where
  preservesLimitsOfShape {J}
    𝒥 :=
    {
      preservesLimit := 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⟩⟩ }

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