Module

IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes.lean

Nyll.AlgebraicCurves.Valuations.IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes

3 declarations indexed from sourceView source ↗

Module documentation

Is Integrally Closed is Discrete Valuation Ring localization of mem associated Primes

Imports1

Nyll.AlgebraicCurves.Valuations.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes

Imported by2

theorem

colon_bot_quotient_mk_eq

L28 ↗

AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes.Ws10Flat.colon_bot_quotient_mk_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat

Lean source · statement

theorem colon_bot_quotient_mk_eq {B : Type*} [CommRing B] (I : Ideal B) (y : B) :
    (⊥ : Submodule B (B ⧸ I)).colon {Ideal.Quotient.mk I y} = I.colon {y}

theorem

isDiscreteValuationRing_localization_of_mem_associatedPrimes

L40 ↗

AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes.Ws10Flat.isDiscreteValuationRing_localization_of_mem_associatedPrimes

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat
section Global
variable {B : Type*} [CommRing B] [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B]

Lean source · statement

theorem isDiscreteValuationRing_localization_of_mem_associatedPrimes
    {x : B} (hx : x ≠ 0) (P : Ideal B) [P.IsPrime]
    (hP : P ∈ associatedPrimes B (B ⧸ Ideal.span {x})) :
    IsDiscreteValuationRing (Localization.AtPrime P)

theorem

isDiscreteValuationRing_localization_of_mem_associatedPrimes

L100 ↗

IsIntegrallyClosed.isDiscreteValuationRing_localization_of_mem_associatedPrimes

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes
open IsLocalRing

Lean source · statement

theorem _root_.IsIntegrallyClosed.isDiscreteValuationRing_localization_of_mem_associatedPrimes
    {B : Type*} [CommRing B] [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B]
    {x : B} (hx : x ≠ 0) (P : Ideal B) [P.IsPrime]
    (hP : P ∈ associatedPrimes B (B ⧸ Ideal.span {x})) :
    IsDiscreteValuationRing (Localization.AtPrime P)

Module documentation

Is Integrally Closed is Discrete Valuation Ring localization of mem associated Primes

Declarations

colon_bot_quotient_mk_eq

isDiscreteValuationRing_localization_of_mem_associatedPrimes

isDiscreteValuationRing_localization_of_mem_associatedPrimes