English
For any W, there is a relation W ≤ W.colimitsOfShape(Discrete PUnit) indicating every morphism is mediated by a colimit over PUnit.
Русский
Для любого W выполняется отношение W ≤ W.colimitsOfShape(Discrete PUnit), то есть любой морфизм относится к колимиту по PUnit.
LaTeX
$$W \le W.colimitsOfShape(Discrete PUnit)$$
Lean4
theorem le_colimitsOfShape_punit : W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1}) :=
by
intro X₁ X₂ f hf
have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))
let c₁ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₁)) h
let c₂ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₂)) h
have hc₁ : IsColimit c₁ := colimitOfDiagramInitial h _
have hc₂ : IsColimit c₂ := colimitOfDiagramInitial h _
have : hc₁.desc (Cocone.mk _ (Discrete.natTrans (fun _ ↦ by exact f) ≫ c₂.ι)) = f :=
hc₁.hom_ext
(fun x ↦ by
obtain rfl : x = ⊥_ _ := by ext
rw [IsColimit.fac]
simp [c₁, c₂])
rw [← this]
exact ⟨_, _, _, _, _, hc₂, _, fun _ ↦ hf⟩
