Lean4
/-- The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.
-/
@[simps toShHom]
def locallyRingedSpaceMap {R S : CommRingCat.{u}} (f : R ⟶ S) :
Spec.locallyRingedSpaceObj S ⟶ Spec.locallyRingedSpaceObj R :=
LocallyRingedSpace.Hom.mk (Spec.sheafedSpaceMap f) fun p =>
IsLocalHom.mk fun a ha => by
-- Here, we are showing that the map on prime spectra induced by `f` is really a morphism of
-- *locally* ringed spaces, i.e. that the induced map on the stalks is a local ring
-- homomorphism.
erw [← localRingHom_comp_stalkIso_apply' f p a] at ha
have : IsLocalHom (stalkIso (↑S) p).inv.hom := isLocalHom_of_isIso _
replace ha := (isUnit_map_iff (stalkIso S p).inv.hom _).mp ha
replace ha := IsLocalHom.map_nonunit ((stalkIso R ((PrimeSpectrum.comap f.hom) p)).hom a) ha
convert RingHom.isUnit_map (stalkIso R (PrimeSpectrum.comap f.hom p)).inv.hom ha
rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply]
