Module

ValuationSubring_isDiscreteValuationRing_of_algebraMap_mem_of_finite.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_isDiscreteValuationRing_of_algebraMap_mem_of_finite

2 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring is Discrete Valuation Ring of algebra Map mem of finite

Imports3

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite

Imported by3

theorem

main

L29 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_algebraMap_mem_of_finite.KrullAkizukiDVR.main

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_algebraMap_mem_of_finite
namespace KrullAkizukiDVR

Lean source · statement

theorem main {A K L : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.KrullDimLE 1 A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [Module.Finite K L]
    (O : ValuationSubring L) (hA : ∀ a : A, algebraMap A L a ∈ O) (hO : O ≠ ⊤) :
    IsDiscreteValuationRing O

theorem

isDiscreteValuationRing_of_algebraMap_mem_of_finite

L81 ↗

ValuationSubring.isDiscreteValuationRing_of_algebraMap_mem_of_finite

Source context 3 commands