id_preservesColimitsOfSize — Mathlib

English

The identity functor preserves all colimits of all sizes; i.e., PreservesColimitsOfSize (Id_C).

Русский

Тождественный функтор сохраняет все колимиты всех размеров; то есть PreservesColimitsOfSize (Id_C).

LaTeX

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

Lean4

instance id_preservesColimitsOfSize : PreservesColimitsOfSize.{w', w} (𝟭 C) where
  preservesColimitsOfShape {J}
    𝒥 :=
    {
      preservesColimit := fun {K} =>
        ⟨fun {c} h =>
          ⟨fun s => h.desc ⟨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⟩⟩ }

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