NYLL
Module

PrimeChain.lean

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

Module documentation

Retaining a prime chain under completion base change

Let q ≤ p be a prime and a closed prime in a finite model over a local base. A closed-point-preserving faithfully flat base change sends p to a specified maximal ideal P of the tensor product. Flat going-down then selects a prime Q ≤ P over the specified q. If the finite model is flat over the base, a second going-down step selects a generic prime below that same Q.

The point of the construction is that neither the height-one branch nor the closed factor is reselected after completion. The resulting chain is the finite-model input for selecting one literal completed generic component.

Imports3
Imported by5

Declarations

theorem

exists_tensorProduct_prime_le_retainedClosedPrime

L40 ↗
EtaleFundamentalGroups.exists_tensorProduct_prime_le_retainedClosedPrime
Documentation

A specified chain q ≤ p survives a closed-point-preserving faithfully flat base change inside the tensor factor selected by p.

The upper prime is produced by flat going-down from the literal extension of p; in particular it contracts to the supplied q, rather than merely to some prime below p.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
Lean source · full declaration
theorem exists_tensorProduct_prime_le_retainedClosedPrime
    {R : Type uR} {R' : Type uR'} {S : Type uS}
    [CommRing R] [CommRing R'] [CommRing S]
    [IsLocalRing R] [IsLocalRing R']
    [Algebra R R'] [Algebra R S]
    [IsLocalHom (algebraMap R R')]
    [Module.FaithfullyFlat R R']
    (q p : Ideal S) [q.IsPrime] [p.IsMaximal]
    [p.LiesOver (IsLocalRing.maximalIdeal R)]
    (hqp : q ≤ p)
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R'))) :
    let T := R' ⊗[R] S
    letI : Algebra S T := Algebra.TensorProduct.rightAlgebra
    let P := p.map (algebraMap S T)
    ∃ Q : Ideal T,
      Q ≤ P ∧ Q.IsPrime ∧ Q.LiesOver q ∧
        P.IsMaximal ∧ P.LiesOver (IsLocalRing.maximalIdeal R') := by
  dsimp only
  let T := R' ⊗[R] S
  let : Algebra S T := Algebra.TensorProduct.rightAlgebra
  let : IsScalarTower R S T :=
    Algebra.TensorProduct.right_isScalarTower
  let : Module.FaithfullyFlat S T :=
    Module.FaithfullyFlat.of_linearEquiv
      (R := S) (M := S ⊗[R] R')
      (Algebra.TensorProduct.commRight R S R').symm.toLinearEquiv
  let P := p.map (algebraMap S T)
  have hPGeometry :=
    tensorProduct_map_liesOver_maximalIdeal_of_residueFieldMap_bijective
      (R := R) (R' := R') p hmax hres
  let : P.IsPrime := hPGeometry.1.isPrime
  let : P.LiesOver p := by
    exact
      Ideal.LiesOver.mk
        (Ideal.comap_map_eq_self_of_faithfullyFlat
          (B := T) p).symm
  obtain ⟨Q, hQP, hQPrime, hQOver⟩ :=
    Ideal.exists_ideal_le_liesOver_of_le
      (R := S) (S := T) (p := q) (q := p) P hqp
  exact ⟨Q, hQP, hQPrime, hQOver,
    hPGeometry.1, hPGeometry.2⟩
theorem

exists_tensorProduct_genericPrime_le_prime_le_retainedClosedPrime

L89 ↗
EtaleFundamentalGroups.exists_tensorProduct_genericPrime_le_prime_le_retainedClosedPrime
Documentation

If the finite model is flat over the original base, the retained height-one/closed chain contains a generic prime over the generic point of the new base. Thus all three primes belong to one literal completed finite model component.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
Lean source · full declaration
theorem exists_tensorProduct_genericPrime_le_prime_le_retainedClosedPrime
    {R : Type uR} {R' : Type uR'} {S : Type uS}
    [CommRing R] [CommRing R'] [CommRing S]
    [IsLocalRing R] [IsLocalRing R'] [IsDomain R']
    [Algebra R R'] [Algebra R S]
    [IsLocalHom (algebraMap R R')]
    [Module.FaithfullyFlat R R'] [Module.Flat R S]
    (q p : Ideal S) [q.IsPrime] [p.IsMaximal]
    [p.LiesOver (IsLocalRing.maximalIdeal R)]
    (hqp : q ≤ p)
    (hmax : (IsLocalRing.maximalIdeal R).map (algebraMap R R') =
      IsLocalRing.maximalIdeal R')
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R R'))) :
    let T := R' ⊗[R] S
    letI : Algebra S T := Algebra.TensorProduct.rightAlgebra
    let P := p.map (algebraMap S T)
    ∃ N Q : Ideal T,
      N ≤ Q ∧ Q ≤ P ∧
        N.IsPrime ∧ N.LiesOver (⊥ : Ideal R') ∧
        Q.IsPrime ∧ Q.LiesOver q ∧
        P.IsMaximal ∧ P.LiesOver (IsLocalRing.maximalIdeal R') := by
  dsimp only
  let T := R' ⊗[R] S
  let : Algebra R' T := Algebra.TensorProduct.leftAlgebra
  let : Algebra S T := Algebra.TensorProduct.rightAlgebra
  let : IsScalarTower R R' T := inferInstance
  let : IsScalarTower R S T :=
    Algebra.TensorProduct.right_isScalarTower
  let : Module.Flat R' T := Module.Flat.baseChange R R' S
  obtain ⟨Q, hQP, hQPrime, hQOver, hPMax, hPOver⟩ :=
    exists_tensorProduct_prime_le_retainedClosedPrime
      (R := R) (R' := R') q p hqp hmax hres
  let : Q.IsPrime := hQPrime
  let qR' := Q.under R'
  let : qR'.IsPrime := hQPrime.comap (algebraMap R' T)
  let : Q.LiesOver qR' := Ideal.over_under (A := R') Q
  obtain ⟨N, hNQ, hNPrime, hNOver⟩ :=
    Ideal.exists_ideal_le_liesOver_of_le
      (R := R') (S := T) (p := (⊥ : Ideal R'))
      (q := qR') Q bot_le
  exact ⟨N, Q, hNQ, hQP, hNPrime, hNOver,
    hQPrime, hQOver, hPMax, hPOver⟩
theorem

exists_adicCompletion_genericPrime_le_prime_le_retainedClosedPrime

L136 ↗
EtaleFundamentalGroups.exists_adicCompletion_genericPrime_le_prime_le_retainedClosedPrime
Documentation

Maximal-adic specialization of the retained generic/height-one/closed prime chain. All completion geometry is supplied by the canonical adic completion map.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
Lean source · full declaration
theorem exists_adicCompletion_genericPrime_le_prime_le_retainedClosedPrime
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [IsDomain R]
    [IsNoetherianRing R] [IsLocalRing R]
    [Algebra R S] [Module.Flat R S]
    (q p : Ideal S) [q.IsPrime] [p.IsMaximal]
    [p.LiesOver (IsLocalRing.maximalIdeal R)]
    (hqp : q ≤ p)
    (hcompletionDomain :
      IsDomain (AdicCompletion (IsLocalRing.maximalIdeal R) R)) :
    let R' := AdicCompletion (IsLocalRing.maximalIdeal R) R
    let T := R' ⊗[R] S
    letI : Algebra S T := Algebra.TensorProduct.rightAlgebra
    let P := p.map (algebraMap S T)
    ∃ N Q : Ideal T,
      N ≤ Q ∧ Q ≤ P ∧
        N.IsPrime ∧ N.LiesOver (⊥ : Ideal R') ∧
        Q.IsPrime ∧ Q.LiesOver q ∧
        P.IsMaximal ∧ P.LiesOver (IsLocalRing.maximalIdeal R') := by
  dsimp only
  let R' := AdicCompletion (IsLocalRing.maximalIdeal R) R
  let : IsDomain R' := hcompletionDomain
  let : Module.FaithfullyFlat R R' :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  exact
    exists_tensorProduct_genericPrime_le_prime_le_retainedClosedPrime
      (R := R) (R' := R') q p hqp
      AdicCompletion.maximalIdeal_eq_map.symm
      (AdicCompletion.residueField_map_bijective R)
abbrev

retainedCompletedFiniteBaseChangeGenericFiber

L178 ↗
EtaleFundamentalGroups.retainedCompletedFiniteBaseChangeGenericFiber
Documentation

The generic fibre of a completed finite base change. This variant is parameterized by a supplied generic prime, rather than by an independently chosen closed factor.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · statement
abbrev retainedCompletedFiniteBaseChangeGenericFiber
def

retainedCompletedGenericIdeal

L183 ↗
EtaleFundamentalGroups.retainedCompletedGenericIdeal
Documentation

Extend a supplied generic prime of the completed finite model to its generic fibre.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
Lean source · statement
def retainedCompletedGenericIdeal
    (N : Ideal (R' ⊗[R] S)) :
    Ideal (retainedCompletedFiniteBaseChangeGenericFiber
      (R := R) (R' := R') (S := S) (K' := K'))
theorem

retainedCompletedGenericPrime_disjoint

L194 ↗
EtaleFundamentalGroups.retainedCompletedGenericPrime_disjoint
Source context 12 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
omit [IsDomain R] [IsDomain S] [Module.Finite R S] in
Lean source · full declaration
theorem retainedCompletedGenericPrime_disjoint
    (N : Ideal (R' ⊗[R] S)) [N.IsPrime]
    [N.LiesOver (⊥ : Ideal R')] :
    let T := R' ⊗[R] S
    Disjoint
      (Algebra.algebraMapSubmonoid T (nonZeroDivisors R') : Set T)
      (N : Set T) := by
  let T := R' ⊗[R] S
  rw [Set.disjoint_left]
  intro x hxM hxN
  rcases hxM with ⟨r, hr, rfl⟩
  have hrN : r ∈ N.under R' := hxN
  have hr0 : r = 0 := by
    have : r ∈ (⊥ : Ideal R') := by
      rw [N.over_def (⊥ : Ideal R')]
      exact hrN
    simpa only [Ideal.mem_bot] using this
  exact (nonZeroDivisors.coe_ne_zero ⟨r, hr⟩) hr0
theorem

retainedCompletedGenericIdeal_isMaximal

L216 ↗
EtaleFundamentalGroups.retainedCompletedGenericIdeal_isMaximal
Documentation

A supplied generic prime over zero becomes a maximal ideal after passing to the generic fibre of the completed finite model.

Source context 12 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
omit [IsDomain R] [IsDomain S] in
Lean source · statement
theorem retainedCompletedGenericIdeal_isMaximal
    (N : Ideal (R' ⊗[R] S)) [N.IsPrime]
    [N.LiesOver (⊥ : Ideal R')] :
    (retainedCompletedGenericIdeal
      (R := R) (R' := R') (S := S) (K' := K') N).IsMaximal
def

retainedCompletedGenericFiberEquiv

L258 ↗
EtaleFundamentalGroups.retainedCompletedGenericFiberEquiv
Documentation

Reassociate the generic fibre of the completed finite model with the literal field tensor K' ⊗[K] L.

Source context 18 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra S L] [IsFractionRing S L]
variable [Algebra R L] [IsScalarTower R S L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
def retainedCompletedGenericFiberEquiv :
    retainedCompletedFiniteBaseChangeGenericFiber
        (R := R) (R' := R') (S := S) (K' := K') ≃ₐ[K']
      (K' ⊗[K] L)
def

retainedCompletedGenericTensorIdeal

L276 ↗
EtaleFundamentalGroups.retainedCompletedGenericTensorIdeal
Documentation

The literal maximal ideal of K' ⊗[K] L selected by the supplied generic prime in the retained completion chain.

Source context 18 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra S L] [IsFractionRing S L]
variable [Algebra R L] [IsScalarTower R S L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
def retainedCompletedGenericTensorIdeal
    (N : Ideal (R' ⊗[R] S)) : Ideal (K' ⊗[K] L)
theorem

retainedCompletedGenericTensorIdeal_isMaximal

L286 ↗
EtaleFundamentalGroups.retainedCompletedGenericTensorIdeal_isMaximal
Documentation

The retained generic prime therefore selects a literal field component of the completed generic tensor product.

Source context 18 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uR' uS uK uL uK'
section LiteralGenericComponent
variable {R : Type uR} {R' : Type uR'} {S : Type uS}
variable [CommRing R] [IsDomain R]
variable [CommRing R'] [IsDomain R'] [Algebra R R']
variable [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
variable {K' : Type uK'} [Field K'] [Algebra R' K']
variable [IsFractionRing R' K']
variable {K : Type uK} {L : Type uL}
variable [Field K] [Algebra R K] [IsFractionRing R K]
variable [Field L] [Algebra S L] [IsFractionRing S L]
variable [Algebra R L] [IsScalarTower R S L]
variable [Algebra K L] [IsScalarTower R K L]
variable [Algebra R K'] [IsScalarTower R R' K']
variable [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
theorem retainedCompletedGenericTensorIdeal_isMaximal
    (N : Ideal (R' ⊗[R] S)) [hNPrime : N.IsPrime]
    [hNOver : N.LiesOver (⊥ : Ideal R')] :
    (retainedCompletedGenericTensorIdeal
      (R := R) (R' := R') (S := S) (K := K) (L := L)
      (K' := K') N).IsMaximal

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