NYLL
Module

ExactNormalizationPrimeChain.lean

Nyll.EtaleFundamentalGroups.Completions.Retained.ExactNormalizationPrimeChain
10 declarations indexed from sourceView source ↗

Module documentation

An exact retained branch in one completed normalization component

Let q ≤ p be a height-one/closed prime chain in a finite flat domain over a two-dimensional regular local ring. If q lies over a prime regular parameter and has a prescribed ramification index, maximal-adic completion retains that exact index at the same right-contraction prime of the literal tensor square.

The generic prime below that tensor prime fixes one literal component of the completed generic fibre. Integral going-up then carries the retained height-one/closed chain into the normalization of that same component. The normalization prime is deliberately not declared to have the same index: that final equality additionally needs normality of the localized tensor factor (equivalently, vertical ramification index one).

Imports11
Imported by1

Declarations

abbrev

MaximalAdicFiniteBaseChange

L48 ↗
EtaleFundamentalGroups.MaximalAdicFiniteBaseChange
Documentation

The completed finite base change used by a retained branch.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
abbrev MaximalAdicFiniteBaseChange
    (R : Type uR) (S : Type uS)
    [CommRing R] [IsLocalRing R] [CommRing S] [Algebra R S]
def

maximalAdicFiniteBaseChangeLeftAlgebra

L54 ↗
EtaleFundamentalGroups.maximalAdicFiniteBaseChangeLeftAlgebra
Documentation

The left scalar algebra on the completed finite base change.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
def maximalAdicFiniteBaseChangeLeftAlgebra
    (R : Type uR) (S : Type uS)
    [CommRing R] [IsLocalRing R] [CommRing S] [Algebra R S] :
    Algebra (AdicCompletion (maximalIdeal R) R)
      (MaximalAdicFiniteBaseChange R S)
def

maximalAdicFiniteBaseChangeRightAlgebra

L62 ↗
EtaleFundamentalGroups.maximalAdicFiniteBaseChangeRightAlgebra
Documentation

The right scalar algebra on the completed finite base change.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
def maximalAdicFiniteBaseChangeRightAlgebra
    (R : Type uR) (S : Type uS)
    [CommRing R] [IsLocalRing R] [CommRing S] [Algebra R S] :
    Algebra S (MaximalAdicFiniteBaseChange R S)
def

maximalAdicFiniteBaseChangeIncludeLeft

L69 ↗
EtaleFundamentalGroups.maximalAdicFiniteBaseChangeIncludeLeft
Documentation

The left inclusion into the completed finite base change.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
def maximalAdicFiniteBaseChangeIncludeLeft
    (R : Type uR) (S : Type uS)
    [CommRing R] [IsLocalRing R] [CommRing S] [Algebra R S] :
    AdicCompletion (maximalIdeal R) R →ₐ[AdicCompletion (maximalIdeal R) R]
      MaximalAdicFiniteBaseChange R S
def

maximalAdicFiniteBaseChangeIncludeRight

L77 ↗
EtaleFundamentalGroups.maximalAdicFiniteBaseChangeIncludeRight
Documentation

The right inclusion into the completed finite base change.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
def maximalAdicFiniteBaseChangeIncludeRight
    (R : Type uR) (S : Type uS)
    [CommRing R] [IsLocalRing R] [CommRing S] [Algebra R S] :
    S →ₐ[R] MaximalAdicFiniteBaseChange R S
structure

AdicRetainedExactTensorPrimeData

L88 ↗
EtaleFundamentalGroups.AdicRetainedExactTensorPrimeData
Documentation

The exact tensor-prime data retained by maximal-adic completion.

Contractions are stored as explicit equalities rather than global Ideal.LiesOver instances. This keeps the unrelated localization and fraction-field instance graphs out of the public result type.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · full declaration
structure AdicRetainedExactTensorPrimeData
    {R : Type uR} {S : Type uS}
    [CommRing R] [IsLocalRing R]
    [CommRing S] [Algebra R S]
    (y : R) (e : ℕ) (q p : Ideal S) where
  /-- The selected generic-component prime in the completed finite base change. -/
  N : Ideal (MaximalAdicFiniteBaseChange R S)
  /-- The retained branch prime in the same completed finite base change. -/
  Q : Ideal (MaximalAdicFiniteBaseChange R S)
  /-- The selected component prime lies below the retained branch prime. -/
  hNQ : N ≤ Q
  /-- The retained branch prime lies below the extended closed prime. -/
  hQP : Q ≤ p.map (maximalAdicFiniteBaseChangeIncludeRight R S).toRingHom
  /-- The selected generic-component ideal is prime. -/
  hNPrime : N.IsPrime
  /-- The selected component contracts to the zero ideal of the completed base. -/
  hNOver :
    N.comap (maximalAdicFiniteBaseChangeIncludeLeft R S).toRingHom = ⊥
  /-- The retained branch ideal is prime. -/
  hQPrime : Q.IsPrime
  /-- The retained branch contracts on the original finite algebra to the chosen prime `q`. -/
  hQOver :
    Q.comap (maximalAdicFiniteBaseChangeIncludeRight R S).toRingHom = q
  /-- The left contraction of the retained branch is generated by the completed parameter `y`. -/
  hQBranch :
    Q.comap (maximalAdicFiniteBaseChangeIncludeLeft R S).toRingHom =
      Ideal.span
        ({algebraMap R (AdicCompletion (maximalIdeal R) R) y} :
          Set (AdicCompletion (maximalIdeal R) R))
  /-- The retained branch has the prescribed ramification index `e` over the completed base. -/
  hQExact :
    letI : Algebra (AdicCompletion (maximalIdeal R) R)
        (MaximalAdicFiniteBaseChange R S) :=
      maximalAdicFiniteBaseChangeLeftAlgebra R S
    Q.ramificationIdx (AdicCompletion (maximalIdeal R) R) = e
  /-- Localization at the branch is a discrete valuation domain in which the selected component
  ideal vanishes. -/
  hQLocal :
    letI : Q.IsPrime := hQPrime
    ∃ hQDomain : IsDomain (Localization.AtPrime Q),
      letI : IsDomain (Localization.AtPrime Q) := hQDomain
      IsDiscreteValuationRing (Localization.AtPrime Q) ∧
        N.map
          (algebraMap (MaximalAdicFiniteBaseChange R S)
            (Localization.AtPrime Q)) = ⊥
  /-- The extension of the closed prime to the completed finite base change is maximal. -/
  hPMaximal :
    (p.map (maximalAdicFiniteBaseChangeIncludeRight R S).toRingHom).IsMaximal
  /-- The extended closed prime contracts to the maximal ideal of the completed local base. -/
  hPOver :
    ∃ hRhatLocal : IsLocalRing (AdicCompletion (maximalIdeal R) R),
      letI : IsLocalRing (AdicCompletion (maximalIdeal R) R) := hRhatLocal
      (p.map (maximalAdicFiniteBaseChangeIncludeRight R S).toRingHom).comap
          (maximalAdicFiniteBaseChangeIncludeLeft R S).toRingHom =
        maximalIdeal (AdicCompletion (maximalIdeal R) R)
def

HasNormalizationChain

L151 ↗
EtaleFundamentalGroups.AdicRetainedExactTensorPrimeData.HasNormalizationChain
Documentation

A retained tensor-prime pair lifts to a prime chain in the normalization of its selected completed generic component.

All fraction-field and normalization instances are intentionally scoped to this predicate instead of being threaded through the enclosing theorem.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
namespace AdicRetainedExactTensorPrimeData
Lean source · statement
def HasNormalizationChain
    {R : Type uR} {S : Type uS} {L : Type uL}
    [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    [CommRing S] [IsDomain S] [Algebra R S]
    [Module.Finite R S] [FaithfulSMul R S]
    [Field L] [Algebra S L] [IsFractionRing S L]
    {y : R} {e : ℕ} {q p : Ideal S}
    (z : R) (hreg : IsRegular R [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal R)
    (data : AdicRetainedExactTensorPrimeData y e q p) : Prop
theorem

exists_adicCompletion_retainedExactTensorPrimeData

L214 ↗
EtaleFundamentalGroups.exists_adicCompletion_retainedExactTensorPrimeData
Documentation

Produce the height-one/DVR data while keeping its auxiliary instances inside the proof rather than in the result type.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
theorem exists_adicCompletion_retainedExactTensorPrimeData
    {R : Type uR} {S : Type uS}
    [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    [CommRing S] [IsDomain S] [IsIntegrallyClosed S] [Algebra R S]
    [Module.Finite R S] [Module.Flat R S] [FaithfulSMul R S]
    {y z : R} (hy : Prime y)
    (hreg : IsRegular R [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal R)
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    [CharZero (R ⧸ Ideal.span ({y} : Set R))]
    {e : ℕ}
    (q p : Ideal S) [q.IsPrime] [p.IsMaximal]
    [q.LiesOver (Ideal.span ({y} : Set R))]
    [p.LiesOver (maximalIdeal R)]
    (hqp : q ≤ p) (hqExact : q.ramificationIdx R = e) :
    Nonempty (AdicRetainedExactTensorPrimeData y e q p)
theorem

adicRetainedExactTensorPrimeData_hasNormalizationChain

L396 ↗
EtaleFundamentalGroups.adicRetainedExactTensorPrimeData_hasNormalizationChain
Documentation

Supply the normalization chain after the tensor-prime data has been constructed. Only this declaration sees the fraction-field instance graph.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
theorem adicRetainedExactTensorPrimeData_hasNormalizationChain
    {R : Type uR} {S : Type uS} {L : Type uL}
    [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    [CommRing S] [IsDomain S] [Algebra R S]
    [Module.Finite R S] [FaithfulSMul R S]
    [Field L] [Algebra S L] [IsFractionRing S L]
    {y z : R} {e : ℕ} {q p : Ideal S}
    (hreg : IsRegular R [y, z])
    (hgen : Ideal.ofList [y, z] = maximalIdeal R)
    (data : AdicRetainedExactTensorPrimeData y e q p) :
    AdicRetainedExactTensorPrimeData.HasNormalizationChain
      (L := L) z hreg hgen data
theorem

exists_adicCompletion_retainedExactTensorPrime_normalizationChain

L467 ↗
EtaleFundamentalGroups.exists_adicCompletion_retainedExactTensorPrime_normalizationChain
Documentation

Retain an exact regular branch through maximal-adic completion and lift its prime chain to the normalization of the one generic component selected by that same chain.

The only ramification equality supplied as input is the original one at q. The completed tensor-prime equality, the literal generic component, and both normalization primes are produced internally.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe uR uS uL
Lean source · statement
theorem exists_adicCompletion_retainedExactTensorPrime_normalizationChain
    {R : Type uR} {S : Type uS} {L : Type uL}
    [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    [CommRing S] [IsDomain S] [IsIntegrallyClosed S] [Algebra R S]
    [Module.Finite R S] [Module.Flat R S] [FaithfulSMul R S]
    [Field L] [Algebra S L] [IsFractionRing S L]
    {y : R} (hy : Prime y)
    (hyQuot : IsRegularLocalRing (R ⧸ Ideal.span ({y} : Set R)))
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞))
    [CharZero (R ⧸ Ideal.span ({y} : Set R))]
    {e : ℕ}
    (q p : Ideal S) [q.IsPrime] [p.IsMaximal]
    [q.LiesOver (Ideal.span ({y} : Set R))]
    [p.LiesOver (maximalIdeal R)]
    (hqp : q ≤ p) (hqExact : q.ramificationIdx R = e) :
    ∃ z : R,
      ∃ hreg : IsRegular R [y, z],
      ∃ hgen : Ideal.ofList [y, z] = maximalIdeal R,
      ∃ data : AdicRetainedExactTensorPrimeData y e q p,
        AdicRetainedExactTensorPrimeData.HasNormalizationChain
          (L := L) z hreg hgen data

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