English
Compatibility between localization to a stalk and the tilde construction: applying localization to a localized element mk f s yields the germ of the corresponding const section.
Русский
Согласованность локализации к stalk и конструкции tilde: применение локализации к локализованному элементу mk f s даёт germs соответствующей константы.
LaTeX
$$$(localizationToStalk M x).hom (LocalizedModule.mk f s) = (\\tilde{M}).germ (\\mathrm{PrimeSpectrum.basicOpen}(s))\\ x\\ s.2 (\\mathrm{const} M f s (\\mathrm{basicOpen} s) \\cdot)$$$
Lean4
@[simp]
theorem localizationToStalk_mk (x : PrimeSpectrum.Top R) (f : M) (s : x.asIdeal.primeCompl) :
(localizationToStalk M x).hom (LocalizedModule.mk f s) =
(tildeInModuleCat M).germ (PrimeSpectrum.basicOpen (s : R)) x s.2
(const M f s (PrimeSpectrum.basicOpen s) fun _ => id) :=
(Module.End.isUnit_iff _ |>.1 (isUnit_toStalk M x s)).injective <|
by
erw [← Module.End.mul_apply]
simp only [IsUnit.mul_val_inv, Module.End.one_apply, Module.algebraMap_end_apply]
change (M.tildeInModuleCat.germ ⊤ x ⟨⟩) ((toOpen M ⊤) f) = _
rw [← map_smul]
fapply TopCat.Presheaf.germ_ext (W := PrimeSpectrum.basicOpen s.1) (hxW := s.2) (F := M.tildeInModuleCat)
· exact homOfLE le_top
· exact 𝟙 _
refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
added this refine hack to be able to add type hint in `change` -/
refine (?_ : @Eq ?ty _ _)
change LocalizedModule.mk f 1 = (s.1 • LocalizedModule.mk f _ : ?ty)
rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq]
exact ⟨1, by simp⟩
