NYLL
Module

Trdeg.lean

Nyll.SchemeTheory.NoetherNormalization.Trdeg
7 declarations indexed from sourceView source ↗

Module documentation

Field Arithmetic, Proposition 6.2.1: Noether normalization

This file connects mathlib's Noether normalization theorem with the transcendence degree of the quotient field. This is the first source-producing step toward the full generator-sensitive statement in Fried--Jarden.

Imports6
  • Nyll.SchemeTheory.NoetherNormalization.GeneratorReduction
  • Mathlib.RingTheory.Algebraic.Integral
  • Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  • Mathlib.RingTheory.AlgebraicIndependent.Transcendental
  • Mathlib.RingTheory.Localization.FractionRing
  • Mathlib.RingTheory.NoetherNormalization
Imported by3

Declarations

theorem

trdeg_fractionRing

L35 ↗
FieldArithmetic.Chapter06.trdeg_fractionRing
Documentation

Passing from a domain to its fraction field does not change transcendence degree.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · statement
theorem trdeg_fractionRing :
    trdeg K (FractionRing A) = trdeg K A
theorem

trdeg_eq_of_injective_isIntegral

L49 ↗
FieldArithmetic.Chapter06.trdeg_eq_of_injective_isIntegral
Documentation

An injective integral map from a polynomial ring has as many variables as the transcendence degree of its target.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · statement
theorem trdeg_eq_of_injective_isIntegral {r : ℕ}
    (g : MvPolynomial (Fin r) K →ₐ[K] A) (hg : Injective g) (hint : g.IsIntegral) :
    trdeg K A = r
theorem

exists_normalization_with_trdeg

L71 ↗
FieldArithmetic.Chapter06.exists_normalization_with_trdeg
Documentation

A Noether normalization whose number of variables is the transcendence degree of the quotient field.

The remaining part of Fried--Jarden Proposition 6.2.1 is the refinement relative to a prescribed finite generating family, including the linear choice over an infinite field.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · full declaration
theorem exists_normalization_with_trdeg [Algebra.FiniteType K A] :
    Exists fun r : ℕ =>
      Exists fun g : MvPolynomial (Fin r) K →ₐ[K] A =>
        Injective g ∧ g.IsIntegral ∧ trdeg K (FractionRing A) = r := by
  obtain ⟨r, g, hg, hint⟩ := exists_integral_inj_algHom_of_fg K A
  refine ⟨r, g, hg, hint, ?_⟩
  rw [trdeg_fractionRing K A]
  exact trdeg_eq_of_injective_isIntegral K A g hg hint
theorem

exists_normalizing_family_with_trdeg

L87 ↗
FieldArithmetic.Chapter06.exists_normalizing_family_with_trdeg
Documentation

Element-family form of Noether normalization over an arbitrary field.

The chosen elements are algebraically independent, their number is the transcendence degree of the quotient field, and the ambient algebra is integral over the subalgebra they generate.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · statement
theorem exists_normalizing_family_with_trdeg [Algebra.FiniteType K A] :
    ∃ r : ℕ, ∃ t : Fin r → A,
      AlgebraicIndependent K t ∧
        Algebra.IsIntegral (Algebra.adjoin K (Set.range t)) A ∧
          trdeg K (FractionRing A) = r
theorem

exists_quotient_normalization_with_trdeg

L121 ↗
FieldArithmetic.Chapter06.exists_quotient_normalization_with_trdeg
Documentation

The quotient presentation form of Noether normalization, retaining the bound on the number of normalizing variables supplied by the given presentation.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · full declaration
theorem exists_quotient_normalization_with_trdeg {n : ℕ}
    (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] :
    Exists fun r : ℕ =>
      r ≤ n ∧
        Exists fun g : MvPolynomial (Fin r) K →ₐ[K] (MvPolynomial (Fin n) K ⧸ I) =>
          Injective g ∧ g.IsIntegral ∧
            trdeg K (FractionRing (MvPolynomial (Fin n) K ⧸ I)) = r := by
  obtain ⟨r, hr, g, hg, hint⟩ :=
    exists_integral_inj_algHom_of_quotient I Ideal.IsPrime.ne_top'
  refine ⟨r, hr, g, hg, hint, ?_⟩
  rw [trdeg_fractionRing K (MvPolynomial (Fin n) K ⧸ I)]
  exact trdeg_eq_of_injective_isIntegral K (MvPolynomial (Fin n) K ⧸ I) g hg hint
theorem

linearNormalization_bridges

L139 ↗
FieldArithmetic.Chapter06.linearNormalization_bridges
Documentation

Bridge from the generator-sensitive induction output to a polynomial normalization map, transcendence degree, and integrality of the ambient algebra.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · statement
theorem linearNormalization_bridges
    {n r : ℕ} (x : Fin n → A) (t : Fin r → A)
    (ht : AlgebraicIndependent K t)
    (hint : ∀ y ∈ Algebra.adjoin K (Set.range x),
      IsIntegral (Algebra.adjoin K (Set.range t)) y)
    (hx : Algebra.adjoin K (Set.range x) = ⊤) :
    ∃ g : MvPolynomial (Fin r) K →ₐ[K]
        Algebra.adjoin K (Set.range t),
      Injective g ∧ Surjective g ∧ g.IsIntegral ∧
        trdeg K (FractionRing A) = r ∧
          Algebra.IsIntegral (Algebra.adjoin K (Set.range t)) A
theorem

exists_linear_normalization_with_trdeg

L205 ↗
FieldArithmetic.Chapter06.exists_linear_normalization_with_trdeg
Documentation

The infinite-field linear form of Noether normalization relative to a prescribed finite generating family.

The normalizing elements are K-linear combinations of the prescribed generators, are algebraically independent, have cardinality equal to the transcendence degree of the quotient field, and make the ambient domain integral over their generated polynomial subalgebra.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function
universe u
variable (K A : Type u)
variable [Field K] [CommRing A] [IsDomain A] [Algebra K A]
Lean source · statement
theorem exists_linear_normalization_with_trdeg
    [Infinite K] {n : ℕ} (x : Fin n → A)
    (hx : Algebra.adjoin K (Set.range x) = ⊤) :
    ∃ r : ℕ, r ≤ n ∧
      ∃ t : Fin r → A,
        (∀ i, t i ∈ Submodule.span K (Set.range x)) ∧
          AlgebraicIndependent K t ∧
            Algebra.IsIntegral (Algebra.adjoin K (Set.range t)) A ∧
              trdeg K (FractionRing A) = r

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