isConnected_iff_colimit_constPUnitFunctor_iso_pUnit

English

IsConnected C is equivalent to the existence of an isomorphism colimit(constPUnitFunctor C) ≅ PUnit.

Русский

Связанность C эквивалентна существованию изоморфизма колимит (constPUnitFunctor C) ≅ PUnit.

LaTeX

$$$\text{IsConnected}(C) \iff \text{Nonempty}\left(\colimit(\text{constPUnitFunctor } C) \cong PUnit\right)$$$

Lean4

/-- An index category is connected iff the colimit of the constant singleton-valued functor is a
singleton. -/
theorem isConnected_iff_colimit_constPUnitFunctor_iso_pUnit [HasColimit (constPUnitFunctor.{w} C)] :
    IsConnected C ↔ Nonempty (colimit (constPUnitFunctor.{w} C) ≅ PUnit) :=
  by
  refine ⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩
  have : Nonempty C := nonempty_of_nonempty_colimit <| Nonempty.map h.inv inferInstance
  refine zigzag_isConnected <| fun c d => ?_
  refine zigzag_of_eqvGen_colimitTypeRel _ (constPUnitFunctor C) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩ ?_
  exact colimit_eq <| h.toEquiv.injective rfl

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