Module

PrimeSeparation.lean

Nyll.SchemeTheory.Normalization.PrimeSeparation

9 declarations indexed from sourceView source ↗

Module documentation

Prime separation in a localized normalization

This file formalizes the weak-approximation argument in Fried--Jarden, Lemma 6.3.2(b). Pairwise distinct primes above a fixed maximal ideal are separated by the Chinese remainder theorem. The resulting elements are the source of the lower bound on the dimension of the local normalization quotient.

No finiteness of the normalization is used here. Accordingly, the final bound is first expressed through a linearly independent family (and hence through Module.rank); the finite-dimensional finrank formulation follows once Lemma 6.3.2(a), whose proof uses Lemma 6.3.1, is available.

Imports5

Nyll.SchemeTheory.Normalization.ConductorQuotient
Nyll.SchemeTheory.PlaneCurves.Dimension
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Localization.AtPrime.Basic

Imported by1

Nyll.SchemeTheory.Normalization.All

abbrev

BaseLocalization

L44 ↗

FieldArithmetic.Chapter06.Lemma632.BaseLocalization

Documentation

The localization of the base ring at a prime ideal.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]

Lean source · statement

abbrev BaseLocalization (p : Ideal R) [p.IsPrime]

abbrev

ExtensionLocalization

L51 ↗

FieldArithmetic.Chapter06.Lemma632.ExtensionLocalization

Documentation

The localization of the extension ring using the image of the complement of p. This is the ring denoted S_p in Fried--Jarden, Lemma 6.3.2.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]

Lean source · statement

abbrev ExtensionLocalization (p : Ideal R) [p.IsPrime]

def

extensionPrime

L61 ↗

FieldArithmetic.Chapter06.Lemma632.extensionPrime

Documentation

The ideal of S underlying a chosen prime above p.

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

def extensionPrime (P : Fin (n + 1) ↪ p.primesOver S)
    (j : Fin (n + 1)) : Ideal S

theorem

extensionPrime_isMaximal

L65 ↗

FieldArithmetic.Chapter06.Lemma632.extensionPrime_isMaximal

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

theorem extensionPrime_isMaximal
    (P : Fin (n + 1) ↪ p.primesOver S) (j : Fin (n + 1)) :
    (extensionPrime P j).IsMaximal

theorem

extensionPrimes_pairwise_coprime

L71 ↗

FieldArithmetic.Chapter06.Lemma632.extensionPrimes_pairwise_coprime

Documentation

Distinct primes above a maximal ideal are pairwise coprime.

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

theorem extensionPrimes_pairwise_coprime
    (P : Fin (n + 1) ↪ p.primesOver S) :
    Pairwise (IsCoprime on extensionPrime P)

def

separatingElement

L89 ↗

FieldArithmetic.Chapter06.Lemma632.separatingElement

Documentation

The Chinese-remainder element which is 1 at the i-th chosen prime and 0 at every other chosen prime.

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

def separatingElement
    (P : Fin (n + 1) ↪ p.primesOver S) (i : Fin n) : S

theorem

separatingElement_sub_one_mem

L95 ↗

FieldArithmetic.Chapter06.Lemma632.separatingElement_sub_one_mem

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

theorem separatingElement_sub_one_mem
    (P : Fin (n + 1) ↪ p.primesOver S) (i : Fin n) :
    separatingElement P i - 1 ∈ extensionPrime P i.castSucc

theorem

separatingElement_mem

L104 ↗

FieldArithmetic.Chapter06.Lemma632.separatingElement_mem

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

theorem separatingElement_mem
    (P : Fin (n + 1) ↪ p.primesOver S) (i : Fin n)
    (j : Fin (n + 1)) (hji : j ≠ i.castSucc) :
    separatingElement P i ∈ extensionPrime P j

theorem

separatingElement_mem_last

L114 ↗

FieldArithmetic.Chapter06.Lemma632.separatingElement_mem_last

Documentation

Every separating element vanishes at the last chosen prime.

Source context 14 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace Lemma632
open Function
universe u v w
variable (K : Type u) (R : Type v) (S : Type w)
variable [Field K] [CommRing R] [CommRing S]
variable [Algebra K R] [Algebra R S] [Algebra K S]
variable [IsScalarTower K R S] [Algebra.IsIntegral R S]
section PrimeSeparation
variable {K R S}
variable {p : Ideal R} [p.IsMaximal]
variable {n : ℕ}

Lean source · statement

theorem separatingElement_mem_last
    (P : Fin (n + 1) ↪ p.primesOver S) (i : Fin n) :
    separatingElement P i ∈ extensionPrime P (Fin.last n)

Module documentation

Prime separation in a localized normalization

Declarations