English
If M is finitely presented, the rankAtStalk restricted to freeLocus is locally constant.
Русский
Если модуль M конечно представлен, ранг в стаьлоке ограниченного свободного локуса локально константен.
LaTeX
$$$IsLocallyConstant\bigl(\mathrm{rankAtStalk}(M)\bigr) \text{ on } \mathrm{freeLocus}(R,M)$$$
Lean4
theorem isOpen_freeLocus [Module.FinitePresentation R M] : IsOpen (freeLocus R M) :=
by
refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_
have : Module.Free _ _ := hx
obtain ⟨r, hr, hr', _⟩ :=
Module.FinitePresentation.exists_free_localizedModule_powers x.asIdeal.primeCompl
(LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) (Localization.AtPrime x.asIdeal)
exact ⟨basicOpen r, basicOpen_subset_freeLocus_iff.mpr inferInstance, (basicOpen r).2, hr⟩
