NYLL
Module

ConductorQuotient.lean

Nyll.SchemeTheory.Normalization.ConductorQuotient
28 declarations indexed from sourceView source ↗

Module documentation

The normalization quotient of an affine curve

Fried--Jarden, Lemma 6.3.1 states that, for an affine integral curve R = K[x, y] with function field F and normalization S in F, the quotient S / R is finite-dimensional over K.

This file develops the conductor and finite-dimensional quotient argument used in the proof. The general theorem that normalization of a one-dimensional affine algebra over an arbitrary field is module-finite is kept as the next source-producing frontier; mathlib's current integral-closure finiteness theorem assumes a finite separable extension.

Imports6
  • Mathlib.RingTheory.AdjoinRoot
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.RingTheory.QuotSMulTop
  • Mathlib.RingTheory.TensorProduct.Finite
Imported by2

Declarations

abbrev

Normalization

L44 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.Normalization
Documentation

The normalization of R in its chosen fraction field F.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
abbrev Normalization
def

baseSubmoduleR

L47 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.baseSubmoduleR
Documentation

The copy of R inside its normalization, as an R-submodule.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def baseSubmoduleR : Submodule R (Normalization R F)
def

baseSubmodule

L51 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.baseSubmodule
Documentation

The copy of R inside its normalization, as a K-subspace.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def baseSubmodule : Submodule K (Normalization R F)
theorem

mem_baseSubmodule_iff

L55 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.mem_baseSubmodule_iff
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] [IsFractionRing R F] in
Lean source · statement
theorem mem_baseSubmodule_iff (s : Normalization R F) :
    s ∈ baseSubmodule K R F ↔
      ∃ r : R, algebraMap R (Normalization R F) r = s
abbrev

Quotient

L61 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.Quotient
Documentation

The quotient of the normalization by the original affine ring.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
abbrev Quotient
def

denominatorSubmodule

L68 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.denominatorSubmodule
Documentation

Elements of the normalization which a fixed element z : R sends back into R.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def denominatorSubmodule (z : R) :
    Submodule R (Normalization R F)
theorem

mem_denominatorSubmodule_iff

L75 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.mem_denominatorSubmodule_iff
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] [IsFractionRing R F] in
Lean source · statement
theorem mem_denominatorSubmodule_iff (z : R) (s : Normalization R F) :
    s ∈ denominatorSubmodule R F z ↔
      algebraMap R (Normalization R F) z * s ∈ baseSubmoduleR R F
theorem

exists_nonzero_commonDenominator

L85 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.exists_nonzero_commonDenominator
Documentation

A finite R-module contained in the fraction field admits a single nonzero common denominator. Applied to the normalization, this is the conductor element z in the proof of Fried--Jarden, Lemma 6.3.1.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
theorem exists_nonzero_commonDenominator
    [Module.Finite R (Normalization R F)] :
    ∃ z : R, z ≠ 0 ∧ denominatorSubmodule R F z = ⊤
theorem

algebraMap_normalization_injective

L133 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.algebraMap_normalization_injective
Documentation

The original domain embeds into its normalization.

Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] in
Lean source · statement
theorem algebraMap_normalization_injective :
    Function.Injective (algebraMap R (Normalization R F))
def

baseEmbeddingEquiv

L140 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.baseEmbeddingEquiv
Documentation

The algebra map identifies R with its image in the normalization.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def baseEmbeddingEquiv :
    R ≃ₗ[R] baseSubmoduleR R F
def

commonDenominatorMap

L154 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.commonDenominatorMap
Documentation

Multiplication by a common denominator, with codomain restricted back to R.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def commonDenominatorMap (z : R)
    (hz : denominatorSubmodule R F z = ⊤) :
    Normalization R F →ₗ[R] R
theorem

algebraMap_commonDenominatorMap

L166 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.algebraMap_commonDenominatorMap
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] in
Lean source · statement
theorem algebraMap_commonDenominatorMap
    (z : R) (hz : denominatorSubmodule R F z = ⊤)
    (s : Normalization R F) :
    algebraMap R (Normalization R F) (commonDenominatorMap R F z hz s) =
      algebraMap R (Normalization R F) z * s
theorem

commonDenominatorMap_algebraMap

L180 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.commonDenominatorMap_algebraMap
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] in
Lean source · statement
theorem commonDenominatorMap_algebraMap
    (z r : R) (hz : denominatorSubmodule R F z = ⊤) :
    commonDenominatorMap R F z hz
        (algebraMap R (Normalization R F) r) = z * r
theorem

commonDenominatorMap_injective

L188 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.commonDenominatorMap_injective
Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
theorem commonDenominatorMap_injective
    {z : R} (hz0 : z ≠ 0)
    (hz : denominatorSubmodule R F z = ⊤) :
    Function.Injective (commonDenominatorMap R F z hz)
def

commonDenominatorMapK

L208 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.commonDenominatorMapK
Documentation

The common-denominator map, viewed over the constant field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def commonDenominatorMapK (z : R)
    (hz : denominatorSubmodule R F z = ⊤) :
    Normalization R F →ₗ[K] R
theorem

commonDenominatorMapK_apply

L215 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.commonDenominatorMapK_apply
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] in
Lean source · statement
theorem commonDenominatorMapK_apply
    (z : R) (hz : denominatorSubmodule R F z = ⊤)
    (s : Normalization R F) :
    commonDenominatorMapK K R F z hz s =
      commonDenominatorMap R F z hz s
def

principalSubmodule

L223 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.principalSubmodule
Documentation

The principal K-subspace zR of R.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def principalSubmodule (z : R) : Submodule K R
theorem

mem_principalSubmodule_iff

L228 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.mem_principalSubmodule_iff
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] [Algebra R F] [IsScalarTower K R F]
  [IsFractionRing R F] in
Lean source · statement
theorem mem_principalSubmodule_iff (z r : R) :
    r ∈ principalSubmodule K R z ↔ ∃ a : R, z * a = r
abbrev

PrincipalQuotient

L235 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.PrincipalQuotient
Documentation

The vector-space quotient R / zR.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
abbrev PrincipalQuotient (z : R)
theorem

commonDenominatorMap_maps_base

L240 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.commonDenominatorMap_maps_base
Documentation

Multiplication by the conductor sends the embedded copy of R into zR.

Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] in
Lean source · statement
theorem commonDenominatorMap_maps_base
    (z : R) (hz : denominatorSubmodule R F z = ⊤) :
    baseSubmodule K R F ≤
      (principalSubmodule K R z).comap
        (commonDenominatorMapK K R F z hz)
def

quotientToPrincipal

L268 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.quotientToPrincipal
Documentation

The injection S/R → R/zR from the proof of Fried--Jarden, Lemma 6.3.1. It sends the class of s to the class of zs.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
def quotientToPrincipal (z : R)
    (hz : denominatorSubmodule R F z = ⊤) :
    Quotient K R F →ₗ[K] PrincipalQuotient K R z
theorem

quotientToPrincipal_mk

L279 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.quotientToPrincipal_mk
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
omit [IsDomain R] in
Lean source · statement
theorem quotientToPrincipal_mk
    (z : R) (hz : denominatorSubmodule R F z = ⊤)
    (s : Normalization R F) :
    quotientToPrincipal K R F z hz
        (Submodule.Quotient.mk s) =
      Submodule.Quotient.mk (commonDenominatorMap R F z hz s)
theorem

quotientToPrincipal_injective

L287 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.quotientToPrincipal_injective
Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
Lean source · statement
theorem quotientToPrincipal_injective
    {z : R} (hz0 : z ≠ 0)
    (hz : denominatorSubmodule R F z = ⊤) :
    Function.Injective (quotientToPrincipal K R F z hz)
theorem

exists_nonzero_polynomial_multiple

L336 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.exists_nonzero_polynomial_multiple
Documentation

In an integral domain integral over K[X], every nonzero principal ideal contains a nonzero polynomial from K[X].

This is the source of the polynomial g(x) ∈ zR in the proof of Fried--Jarden, Lemma 6.3.1.

Source context 15 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
section PolynomialNormalization
variable [Algebra (Polynomial K) R]
variable [IsScalarTower K (Polynomial K) R]
variable [Algebra.IsIntegral (Polynomial K) R]
omit [Algebra K R] [IsScalarTower K (Polynomial K) R] in
Lean source · statement
theorem exists_nonzero_polynomial_multiple
    (z : R) (hz : z ≠ 0) :
    ∃ g : Polynomial K, g ≠ 0 ∧
      ∃ r : R, algebraMap (Polynomial K) R g = z * r
theorem

exists_monic_polynomial_multiple

L362 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.exists_monic_polynomial_multiple
Documentation

The polynomial in a nonzero principal ideal may be chosen monic.

Source context 15 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
section PolynomialNormalization
variable [Algebra (Polynomial K) R]
variable [IsScalarTower K (Polynomial K) R]
variable [Algebra.IsIntegral (Polynomial K) R]
omit [Algebra K R] [IsScalarTower K (Polynomial K) R] in
Lean source · statement
theorem exists_monic_polynomial_multiple
    (z : R) (hz : z ≠ 0) :
    ∃ q : Polynomial K, q.Monic ∧
      ∃ r : R, algebraMap (Polynomial K) R q = z * r
theorem

quotSMulTop_finite_of_monic

L379 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.quotSMulTop_finite_of_monic
Documentation

Reduction modulo a monic polynomial of K[X] makes every finite K[X]-module finite-dimensional over K.

Source context 15 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
section PolynomialNormalization
variable [Algebra (Polynomial K) R]
variable [IsScalarTower K (Polynomial K) R]
variable [Algebra.IsIntegral (Polynomial K) R]
omit [IsDomain R] [Algebra.IsIntegral (Polynomial K) R] in
Lean source · statement
theorem quotSMulTop_finite_of_monic
    [Module.Finite (Polynomial K) R]
    (q : Polynomial K) (hq : q.Monic) :
    Module.Finite K (QuotSMulTop q R)
theorem

principalQuotient_finite

L399 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.principalQuotient_finite
Documentation

For a finite integral K[X]-domain, quotienting by a nonzero element is finite-dimensional over K.

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
section PolynomialNormalization
variable [Algebra (Polynomial K) R]
variable [IsScalarTower K (Polynomial K) R]
variable [Algebra.IsIntegral (Polynomial K) R]
Lean source · statement
theorem principalQuotient_finite
    [Module.Finite (Polynomial K) R]
    (z : R) (hz : z ≠ 0) :
    Module.Finite K (PrincipalQuotient K R z)
theorem

normalizationQuotient_finite_of_normalization_finite

L465 ↗
FieldArithmetic.Chapter06.NormalizationQuotient.normalizationQuotient_finite_of_normalization_finite
Documentation

The complete conductor argument of Fried--Jarden, Lemma 6.3.1, from module-finiteness of the normalization.

The separate normalization-finiteness input is exactly the classical theorem cited in the first sentence of the printed proof.

Source context 15 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace NormalizationQuotient
open scoped nonZeroDivisors Pointwise TensorProduct
universe u v w
variable (K : Type u) (R : Type v) (F : Type w)
variable [Field K] [CommRing R] [IsDomain R] [Field F]
variable [Algebra K R] [Algebra R F] [Algebra K F]
variable [IsScalarTower K R F] [IsFractionRing R F]
section FiniteNormalization
variable [Algebra (Polynomial K) R]
variable [IsScalarTower K (Polynomial K) R]
variable [Module.Finite (Polynomial K) R]
variable [Module.Finite R (Normalization R F)]
Lean source · statement
theorem normalizationQuotient_finite_of_normalization_finite :
    Module.Finite K (Quotient K R F)

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