Module

Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime.lean

Nyll.AlgebraicCurves.Valuations.Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime

3 declarations indexed from sourceView source ↗

Module documentation

Algebra IsStandardSmoothOfRelativeDimension isDiscreteValuationRing localization atPrime

Localizing a standard smooth algebra of relative dimension one at the specified prime produces a discrete valuation ring.

Imports6

Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.Unramified.LocalRing
Mathlib.Tactic.ByContra
Mathlib.Tactic.Push
Mathlib.Tactic.Ring.RingNF

Imported by5

theorem

isDomain_of_maximalIdeal_eq_span

L45 ↗

AlgebraicCurves.Valuations.Proofs.Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime.Algebra.IsStandardSmoothOfRelativeDimension.isDomain_of_maximalIdeal_eq_span

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime
universe u v
open IsLocalRing
attribute [local instance] Ideal.Quotient.field
namespace Algebra
open _root_.Algebra
namespace IsStandardSmoothOfRelativeDimension
open _root_.Algebra.IsStandardSmoothOfRelativeDimension
open _root_.Algebra.IsStandardSmoothOfRelativeDimension
open _root_.Algebra

Lean source · statement

theorem isDomain_of_maximalIdeal_eq_span {L : Type*} [CommRing L] [IsLocalRing L]
    [IsNoetherianRing L] {ϖ : L} (hreg : IsSMulRegular L ϖ)
    (hmax : maximalIdeal L = Ideal.span {ϖ}) : IsDomain L

theorem

atom_main

L89 ↗

AlgebraicCurves.Valuations.Proofs.Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime.Algebra.IsStandardSmoothOfRelativeDimension.atom_main

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime
universe u v
open IsLocalRing
attribute [local instance] Ideal.Quotient.field
namespace Algebra
open _root_.Algebra
namespace IsStandardSmoothOfRelativeDimension
open _root_.Algebra.IsStandardSmoothOfRelativeDimension
open _root_.Algebra.IsStandardSmoothOfRelativeDimension
open _root_.Algebra

Lean source · statement

theorem atom_main
    {k : Type u} [Field k] {A : Type v} [CommRing A] [Algebra k A]
    [Algebra.IsStandardSmoothOfRelativeDimension 1 k A]
    (p : Ideal A) [p.IsMaximal] :
    ∃ _ : IsDomain (Localization.AtPrime p), IsDiscreteValuationRing (Localization.AtPrime p)

theorem

isDiscreteValuationRing_localization_atPrime

L150 ↗

Algebra.IsStandardSmoothOfRelativeDimension.isDiscreteValuationRing_localization_atPrime

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime
universe u v
open IsLocalRing
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem
  _root_.Algebra.IsStandardSmoothOfRelativeDimension.isDiscreteValuationRing_localization_atPrime
    {k : Type u} [Field k] {A : Type v} [CommRing A] [Algebra k A]
    [Algebra.IsStandardSmoothOfRelativeDimension 1 k A]
    (p : Ideal A) [p.IsMaximal] :
    ∃ _ : IsDomain (Localization.AtPrime p), IsDiscreteValuationRing (Localization.AtPrime p)

Module documentation

Algebra IsStandardSmoothOfRelativeDimension isDiscreteValuationRing localization atPrime

Declarations

isDomain_of_maximalIdeal_eq_span

atom_main

isDiscreteValuationRing_localization_atPrime