English
There is a canonical coequalizer in LocallyRingedSpace for any pair of arrows f,g: X ⟶ Y, providing a coequalizer object with the usual universal property.
Русский
Существует канонический коэквализатор в LocallyRingedSpace для пары стрелок f,g: X ⟶ Y, удовлетворяющий универсальному свойству коэквализатора.
LaTeX
$$instance : HasCoequalizer f g$$
Lean4
@[instance]
theorem coequalizer_π_app_isLocalHom (U : TopologicalSpace.Opens (coequalizer f.toShHom g.toShHom).carrier) :
IsLocalHom ((coequalizer.π f.toShHom g.toShHom :).c.app (op U)).hom :=
by
have := ι_comp_coequalizerComparison f.toShHom g.toShHom SheafedSpace.forgetToPresheafedSpace
rw [← PreservesCoequalizer.iso_hom] at this
erw [SheafedSpace.congr_app this.symm (op U)]
rw [PresheafedSpace.comp_c_app, ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10754): this instance has to be manually added
haveI : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace f.toShHom g.toShHom).hom.c :=
inferInstance
have :=
CommRingCat.equalizer_ι_isLocalHom'
(PresheafedSpace.componentwiseDiagram _
((Opens.map
(PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
(Hom.toShHom g)).hom.base).obj
(unop (op U))))
infer_instance
