NYLL
Module

Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
19 declarations indexed from sourceView source ↗

Module documentation

Finite intermediate algebras in a fraction field

An intermediate algebra that is finite in the fraction field satisfies the Krull–Akizuki finiteness and dimension bounds. Length estimates for scalar-multiple quotients and finite lattices provide the supporting module arguments.

Imports14
  • Mathlib.Algebra.Module.Torsion.Basic
  • Mathlib.LinearAlgebra.Dimension.Free
  • Mathlib.RingTheory.Algebraic.Basic
  • Mathlib.RingTheory.DedekindDomain.Basic
  • Mathlib.RingTheory.HopkinsLevitzki
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.RingTheory.Ideal.Quotient.Noetherian
  • Mathlib.RingTheory.KrullDimension.Basic
  • Mathlib.RingTheory.Length
  • Mathlib.RingTheory.Localization.FractionRing
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Lift
  • Mathlib.Tactic.Linarith
  • Mathlib.Tactic.NormNum
Imported by5

Declarations

def

smulRange

L46 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.smulRange
Documentation

The submodule consisting of scalar multiples by the given ring element.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
Lean source · statement
def smulRange {A : Type*} [CommRing A] (a : A) (M : Type*) [AddCommGroup M] [Module A M] :
    Submodule A M
theorem

mem_smulRange_iff

L50 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.mem_smulRange_iff
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
Lean source · statement
theorem mem_smulRange_iff {A : Type*} [CommRing A] {a : A} {M : Type*} [AddCommGroup M] [Module A M]
    (x : M) : x ∈ smulRange a M ↔ ∃ y : M, a • y = x
theorem

smul_mem_smulRange

L54 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.smul_mem_smulRange
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
Lean source · statement
theorem smul_mem_smulRange {A : Type*} [CommRing A] (a : A) {M : Type*} [AddCommGroup M]
    [Module A M]
    (x : M) : a • x ∈ smulRange a M
theorem

le_of_forall_mul_le

L59 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.le_of_forall_mul_le
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
Lean source · statement
theorem le_of_forall_mul_le {x y c : ℕ∞} (hy : y ≠ ⊤) (hc : c ≠ ⊤)
    (h : ∀ k : ℕ, (k : ℕ∞) * x ≤ (k : ℕ∞) * y + c) : x ≤ y
theorem

isArtinianRing_quotient_span_singleton

L85 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.isArtinianRing_quotient_span_singleton
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Domain
variable {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
omit [IsDomain A] in
Lean source · statement
theorem isArtinianRing_quotient_span_singleton {d : A} (hd : d ≠ 0) :
    IsArtinianRing (A ⧸ Ideal.span {d})
theorem

length_ne_top_of_isTorsionBy

L110 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_ne_top_of_isTorsionBy
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Domain
variable {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
omit [IsDomain A] in
Lean source · statement
theorem length_ne_top_of_isTorsionBy {M : Type*} [AddCommGroup M] [Module A M] [Module.Finite A M]
    {d : A} (hd : d ≠ 0) (hM : ∀ m : M, d • m = 0) : Module.length A M ≠ ⊤
theorem

pow_smul_injective

L133 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.pow_smul_injective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Filtration
variable {A : Type*} [CommRing A]
Lean source · statement
theorem pow_smul_injective {M : Type*} [AddCommGroup M] [Module A M] {a : A}
    (hinj : ∀ m : M, a • m = 0 → m = 0) (k : ℕ) (m : M) (h : a ^ k • m = 0) : m = 0
theorem

smulRange_pow_succ_le

L141 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.smulRange_pow_succ_le
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Filtration
variable {A : Type*} [CommRing A]
Lean source · statement
theorem smulRange_pow_succ_le {M : Type*} [AddCommGroup M] [Module A M] (a : A) (k : ℕ) :
    smulRange (a ^ (k + 1)) M ≤ smulRange (a ^ k) M
theorem

length_quot_pow

L147 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_quot_pow
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Filtration
variable {A : Type*} [CommRing A]
Lean source · statement
theorem length_quot_pow {M : Type*} [AddCommGroup M] [Module A M] (a : A)
    (hinj : ∀ m : M, a • m = 0 → m = 0) (k : ℕ) :
    Module.length A (M ⧸ smulRange (a ^ k) M) = k * Module.length A (M ⧸ smulRange a M)
theorem

length_quot_le

L220 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_quot_le
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Filtration
variable {A : Type*} [CommRing A]
Lean source · statement
theorem length_quot_le {M : Type*} [AddCommGroup M] [Module A M] (E : Submodule A M) (b : A) :
    Module.length A (M ⧸ smulRange b M) ≤
      Module.length A (E ⧸ smulRange b E) + Module.length A (M ⧸ E)
theorem

length_quot_smulRange_eq_of_equiv

L258 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_quot_smulRange_eq_of_equiv
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Filtration
variable {A : Type*} [CommRing A]
Lean source · statement
theorem length_quot_smulRange_eq_of_equiv {M N : Type*} [AddCommGroup M] [Module A M]
    [AddCommGroup N] [Module A N]
    (e : M ≃ₗ[A] N) (a : A) :
    Module.length A (M ⧸ smulRange a M) = Module.length A (N ⧸ smulRange a N)
theorem

length_quot_le_of_fg

L277 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_quot_le_of_fg
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Core
variable {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
Lean source · statement
theorem length_quot_le_of_fg {P : Type*} [AddCommGroup P] [Module A P]
    (htf : ∀ a : A, a ≠ 0 → ∀ p : P, a • p = 0 → p = 0)
    (E : Submodule A P) (hEd : ∀ p : P, ∃ d : A, d ≠ 0 ∧ d • p ∈ E)
    {a : A} (ha : a ≠ 0) (M₁ : Submodule A P) (hM₁ : M₁.FG) (hEM₁ : E ≤ M₁) :
    Module.length A (M₁ ⧸ smulRange a M₁) ≤ Module.length A (E ⧸ smulRange a E)
theorem

length_le_of_fg_quot

L339 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_le_of_fg_quot
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Core
variable {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
Lean source · statement
theorem length_le_of_fg_quot {P : Type*} [AddCommGroup P] [Module A P]
    (htf : ∀ a : A, a ≠ 0 → ∀ p : P, a • p = 0 → p = 0)
    (E : Submodule A P) (hE : E.FG) (hEd : ∀ p : P, ∃ d : A, d ≠ 0 ∧ d • p ∈ E)
    {a : A} (ha : a ≠ 0) (N' : Submodule A (P ⧸ smulRange a P)) (hN' : N'.FG) :
    Module.length A N' ≤ Module.length A (E ⧸ smulRange a E)
theorem

length_ne_top_of_forall_fg_le

L381 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.length_ne_top_of_forall_fg_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Core
variable {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
omit [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A] in
Lean source · statement
theorem length_ne_top_of_forall_fg_le {Q : Type*} [AddCommGroup Q] [Module A Q] {y : ℕ∞}
    (hy : y ≠ ⊤)
    (h : ∀ N : Submodule A Q, N.FG → Module.length A N ≤ y) : Module.length A Q ≠ ⊤
theorem

core

L431 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.core
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Core
variable {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
Lean source · statement
theorem core {P : Type*} [AddCommGroup P] [Module A P]
    (htf : ∀ a : A, a ≠ 0 → ∀ p : P, a • p = 0 → p = 0)
    (E : Submodule A P) (hE : E.FG) (hEd : ∀ p : P, ∃ d : A, d ≠ 0 ∧ d • p ∈ E)
    {a : A} (ha : a ≠ 0) :
    Module.length A (P ⧸ smulRange a P) ≠ ⊤
theorem

exists_smul_mem_span

L452 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.exists_smul_mem_span
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Lattice
variable {A K : Type*} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · statement
theorem exists_smul_mem_span {V : Type*} [AddCommGroup V] [Module K V] [Module A V]
    [IsScalarTower A K V]
    (S : Set V) {x : V} (hx : x ∈ Submodule.span K S) :
    ∃ d : A, d ≠ 0 ∧ d • x ∈ Submodule.span A S
theorem

exists_lattice

L478 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.exists_lattice
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Lattice
variable {A K : Type*} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · statement
theorem exists_lattice {V P : Type*} [AddCommGroup V] [Module K V] [Module A V]
    [IsScalarTower A K V]
    [FiniteDimensional K V] [AddCommGroup P] [Module A P]
    (f : P →ₗ[A] V) (hf : Function.Injective f) :
    ∃ E : Submodule A P, E.FG ∧ ∀ p : P, ∃ d : A, d ≠ 0 ∧ d • p ∈ E
theorem

main

L533 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite.KrullAkizukiLa.main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
namespace KrullAkizukiLa
open Module
section Main
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]
    (B : Subalgebra A L) :
    IsNoetherianRing B ∧ Ring.DimensionLEOne B ∧
      ∀ J : Ideal B, J ≠ ⊥ → IsFiniteLength A (B ⧸ J)
theorem

isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite

L637 ↗
Subalgebra.isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
Lean source · statement
theorem _root_.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.DimensionLEOne B ∧
      ∀ J : Ideal B, J ≠ ⊥ → IsFiniteLength A (B ⧸ J)

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