English
The free locus over Localization S and LocalizedModule S M coincides with the preimage of the free locus over R M under the natural map.
Русский
Свободный локус после локализации совпадает с предобразом свободного локуса над R через естественное отображение.
LaTeX
$$$\mathrm{freeLocus}(\mathrm{Localization}(S), \mathrm{LocalizedModule}(S,M)) = \mathrm{comap}(\text{algebraMap}_{R}^{\mathrm{Localization}S})^{-1}\big(\mathrm{freeLocus}(R,M)\big)$$$
Lean4
theorem freeLocus_localization (S : Submonoid R) :
freeLocus (Localization S) (LocalizedModule S M) = comap (algebraMap R _) ⁻¹' freeLocus R M :=
by
ext p
simp only [Set.mem_preimage]
let p' := p.asIdeal.comap (algebraMap R _)
have hp' : S ≤ p'.primeCompl := fun x hx H ↦
p.isPrime.ne_top (Ideal.eq_top_of_isUnit_mem _ H (IsLocalization.map_units _ ⟨x, hx⟩))
let Rₚ := Localization.AtPrime p'
let Mₚ := LocalizedModule p'.primeCompl M
letI : Algebra (Localization S) Rₚ := IsLocalization.localizationAlgebraOfSubmonoidLe _ _ S p'.primeCompl hp'
have : IsScalarTower R (Localization S) Rₚ := IsLocalization.localization_isScalarTower_of_submonoid_le ..
have : IsLocalization.AtPrime Rₚ p.asIdeal :=
by
have := IsLocalization.isLocalization_of_submonoid_le (Localization S) Rₚ _ _ hp'
apply
IsLocalization.isLocalization_of_is_exists_mul_mem _ (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl)
· rintro _ ⟨x, hx, rfl⟩; exact hx
· rintro ⟨x, hx⟩
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective S x
refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
rw [IsLocalization.mk'_eq_mul_mk'_one]
exact Ideal.mul_mem_right _ _ H
letI : Module (Localization S) Mₚ := Module.compHom Mₚ (algebraMap _ Rₚ)
have : IsScalarTower R (Localization S) Mₚ :=
⟨fun r r' m ↦
show algebraMap _ Rₚ (r • r') • m = _ by
simp [p', Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; rfl⟩
have : IsScalarTower (Localization S) Rₚ Mₚ :=
⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩
let l :=
(IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
(LocalizedModule.mkLinearMap p'.primeCompl M)).extendScalarsOfIsLocalization
S (Localization S)
have : IsLocalizedModule p.asIdeal.primeCompl l :=
by
have : IsLocalizedModule p'.primeCompl (l.restrictScalars R) :=
inferInstanceAs
(IsLocalizedModule p'.primeCompl
(IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
(LocalizedModule.mkLinearMap p'.primeCompl M)))
have : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l :=
IsLocalizedModule.of_restrictScalars p'.primeCompl ..
apply IsLocalizedModule.of_exists_mul_mem (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl)
· rintro _ ⟨x, hx, rfl⟩; exact hx
· rintro ⟨x, hx⟩
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective S x
refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
rw [IsLocalization.mk'_eq_mul_mk'_one]
exact Ideal.mul_mem_right _ _ H
rw [mem_freeLocus_of_isLocalization (R := Localization S) p Rₚ Mₚ l]
rfl
