isConnected_iff_isColimit_pUnitCocone

English

IsConnected C is equivalent to the existence of a colimit cocone at pUnit, i.e., Nonempty (IsColimit (pUnitCocone C)).

Русский

Связанность C эквивалентна существованию колимитного коконa в pUnit, то есть Nonempty (IsColimit (pUnitCocone C)).

LaTeX

$$$\text{IsConnected}(C) \iff \text{Nonempty}\left(\text{IsColimit}(\text{pUnitCocone}(C))\right)$$$

Lean4

theorem isConnected_iff_isColimit_pUnitCocone : IsConnected C ↔ Nonempty (IsColimit (pUnitCocone.{w} C)) :=
  by
  refine ⟨fun inst => ⟨isColimitPUnitCocone C⟩, fun ⟨h⟩ => ?_⟩
  let colimitCocone : ColimitCocone (constPUnitFunctor C) := ⟨pUnitCocone.{w} C, h⟩
  have : HasColimit (constPUnitFunctor.{w} C) := ⟨⟨colimitCocone⟩⟩
  simp only [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{w} C]
  exact ⟨colimit.isoColimitCocone colimitCocone⟩

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