instSubsingletonColimitPUnit — Mathlib

English

If C is preconnected and HasColimit (constPUnitFunctor C), then colimit (constPUnitFunctor C) is a Subsingleton (i.e., has at most one element up to equality).

Русский

Если C предсвязно и существует колимит константного п-функторa, то колимит константного п-функторa является одноэлементным объектом.

LaTeX

$$$\operatorname{Subsingleton}(\operatorname{colimit}(\text{constPUnitFunctor } C))$$$

Lean4

instance instSubsingletonColimitPUnit [IsPreconnected C] [HasColimit (constPUnitFunctor.{w} C)] :
    Subsingleton (colimit (constPUnitFunctor.{w} C)) where
  allEq a
    b := by
    obtain ⟨c, ⟨⟩, rfl⟩ := jointly_surjective' a
    obtain ⟨d, ⟨⟩, rfl⟩ := jointly_surjective' b
    apply constant_of_preserves_morphisms (colimit.ι (constPUnitFunctor C) · PUnit.unit)
    exact fun c d f => colimit_sound f rfl

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