Lean4
/-- (Implementation detail)
The cocone associated to a locally directed diagram is a colimit.
One usually does not want to use this directly, and instead use the generic `colimit` API.
-/
noncomputable def isColimit : IsColimit (cocone F)
where
desc
s :=
Multicoequalizer.desc _ _ (fun i ↦ s.ι.app ↓i)
(by
rintro ⟨i, j⟩
dsimp [glueData, GlueData.diagram]
simp only [t, IsOpenImmersion.lift_fac]
apply (Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_
simp only [Opens.iSupOpenCover, V, Scheme.homOfLE_ι_assoc]
rw [homOfLE_tAux_assoc F (↓i) (↓j) k.2.1 k.2.2, Iso.eq_inv_comp]
simp)
fac s
j := by
refine (Category.assoc _ _ _).trans ?_
conv_lhs => enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _
simp
uniq s m
hm :=
Multicoequalizer.hom_ext _ _ _ fun i ↦
by
simp [← hm ↓i, cocone, reassoc_of% glueDataι_naturality]
rfl
