isRegular_of_isLocalizedModule_of_mem

English

If rs is a weakly regular R-sequence, then after localization at p, the image sequence is weakly regular in the localized ring.

Русский

После локализации в p образ последовательности остается слабой регулярной.

LaTeX

$$$\text{IsWeaklyRegular}_S( rs.map( algebraMap_R^S) ).$$$

Lean4

theorem isRegular_of_isLocalizedModule_of_mem [Nontrivial N] [Module.Finite S N] (f : M →ₗ[R] N)
    [IsLocalizedModule.AtPrime p f] {rs : List R} (reg : IsWeaklyRegular M rs) (mem : ∀ r ∈ rs, r ∈ p) :
    IsRegular N (rs.map (algebraMap R S)) :=
  by
  have : IsLocalRing S := IsLocalization.AtPrime.isLocalRing S p
  refine
    (IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal (fun _ hr ↦ ?_)).mpr <|
      reg.of_isLocalizedModule S p.primeCompl f
  rcases List.mem_map.mp hr with ⟨r, hr, eq⟩
  simpa only [← eq, IsLocalization.AtPrime.to_map_mem_maximal_iff S p] using mem r hr

Похожие утверждения