id_reflectsColimits — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance id_reflectsColimits : ReflectsColimitsOfSize.{w, w'} (𝟭 C) where
  reflectsColimitsOfShape {J}
    𝒥 :=
    {
      reflectsColimit := 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⟩⟩ }

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