Module

FiniteFlat.lean

Nyll.EtaleFundamentalGroups.Ramification.Tensor.FiniteFlat

13 declarations indexed from sourceView source ↗

Module documentation

Ramification under a finite, flat tensor square

Let S / R be finite and let R' / R be flat. A prime of R' ⊗[R] S has two contractions, one to S and one to R'. If the second contraction is the scheme-theoretic extension of the contraction to R, then the two horizontal ramification indices agree in residue characteristic zero.

The point which is not covered by the usual etale base-change lemma is that R' / R need not be etale (the intended application is an adic completion). Instead, the proof identifies the localization of the S-fiber at the retained tensor prime with a localization of

p'.ResidueField ⊗[p.ResidueField] q.ResidueField.

The latter is a reduced Artinian algebra: finiteness comes from S / R, and separability comes from residue characteristic zero. Its prime localizations are therefore fields, which says that the vertical ramification index is one. The tensor prime itself, rather than an independently selected component, is retained throughout.

Imports4

Mathlib.RingTheory.Etale.Field
Mathlib.RingTheory.Flat.Stability
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.RamificationInertia.Ramification

Imported by3

def

residueFieldFiberAlgEquiv

L51 ↗

EtaleFundamentalGroups.residueFieldFiberAlgEquiv

Documentation

Tensoring a residue field once more with the residue field below does not change it. This is the canonical localization-and-quotient identification; it does not choose a field component.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section ResidueTensor
variable {R : Type uR} {S : Type uS}
  [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

def residueFieldFiberAlgEquiv
    (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
    [IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)] :
    p.Fiber q.ResidueField ≃ₐ[p.ResidueField] q.ResidueField

theorem

isField_localizationAtPrime_finiteSeparableTensor

L125 ↗

EtaleFundamentalGroups.isField_localizationAtPrime_finiteSeparableTensor

Documentation

A prime localization of a finite separable tensor product of fields is a field.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section ResidueTensor
variable {R : Type uR} {S : Type uS}
  [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem isField_localizationAtPrime_finiteSeparableTensor
    {K H L : Type*} [Field K] [Field H] [Field L]
    [Algebra K H] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (m : Ideal (H ⊗[K] L)) [m.IsPrime] :
    IsField (Localization.AtPrime m)

instance

tensorSquareRightAlgebra

L162 ↗

EtaleFundamentalGroups.tensorSquareRightAlgebra

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/

Lean source · statement

instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S)

instance

tensorSquareRightScalarTower

L166 ↗

EtaleFundamentalGroups.tensorSquareRightScalarTower

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra

Lean source · statement

instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S)

instance

tensorSquareRightFlat

L170 ↗

EtaleFundamentalGroups.tensorSquareRightFlat

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower

Lean source · statement

instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S)

theorem

isField_localization_of_fiber_prime

L178 ↗

EtaleFundamentalGroups.isField_localization_of_fiber_prime

Documentation

Transfer the field property from a prime localization of a fiber back to the corresponding prime localization of the algebra. The fiber prime comparison is explicit, so only one localization-algebra instance is live.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem isField_localization_of_fiber_prime
    {A : Type*} [CommRing A] [Algebra R' A]
    (p' : Ideal R') [p'.IsPrime]
    (s : PrimeSpectrum (p'.Fiber A))
    (r : Ideal A) [r.IsPrime] [r.LiesOver p']
    (hrs : r = s.asIdeal.comap
      Algebra.TensorProduct.includeRight.toRingHom)
    (hpA : p'.map (algebraMap R' A) = ⊥)
    (hFieldS : IsField (Localization.AtPrime s.asIdeal)) :
    IsField (Localization.AtPrime r)

theorem

right_maximalIdeal_of_fiber_localization_isField

L264 ↗

EtaleFundamentalGroups.right_maximalIdeal_of_fiber_localization_isField

Documentation

A field localization of the retained fiber prime forces the vertical maximal ideal at the original tensor prime.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem right_maximalIdeal_of_fiber_localization_isField
    {T : Type*} [CommRing T] [Algebra S T]
    (q : Ideal S) [q.IsPrime]
    (Q : Ideal T) [Q.IsPrime] [Q.LiesOver q]
    (r : PrimeSpectrum (q.Fiber T))
    (hQr : Q = r.asIdeal.comap
      Algebra.TensorProduct.includeRight.toRingHom)
    (hFieldR : IsField (Localization.AtPrime r.asIdeal)) :
    q.map (algebraMap S (Localization.AtPrime Q)) =
      IsLocalRing.maximalIdeal (Localization.AtPrime Q)

theorem

tensorProduct_localization_right_maximalIdeal_core

L371 ↗

EtaleFundamentalGroups.tensorProduct_localization_right_maximalIdeal_core

Documentation

Construct the vertical maximal-ideal equality at the retained tensor prime. All residue-fiber instances are owned by this boundary; callers see only the canonical right tensor algebra fixed above.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem tensorProduct_localization_right_maximalIdeal_core
    [Module.Finite R S] [Module.Flat R R']
    (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (p' : Ideal R')
    (Q : Ideal (R' ⊗[R] S)) [Q.IsPrime] [Q.LiesOver p']
    (hQq : Q.comap
      Algebra.TensorProduct.includeRight.toRingHom = q)
    (hpmap : p.map (algebraMap R R') = p')
    [CharZero (R ⧸ p)] :
    q.map (algebraMap S (Localization.AtPrime Q)) =
      IsLocalRing.maximalIdeal (Localization.AtPrime Q)

theorem

ramificationIdx_tensorProduct_eq_of_finite_flat_charZero

L536 ↗

EtaleFundamentalGroups.ramificationIdx_tensorProduct_eq_of_finite_flat_charZero

Documentation

Ramification is preserved at the retained prime of a finite tensor square after a flat base change in residue characteristic zero.

hQq is the literal right-coordinate contraction of Q; hpmap says that its left contraction is the scheme-theoretic extension of p. Neither a tensor component, a residue-field comparison, nor a ramification-index equality is supplied as an input.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem ramificationIdx_tensorProduct_eq_of_finite_flat_charZero
    [Module.Finite R S] [Module.Flat R R']
    (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (p' : Ideal R')
    (Q : Ideal (R' ⊗[R] S)) [Q.IsPrime] [Q.LiesOver p']
    (hQq : Q.comap
      Algebra.TensorProduct.includeRight.toRingHom = q)
    (hpmap : p.map (algebraMap R R') = p')
    [CharZero (R ⧸ p)] :
    Q.ramificationIdx R' = q.ramificationIdx R

theorem

tensorProduct_localization_right_maximalIdeal_eq_of_finite_flat_charZero

L589 ↗

EtaleFundamentalGroups.tensorProduct_localization_right_maximalIdeal_eq_of_finite_flat_charZero

Documentation

At the retained tensor prime, the vertical local maximal ideal is exactly the extension of the old prime.

This is the ideal-theoretic content hidden behind the vertical ramification index one in ramificationIdx_tensorProduct_eq_of_finite_flat_charZero. It is useful before passing to a normalization: no independently chosen prime, formal unramifiedness hypothesis, or comparison of local rings is supplied.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem tensorProduct_localization_right_maximalIdeal_eq_of_finite_flat_charZero
    [Module.Finite R S] [Module.Flat R R']
    (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (p' : Ideal R')
    (Q : Ideal (R' ⊗[R] S)) [Q.IsPrime] [Q.LiesOver p']
    (hQq : Q.comap
      Algebra.TensorProduct.includeRight.toRingHom = q)
    (hpmap : p.map (algebraMap R R') = p')
    [CharZero (R ⧸ p)] :
    q.map (algebraMap S (Localization.AtPrime Q)) =
      IsLocalRing.maximalIdeal (Localization.AtPrime Q)

theorem

tensorProduct_localization_right_maximalIdeal_eq_span_of_finite_flat_charZero

L608 ↗

EtaleFundamentalGroups.tensorProduct_localization_right_maximalIdeal_eq_span_of_finite_flat_charZero

Documentation

Principal-branch form of tensorProduct_localization_right_maximalIdeal_eq_of_finite_flat_charZero. The equality between the mapped source branch and the completed branch is discharged by Ideal.map_span.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem tensorProduct_localization_right_maximalIdeal_eq_span_of_finite_flat_charZero
    [Module.Finite R S] [Module.Flat R R']
    (y : R)
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (Ideal.span ({y} : Set R))]
    (Q : Ideal (R' ⊗[R] S)) [Q.IsPrime]
    [Q.LiesOver
      (Ideal.span ({algebraMap R R' y} : Set R'))]
    (hQq : Q.comap
      Algebra.TensorProduct.includeRight.toRingHom = q)
    [CharZero (R ⧸ Ideal.span ({y} : Set R))] :
    q.map (algebraMap S (Localization.AtPrime Q)) =
      IsLocalRing.maximalIdeal (Localization.AtPrime Q)

theorem

ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero

L635 ↗

EtaleFundamentalGroups.ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero

Documentation

Application form for a retained completion prime over a principal height-one boundary. The mapped-prime equality is generated internally from Ideal.map_span; the only prime comparison is the literal right contraction of the retained tensor prime.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero
    [Module.Finite R S] [Module.Flat R R']
    (y : R)
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (Ideal.span ({y} : Set R))]
    (Q : Ideal (R' ⊗[R] S)) [Q.IsPrime]
    [Q.LiesOver
      (Ideal.span ({algebraMap R R' y} : Set R'))]
    (hQq : Q.comap
      Algebra.TensorProduct.includeRight.toRingHom = q)
    [CharZero (R ⧸ Ideal.span ({y} : Set R))] :
    Q.ramificationIdx R' = q.ramificationIdx R

theorem

ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero_of_eq

L658 ↗

EtaleFundamentalGroups.ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero_of_eq

Documentation

Exact-index form used after a selected branch has supplied its ramification index before completion.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uS uR'
section TensorSquare
variable {R : Type uR} {S : Type uS} {R' : Type uR'}
  [CommRing R] [CommRing S] [CommRing R']
  [Algebra R S] [Algebra R R']

/- The canonical right tensor algebra, scalar tower, and inherited flatness
are owned here once.  This prevents each public wrapper from rebuilding the
same instance path. -/
local instance tensorSquareRightAlgebra :
    Algebra S (R' ⊗[R] S) :=
  Algebra.TensorProduct.rightAlgebra
local instance tensorSquareRightScalarTower :
    IsScalarTower R S (R' ⊗[R] S) :=
  Algebra.TensorProduct.right_isScalarTower
local instance tensorSquareRightFlat [Module.Flat R R'] :
    Module.Flat S (R' ⊗[R] S) :=
  Module.Flat.of_linearEquiv
    (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv

Lean source · statement

theorem ramificationIdx_tensorProduct_span_eq_of_finite_flat_charZero_of_eq
    [Module.Finite R S] [Module.Flat R R']
    (y : R)
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (Ideal.span ({y} : Set R))]
    (Q : Ideal (R' ⊗[R] S)) [Q.IsPrime]
    [Q.LiesOver
      (Ideal.span ({algebraMap R R' y} : Set R'))]
    (hQq : Q.comap
      Algebra.TensorProduct.includeRight.toRingHom = q)
    [CharZero (R ⧸ Ideal.span ({y} : Set R))]
    {N : ℕ} (hq : q.ramificationIdx R = N) :
    Q.ramificationIdx R' = N

Module documentation

Ramification under a finite, flat tensor square

Declarations