Lean4
/-- (Implementation detail)
The cocone associated to a locally directed diagram is a colimit as locally ringed spaces.
One usually does not want to use this directly, and instead use the generic `colimit` API.
-/
noncomputable def isColimitForgetToLocallyRingedSpace :
IsColimit (Scheme.forgetToLocallyRingedSpace.mapCocone (cocone F))
where
desc
s :=
(glueData F).isoLocallyRingedSpace.hom ≫
Multicoequalizer.desc _ _ (fun i ↦ s.ι.app ↓i)
(by
rintro ⟨i, j⟩
dsimp [glueData, GlueData.diagram]
simp only [t, IsOpenImmersion.lift_fac, ← Scheme.comp_toLRSHom]
rw [← cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.fromGlued.toLRSHom, ←
cancel_epi (Scheme.Opens.iSupOpenCover _).ulift.gluedCover.isoLocallyRingedSpace.inv]
refine Multicoequalizer.hom_ext _ _ _ fun ⟨k, hk⟩ ↦ ?_
rw [← CategoryTheory.GlueData.ι, reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv, ← cancel_epi (Hom.isoOpensRange (F.map _)).hom.toLRSHom]
simp only [Opens.iSupOpenCover, Cover.ulift, V, ← comp_toLRSHom_assoc, Cover.ι_fromGlued_assoc, homOfLE_ι,
Hom.isoOpensRange_hom_ι]
generalize_proofs _ _ h
rw [homOfLE_tAux F (↓i) (↓j) h.choose.2.1 h.choose.2.2, Iso.hom_inv_id_assoc]
exact (s.w h.choose.2.1).trans (s.w h.choose.2.2).symm)
fac s
j :=
by
simp only [cocone, Functor.mapCocone_ι_app, Scheme.comp_toLRSHom, forgetToLocallyRingedSpace_map,
← GlueData.ι_isoLocallyRingedSpace_inv]
simpa [CategoryTheory.GlueData.ι] using s.w _
uniq s m
hm := by
rw [← Iso.inv_comp_eq]
refine Multicoequalizer.hom_ext _ _ _ fun i ↦ ?_
conv_lhs => rw [← ι.eq_def]
dsimp
simp [cocone, ← hm, glueDataι_naturality, ← GlueData.ι_isoLocallyRingedSpace_inv, -ι_gluedIso_inv_assoc,
-ι_gluedIso_inv]
