Module

IsNoetherianRing_of_ringKrullDim_le_one_of_finiteDimensional_subalgebra.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsNoetherianRing_of_ringKrullDim_le_one_of_finiteDimensional_subalgebra

1 declaration indexed from sourceView source ↗

Module documentation

Noetherian subalgebras of finite fraction-field extensions

Subalgebras of finite-dimensional fraction-field extensions of Noetherian domains of Krull dimension at most one are Noetherian and have Krull dimension at most one.

Imports8

Mathlib.Algebra.Algebra.Subalgebra.Basic
Mathlib.Algebra.Group.Action.Defs
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.RingTheory.DedekindDomain.Basic
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.Noetherian.Defs
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite

Imported by2

theorem

of_ringKrullDim_le_one_of_finiteDimensional_subalgebra

L38 ↗

IsNoetherianRing.of_ringKrullDim_le_one_of_finiteDimensional_subalgebra

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsNoetherianRing_of_ringKrullDim_le_one_of_finiteDimensional_subalgebra
universe u v w

Lean source · statement

theorem _root_.IsNoetherianRing.of_ringKrullDim_le_one_of_finiteDimensional_subalgebra
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] (hR : ringKrullDim R ≤ 1)
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
    (L : Type w) [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L] [FiniteDimensional K L]
    (B : Subalgebra R L) :
    IsNoetherianRing ↥B ∧ ringKrullDim ↥B ≤ 1

Module documentation

Noetherian subalgebras of finite fraction-field extensions

Declarations

of_ringKrullDim_le_one_of_finiteDimensional_subalgebra