English
For each open U, the stalk map induced by the cospan projection in the coequalizer is a local homomorphism.
Русский
Для каждого открытого U индуцированное вдоль проекции коэквализатора отображение на стэках является локальным гомоморфизмом.
LaTeX
$$IsLocalHom ((coequalizer.π f.toShHom g.toShHom :).c.app (op U)).hom$$
Lean4
/-- The explicit coproduct for `F : discrete ι ⥤ LocallyRingedSpace`. -/
noncomputable def coproduct : LocallyRingedSpace
where
toSheafedSpace := colimit (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (F ⋙ forgetToSheafedSpace)
isLocalRing
x := by
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
haveI : IsLocalRing (((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) := (F.obj i).isLocalRing _
exact
(asIso
((colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (F ⋙ forgetToSheafedSpace) i :).stalkMap
y)).symm.commRingCatIsoToRingEquiv.isLocalRing
