Krull–Akizuki theorem

TheoremKrull–Akizuki theorem#✓fully proved

The Krull–Akizuki theorem: a subalgebra of a finite extension of the fraction field of a Noetherian domain of Krull dimension at most one is Noetherian of Krull dimension at most one, and every nonzero quotient has finite length over the base.

theorem Subalgebra.isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
    {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]
    (B : Subalgebra A L) :
    IsNoetherianRing B ∧ Ring.KrullDimLE 1 B ∧
      ∀ J : Ideal B, J ≠ ⊥ → IsFiniteLength A (B ⧸ J)

Used by 1

Used byValuation subrings of finite extensions of dimension-one domains are DVRs

TheoremValuation subrings of finite extensions of dimension-one domains are DVRs#✓fully proved

A valuation subring of a finite extension of the fraction field of a Noetherian domain of Krull dimension at most one, containing the base ring and different from the whole field, is a discrete valuation ring.

theorem ValuationSubring.isDiscreteValuationRing_of_algebraMap_mem_of_finite
    {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

Uses 1

Proof usesKrull–Akizuki theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.