English
Further specialization: rankAtStalk is locally constant on freeLocus given FP and flatness; stability under base change persists.
Русский
Уточнение: rankAtStalk локально константен на freeLocus при FP и плоскостности; сохранение базового изменения сохраняется.
LaTeX
$$$IsLocallyConstant(\mathrm{rankAtStalk}(M))$ на $\mathrm{freeLocus}(R,M)$ under FP and flatness$$
Lean4
theorem isLocallyConstant_rankAtStalk_freeLocus [Module.FinitePresentation R M] :
IsLocallyConstant (fun x : freeLocus R M ↦ rankAtStalk M x.1) :=
by
refine (IsLocallyConstant.iff_exists_open _).mpr fun ⟨x, hx⟩ ↦ ?_
have : Module.Free _ _ := hx
obtain ⟨f, hf, hf', hf''⟩ :=
Module.FinitePresentation.exists_free_localizedModule_powers x.asIdeal.primeCompl
(LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) (Localization.AtPrime x.asIdeal)
refine ⟨Subtype.val ⁻¹' basicOpen f, (basicOpen f).2.preimage continuous_subtype_val, hf, ?_⟩
rintro ⟨p, hp''⟩ hp
let p' := Algebra.algebraMapSubmonoid (Localization (.powers f)) p.asIdeal.primeCompl
have hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl := by simpa [Submonoid.powers_le, Ideal.primeCompl]
let Rₚ := Localization.AtPrime p.asIdeal
let Mₚ := LocalizedModule p.asIdeal.primeCompl M
letI : Algebra (Localization.Away f) Rₚ :=
IsLocalization.localizationAlgebraOfSubmonoidLe _ _ (.powers f) p.asIdeal.primeCompl hp'
have : IsScalarTower R (Localization.Away f) Rₚ := IsLocalization.localization_isScalarTower_of_submonoid_le ..
letI : Module (Localization.Away f) Mₚ := Module.compHom Mₚ (algebraMap _ Rₚ)
have : IsScalarTower R (Localization.Away f) Mₚ :=
⟨fun r r' m ↦
show algebraMap _ Rₚ (r • r') • m = _ by
simp [Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; rfl⟩
have : IsScalarTower (Localization.Away f) 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 (.powers f) M)
(LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)).extendScalarsOfIsLocalization
(.powers f) (Localization.Away f)
have : IsLocalization p' Rₚ := IsLocalization.isLocalization_of_submonoid_le (Localization.Away f) Rₚ _ _ hp'
have : IsLocalizedModule p.asIdeal.primeCompl (l.restrictScalars R) :=
inferInstanceAs
(IsLocalizedModule p.asIdeal.primeCompl
((IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap (.powers f) M)
(LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))))
have : IsLocalizedModule (Algebra.algebraMapSubmonoid _ p.asIdeal.primeCompl) l :=
IsLocalizedModule.of_restrictScalars p.asIdeal.primeCompl ..
have := Module.finrank_of_isLocalizedModule_of_free Rₚ p' l
simp [Rₚ, rankAtStalk, this, hf'']
