English
If f = g for morphisms in LocallyRingedSpace, then the corresponding stalk maps are pointwise congruent in the LocalHom sense.
Русский
Если f = g для морфизмов в LocallyRingedSpace, то соответствующие stalk maps совпадают на уровне локальных гомоморфизмов.
LaTeX
$$isLocalHom_stalkMap_congr {X Y} (f g) (H: f=g) (x) (h: IsLocalHom (f.stalkMap x).hom) : IsLocalHom (g.stalkMap x).hom$$
Lean4
/-- The cofork constructed in `coequalizerCofork` is indeed a colimit cocone. -/
noncomputable def coequalizerCoforkIsColimit : IsColimit (coequalizerCofork f g) :=
by
apply Cofork.IsColimit.mk'
intro s
have e : f.toShHom ≫ s.π.toShHom = g.toShHom ≫ s.π.toShHom := by injection s.condition
refine ⟨⟨coequalizer.desc s.π.toShHom e, ?_⟩, ?_⟩
· intro x
rcases (TopCat.epi_iff_surjective (coequalizer.π f.toShHom g.toShHom).base).mp inferInstance x with
⟨y, rfl⟩
-- Porting note: was `apply isLocalHom_of_comp _ (PresheafedSpace.stalkMap ...)`, this
-- used to allow you to provide the proof that `... ≫ ...` is a local ring homomorphism later,
-- but this is no longer possible
set h := _
change IsLocalHom h
suffices _ : IsLocalHom (((coequalizerCofork f g).π.1.stalkMap _).hom.comp h) by
apply isLocalHom_of_comp _ ((coequalizerCofork f g).π.1.stalkMap _).hom
rw [← CommRingCat.hom_ofHom h, ← CommRingCat.hom_comp]
erw [← PresheafedSpace.stalkMap.comp]
apply isLocalHom_stalkMap_congr _ _ (coequalizer.π_desc s.π.toShHom e).symm y
infer_instance
constructor
· exact LocallyRingedSpace.Hom.ext' (coequalizer.π_desc _ _)
intro m h
replace h : (coequalizerCofork f g).π.toShHom ≫ m.1 = s.π.toShHom := by rw [← h]; rfl
apply LocallyRingedSpace.Hom.ext'
apply (colimit.isColimit (parallelPair f.toShHom g.toShHom)).uniq (Cofork.ofπ s.π.toShHom e) m.1
rintro ⟨⟩
· rw [← (colimit.cocone (parallelPair f.toShHom g.toShHom)).w WalkingParallelPairHom.left, Category.assoc]
change _ ≫ _ ≫ _ = _ ≫ _
congr
· exact h
