NYLL
Module

IntegralExtensionLocalFactors.lean

Nyll.EtaleFundamentalGroups.Completions.DVR.IntegralExtensionLocalFactors
6 declarations indexed from sourceView source ↗

Module documentation

Completed local factors of a finite DVR extension

For a finite Dedekind extension C / V, base change to the actual valued-field completion of the fraction field of V is the product of the completed local rings at the primes of C above the closed point. Each local completion is then identified with the valuation subring in the actual valued-field completion of the fraction field of C for that prime.

Imports6
Imported by2

Declarations

abbrev

completedPrimeValuationSubring

L42 ↗
EtaleFundamentalGroups.completedPrimeValuationSubring
Documentation

The valuation subring in the actual completion of the fraction field of C, for the valuation defined by a prime Q above the closed point of V.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uV uC uK uL
variable {V : Type uV} {C : Type uC}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [CommRing C] [IsDedekindDomain C]
variable [Algebra V C] [Algebra.IsIntegral V C]
variable [Module.IsTorsionFree V C] [Module.Finite V C]
variable {K : Type uK} [Field K] [Algebra V K] [IsFractionRing V K]
variable {L : Type uL} [Field L] [Algebra C L] [IsFractionRing C L]
Lean source · statement
abbrev completedPrimeValuationSubring
    (Q : (IsLocalRing.maximalIdeal V).primesOver C) : Type uL
def

completedPrimeAdicEquivValuationSubring

L60 ↗
EtaleFundamentalGroups.completedPrimeAdicEquivValuationSubring
Documentation

The completion of the local ring at Q is the valuation subring in its actual valued-field completion.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uV uC uK uL
variable {V : Type uV} {C : Type uC}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [CommRing C] [IsDedekindDomain C]
variable [Algebra V C] [Algebra.IsIntegral V C]
variable [Module.IsTorsionFree V C] [Module.Finite V C]
variable {K : Type uK} [Field K] [Algebra V K] [IsFractionRing V K]
variable {L : Type uL} [Field L] [Algebra C L] [IsFractionRing C L]
Lean source · statement
def completedPrimeAdicEquivValuationSubring
    (Q : (IsLocalRing.maximalIdeal V).primesOver C) :
    AdicCompletion
        (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
        (Localization.AtPrime Q.1) ≃+*
      completedPrimeValuationSubring (L := L) Q
def

completedPrimeMap

L85 ↗
EtaleFundamentalGroups.completedPrimeMap
Documentation

The canonical map from the integral extension to the completed valuation subring selected by Q.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uV uC uK uL
variable {V : Type uV} {C : Type uC}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [CommRing C] [IsDedekindDomain C]
variable [Algebra V C] [Algebra.IsIntegral V C]
variable [Module.IsTorsionFree V C] [Module.Finite V C]
variable {K : Type uK} [Field K] [Algebra V K] [IsFractionRing V K]
variable {L : Type uL} [Field L] [Algebra C L] [IsFractionRing C L]
Lean source · statement
def completedPrimeMap
    (Q : (IsLocalRing.maximalIdeal V).primesOver C) :
    C →+* completedPrimeValuationSubring (L := L) Q
theorem

completedPrimeMap_comap_maximalIdeal

L106 ↗
EtaleFundamentalGroups.completedPrimeMap_comap_maximalIdeal
Documentation

The completed factor map remembers the original prime: the completed maximal ideal contracts exactly to Q.

Source context 12 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uV uC uK uL
variable {V : Type uV} {C : Type uC}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [CommRing C] [IsDedekindDomain C]
variable [Algebra V C] [Algebra.IsIntegral V C]
variable [Module.IsTorsionFree V C] [Module.Finite V C]
variable {K : Type uK} [Field K] [Algebra V K] [IsFractionRing V K]
variable {L : Type uL} [Field L] [Algebra C L] [IsFractionRing C L]
omit [Algebra.IsIntegral V C] in
Lean source · statement
theorem completedPrimeMap_comap_maximalIdeal
    (Q : (IsLocalRing.maximalIdeal V).primesOver C) :
    (IsLocalRing.maximalIdeal
      (completedPrimeValuationSubring (L := L) Q)).comap
        (completedPrimeMap (L := L) Q) = Q.1
def

completedDVRIntegralExtensionLocalFactorsRingEquiv

L135 ↗
EtaleFundamentalGroups.completedDVRIntegralExtensionLocalFactorsRingEquiv
Documentation

Base change of a finite Dedekind extension to the actual completion of the base DVR splits canonically into its completed local factors.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uV uC uK uL
variable {V : Type uV} {C : Type uC}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [CommRing C] [IsDedekindDomain C]
variable [Algebra V C] [Algebra.IsIntegral V C]
variable [Module.IsTorsionFree V C] [Module.Finite V C]
variable {K : Type uK} [Field K] [Algebra V K] [IsFractionRing V K]
variable {L : Type uL} [Field L] [Algebra C L] [IsFractionRing C L]
Lean source · full declaration
def completedDVRIntegralExtensionLocalFactorsRingEquiv :
    let p := IsLocalRing.maximalIdeal V
    let baseHat := standardDVFCompletionCompleteDVF V K
    letI : Algebra V baseHat.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    (baseHat.valuationSubring ⊗[V] C) ≃+*
      ∀ Q : p.primesOver C,
        completedPrimeValuationSubring (L := L) Q := by
  let p := IsLocalRing.maximalIdeal V
  have hp : p ≠ ⊥ := by
    simpa [p, ne_eq, ← IsLocalRing.isField_iff_maximalIdeal_eq] using
      (IsDiscreteValuationRing.not_isField V)
  let baseHat := standardDVFCompletionCompleteDVF V K
  letI : Algebra V baseHat.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  let eBase : AdicCompletion p V ≃ₐ[V] baseHat.valuationSubring :=
    standardDVRAdicCompletionEquivCompletionValuationSubring V K
  let eTensor : (baseHat.valuationSubring ⊗[V] C) ≃ₐ[V]
      (AdicCompletion p V ⊗[V] C) :=
    Algebra.TensorProduct.congr eBase.symm (AlgEquiv.refl : C ≃ₐ[V] C)
  let eMapped : (AdicCompletion p V ⊗[V] C) ≃+*
      AdicCompletion (p.map (algebraMap V C)) C :=
    tensorProductMappedIdealCompletionFreeRingEquiv
      (R₀ := V) (S₀ := C) p
  let eLocal :=
    adicCompletionIntegralExtensionLocalFactorsRingEquiv
      (A := V) (B := C) p hp
  let eActual :
      (∀ Q : p.primesOver C,
        AdicCompletion
          (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
          (Localization.AtPrime Q.1)) ≃+*
      (∀ Q : p.primesOver C,
        completedPrimeValuationSubring (L := L) Q) :=
    RingEquiv.piCongrRight fun Q =>
      completedPrimeAdicEquivValuationSubring (L := L) Q
  exact eTensor.toRingEquiv.trans (eMapped.trans (eLocal.trans eActual))
theorem

completedDVRIntegralExtensionLocalFactorsRingEquiv_includeRight_apply

L176 ↗
EtaleFundamentalGroups.completedDVRIntegralExtensionLocalFactorsRingEquiv_includeRight_apply
Documentation

On the right tensor factor, the global product decomposition is exactly the canonical map into the completed local factor selected by Q.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uV uC uK uL
variable {V : Type uV} {C : Type uC}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [CommRing C] [IsDedekindDomain C]
variable [Algebra V C] [Algebra.IsIntegral V C]
variable [Module.IsTorsionFree V C] [Module.Finite V C]
variable {K : Type uK} [Field K] [Algebra V K] [IsFractionRing V K]
variable {L : Type uL} [Field L] [Algebra C L] [IsFractionRing C L]
Lean source · full declaration
theorem completedDVRIntegralExtensionLocalFactorsRingEquiv_includeRight_apply
    (x : C) (Q : (IsLocalRing.maximalIdeal V).primesOver C) :
    let baseHat := standardDVFCompletionCompleteDVF V K
    letI : Algebra V baseHat.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    completedDVRIntegralExtensionLocalFactorsRingEquiv
        (V := V) (C := C) (K := K) (L := L)
        (Algebra.TensorProduct.includeRight x) Q =
      completedPrimeMap (L := L) Q x := by
  let p := IsLocalRing.maximalIdeal V
  have hp : p ≠ ⊥ := by
    simpa [p, ne_eq, ← IsLocalRing.isField_iff_maximalIdeal_eq] using
      (IsDiscreteValuationRing.not_isField V)
  have hQ : Q.1 ≠ ⊥ :=
    Ideal.ne_bot_of_liesOver_of_ne_bot hp Q.1
  let W := Localization.AtPrime Q.1
  let : IsDiscreteValuationRing W :=
    IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain C hQ W
  let : Algebra W L :=
    localizationAtPrimeToFractionFieldAlgebra (K := L) Q.1
  let : IsFractionRing W L :=
    localizationAtPrimeToFractionField_isFractionRing (K := L) Q.1
  dsimp only [completedDVRIntegralExtensionLocalFactorsRingEquiv,
    completedPrimeMap, completedPrimeAdicEquivValuationSubring]
  simp only [RingEquiv.trans_apply, RingEquiv.piCongrRight_apply,
    AlgEquiv.coe_ringEquiv, Algebra.TensorProduct.congr_apply,
    Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul,
    map_one,
    adicCompletionIntegralExtensionLocalFactorsRingEquiv_apply]
  rw [← Algebra.TensorProduct.includeRight_apply,
    tensorProductMappedIdealCompletionFreeRingEquiv_includeRight_apply,
    adicCompletionIntegralExtensionEquivPi_of,
    adicCompletionPrimePowerLocalFactorAlgEquiv_of]
  change standardDVRAdicCompletionEquivCompletionValuationSubring
      (Localization.AtPrime Q.1) L
        (AdicCompletion.of
          (IsLocalRing.maximalIdeal (Localization.AtPrime Q.1))
          (Localization.AtPrime Q.1)
          (algebraMap C (Localization.AtPrime Q.1) x)) =
    standardDVRToCompletionValuationSubringMap
      (Localization.AtPrime Q.1) L
        (algebraMap C (Localization.AtPrime Q.1) x)
  rw [standardDVRAdicCompletionEquivCompletionValuationSubring_apply_of]
  rfl

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