English
The pushforward stalk homomorphism is localized at p, i.e. becomes a localized map of modules over the base ring.
Русский
Гомоморфизм пушфорвардного стока локализуется в точке p, становится локализованной гомоморфизмом модулей над базовым кольцом.
LaTeX
$$$\text{IsLocalizedModule} \, p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).$$$
Lean4
theorem isLocalizedModule_toPushforwardStalkAlgHom_aux (y) :
∃ x : S × p.asIdeal.primeCompl, x.2 • y = toPushforwardStalkAlgHom R S p x.1 :=
by
obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.germ_exist _ _ y
obtain ⟨_, ⟨r, rfl⟩, hpr : p ∈ PrimeSpectrum.basicOpen r, hrU : PrimeSpectrum.basicOpen r ≤ U⟩ :=
PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U from hp) U.2
change PrimeSpectrum.basicOpen r ≤ U at hrU
replace e :=
((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply (homOfLE hrU) p hpr
_).trans
e
set s' := (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map (homOfLE hrU).op s with h
replace e : ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).val).germ _ p hpr) s' = y := by
rw [h]; exact e
clear_value s'; clear! U
obtain ⟨⟨s, ⟨_, n, rfl⟩⟩, hsn⟩ :=
@IsLocalization.surj _ _ _ _ _ _ (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) s'
refine ⟨⟨s, ⟨r, hpr⟩ ^ n⟩, ?_⟩
rw [Submonoid.smul_def, Algebra.smul_def, algebraMap_pushforward_stalk, toPushforwardStalk, CommRingCat.comp_apply,
CommRingCat.comp_apply]
iterate 2
erw [←
(Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply (homOfLE le_top) p hpr]
rw [← e]
let f := TopCat.Presheaf.germ (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).val) _ p hpr
rw [← map_mul, mul_comm]
dsimp only [Subtype.coe_mk] at hsn
rw [← map_pow (algebraMap R S)] at hsn
congr 1
