English
For a cocone c over F, c.IsColimit holds if and only if the transported cocone under F.coconeTypesEquiv has a colimit structure. In other words, c is colimiting exactly when the corresponding cocone in Type via the equivalence is a colimit.
Русский
Для кокона c над F множество IsColimit верно тогда и только тогда, когда соответствующий кокон в Type, полученный через эквивалентность F.coconeTypesEquiv, образует колимит.
LaTeX
$$$$ c.IsColimit \iff Nonempty( Limits.IsColimit ( F.coconeTypesEquiv c ) ). $$$$
Lean4
theorem isColimit_iff (c : CoconeTypes.{u} F) : c.IsColimit ↔ Nonempty (Limits.IsColimit (F.coconeTypesEquiv c)) :=
by
constructor
· intro hc
exact
⟨{ desc s := hc.desc (F.coconeTypesEquiv.symm s)
fac s j := hc.fac (F.coconeTypesEquiv.symm s) j
uniq s m
hm :=
hc.funext
(fun j ↦ by
rw [hc.fac]
exact hm j) }⟩
· rintro ⟨hc⟩
classical
refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
· let f (z : F.ColimitType) : ULift.{u} Bool := ULift.up (x = z)
suffices f x = f y by simpa [f] using this
have : (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))).comp (F.descColimitType c) = f :=
by
ext z
obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
exact congr_fun (hc.fac _ j) z
simp only [← this, coconeTypesEquiv_apply_pt, Function.comp_apply, h]
· let f₁ : c.pt ⟶ ULift.{u} Bool := fun _ => ULift.up true
let f₂ : c.pt ⟶ ULift.{u} Bool := fun x => ULift.up (∃ a, F.descColimitType c a = x)
suffices f₁ = f₂ by simpa [f₁, f₂] using congrFun this x
refine hc.hom_ext fun j => funext fun x => ?_
simpa [f₁, f₂] using ⟨F.ιColimitType j x, by simp⟩
