English
The stalk carries a natural algebra structure over the base ring, functorially induced by the structure sheaf and the map of rings.
Русский
Сток имеет естественную алгебраическую структуру над базовым кольцом, универсально индуцированную структурной оболочкой и отображением колец.
LaTeX
$$$\text{Algebra } R \bigl(((\Spec.topMap\cdot).stalk p) \bigr).carrier$$$
Lean4
instance isLocalizedModule_toPushforwardStalkAlgHom :
IsLocalizedModule p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).toLinearMap :=
by
apply IsLocalizedModule.mkOfAlgebra
· intro x hx; rw [algebraMap_pushforward_stalk, toPushforwardStalk_comp]
change
IsUnit
((TopCat.Presheaf.stalkFunctor CommRingCat p).map
(Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).c _)
exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _
· apply isLocalizedModule_toPushforwardStalkAlgHom_aux
· intro x hx
rw [toPushforwardStalkAlgHom_apply, ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
toPushforwardStalk] at hx
rw [CommRingCat.comp_apply, map_zero] at hx
obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq (C := CommRingCat) _ _ _ _ _ _ hx
obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU) U.2
apply_fun (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map (homOfLE hrU).op at e
simp only [map_zero] at e
have : toOpen S (PrimeSpectrum.basicOpen <| algebraMap R S r) x = 0 := by refine Eq.trans ?_ e; rfl
have :=
(@IsLocalization.mk'_one _ _ _ _ _ _ (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans
this
obtain ⟨⟨_, n, rfl⟩, e⟩ := (IsLocalization.mk'_eq_zero_iff _ _).mp this
refine ⟨⟨r, hpr⟩ ^ n, ?_⟩
rw [Submonoid.smul_def, Algebra.smul_def, SubmonoidClass.coe_pow, map_pow]
exact e
