NYLL
Module

IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes.lean

Nyll.AlgebraicCurves.Valuations.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
6 declarations indexed from sourceView source ↗

Module documentation

Is Integrally Closed is Discrete Valuation Ring of maximal Ideal mem associated Primes

Imports8
  • Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
  • Mathlib.RingTheory.DiscreteValuationRing.TFAE
  • Mathlib.RingTheory.IntegralClosure.Algebra.Basic
  • Mathlib.RingTheory.Localization.Submodule
  • Mathlib.RingTheory.Finiteness.Ideal
  • Mathlib.Tactic.Ring
  • Mathlib.Tactic.Push
  • Mathlib.Tactic.Choose
Imported by2

Declarations

theorem

exists_maximalIdeal_eq_colon_of_eq_radical_colon

L39 ↗
AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes.Ws10Flat.exists_maximalIdeal_eq_colon_of_eq_radical_colon
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat
section Local
variable {B : Type*} [CommRing B]
Lean source · statement
theorem exists_maximalIdeal_eq_colon_of_eq_radical_colon [IsNoetherianRing B] [IsLocalRing B]
    {I : Ideal B} {y : B} (h : maximalIdeal B = (I.colon {y}).radical) :
    ∃ y' : B, maximalIdeal B = I.colon {y'}
theorem

colon_bot_quotient_mk_eq

L68 ↗
AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes.Ws10Flat.colon_bot_quotient_mk_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat
section Local
variable {B : Type*} [CommRing B]
Lean source · statement
theorem colon_bot_quotient_mk_eq (I : Ideal B) (y : B) :
    (⊥ : Submodule B (B ⧸ I)).colon {Ideal.Quotient.mk I y} = I.colon {y}
theorem

isDiscreteValuationRing_of_maximalIdeal_eq_colon

L78 ↗
AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes.Ws10Flat.isDiscreteValuationRing_of_maximalIdeal_eq_colon
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat
section Local
variable {B : Type*} [CommRing B]
variable [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B] [IsLocalRing B]
Lean source · statement
theorem isDiscreteValuationRing_of_maximalIdeal_eq_colon
    {x y : B} (hx : x ≠ 0) (h : maximalIdeal B = (Ideal.span {x}).colon {y}) :
    IsDiscreteValuationRing B
theorem

isDiscreteValuationRing_of_maximalIdeal_eq_radical_colon

L153 ↗
AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes.Ws10Flat.isDiscreteValuationRing_of_maximalIdeal_eq_radical_colon
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat
section Local
variable {B : Type*} [CommRing B]
variable [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B] [IsLocalRing B]
Lean source · statement
theorem isDiscreteValuationRing_of_maximalIdeal_eq_radical_colon
    {x y : B} (hx : x ≠ 0) (h : maximalIdeal B = ((Ideal.span {x}).colon {y}).radical) :
    IsDiscreteValuationRing B
theorem

isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes

L159 ↗
AlgebraicCurves.Valuations.Proofs.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes.Ws10Flat.isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
open IsLocalRing
namespace Ws10Flat
section Local
variable {B : Type*} [CommRing B]
variable [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B] [IsLocalRing B]
Lean source · statement
theorem isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
    {x : B} (hx : x ≠ 0) (h : maximalIdeal B ∈ associatedPrimes B (B ⧸ Ideal.span {x})) :
    IsDiscreteValuationRing B
theorem

isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes

L172 ↗
IsIntegrallyClosed.isDiscreteValuationRing_of_maximalIdeal_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_of_maximalIdeal_mem_associatedPrimes
open IsLocalRing
Lean source · statement
theorem _root_.IsIntegrallyClosed.isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
    {B : Type*} [CommRing B] [IsDomain B] [IsNoetherianRing B] [IsIntegrallyClosed B] [IsLocalRing
      B]
    {x : B} (hx : x ≠ 0)
    (h : IsLocalRing.maximalIdeal B ∈ associatedPrimes B (B ⧸ Ideal.span {x})) :
    IsDiscreteValuationRing B

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.