Module

Module_exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one

1 declaration indexed from sourceView source ↗

Module documentation

Module exists not Mem and free localized Module of is Integrally Closed of ring Krull Dim

le one

Imports5

Mathlib.Algebra.NoZeroSMulDivisors.Defs
Mathlib.LinearAlgebra.FreeModule.PID
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Localization.Free
Mathlib.RingTheory.Localization.Submodule

Imported by2

theorem

exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one

L31 ↗

Module.exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace Module
universe u

Lean source · statement

theorem
  _root_.Module.exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] (𝔭 : Ideal A) [𝔭.IsPrime]
    (h𝔭ic : IsIntegrallyClosed (Localization.AtPrime 𝔭)) (h𝔭dim : ringKrullDim
      (Localization.AtPrime 𝔭) ≤ 1)
    (B : Type u) [AddCommGroup B] [Module A B] [Module.Finite A B] [NoZeroSMulDivisors A B] :
    ∃ f : A, f ∉ 𝔭 ∧ Module.Free (Localization.Away f) (LocalizedModule (Submonoid.powers f) B)

Module documentation

Module exists not Mem and free localized Module of is Integrally Closed of ring Krull Dim

Declarations

exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one