EtaleFundamentalGroups.Kummer.integralClosure_completeDVFFactorialRootTensorProduct_etale
Over a complete discrete valuation field, the normalization of the factorial uniformizer-root generic tensor product is etale over the integral root ring. All selected actual factors are constructed componentwise and then assembled through the canonical Artinian product decomposition.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
universe u v wLean source · full declaration
theorem integralClosure_completeDVFFactorialRootTensorProduct_etale
{K : Type u} {L : Type w} [Field K] [Field L]
[Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
(base : CompleteDVF.{u, v} K)
[CharZero base.residueField]
(varpi : base.valuationSubring)
(hvarpi : base.valuation.IsUniformizer (varpi : K))
(D : ℕ) (hdegree : Module.finrank K L ≤ D) :
let V := base.valuationSubring
letI : IsFractionRing V K :=
base.toDVF.valuationSubring_isFractionRing
letI : IsIntegrallyClosed V :=
base.toDVF.valuationSubring_isIntegrallyClosed
let N := D.factorial
let Rn := AdjoinRoot (X ^ N - C varpi)
letI : IsDomain Rn :=
completeDVFFactorialRootRing_isDomain base varpi hvarpi D
let F := FractionRing Rn
letI : Algebra K F :=
completeDVFFactorialRootFractionFieldAlgebra base varpi hvarpi D
letI : IsScalarTower V K F :=
completeDVFFactorialRootFractionField_isScalarTower
base varpi hvarpi D
let G := F ⊗[K] L
letI : Algebra Rn G :=
genericTensorProductLeftScalarAlgebra
(R := Rn) (K := K) (F := F) (L := L)
Algebra.Etale Rn (integralClosure Rn G) := by
dsimp only
let V := base.valuationSubring
let N := D.factorial
let Rn := AdjoinRoot (X ^ N - C varpi)
let : IsFractionRing V K :=
base.toDVF.valuationSubring_isFractionRing
let : IsIntegrallyClosed V :=
base.toDVF.valuationSubring_isIntegrallyClosed
let : IsDomain Rn :=
completeDVFFactorialRootRing_isDomain base varpi hvarpi D
let F := FractionRing Rn
let : Algebra K F :=
completeDVFFactorialRootFractionFieldAlgebra base varpi hvarpi D
let : IsScalarTower V K F :=
completeDVFFactorialRootFractionField_isScalarTower
base varpi hvarpi D
let G := F ⊗[K] L
let : Algebra Rn G :=
genericTensorProductLeftScalarAlgebra
(R := Rn) (K := K) (F := F) (L := L)
apply integralClosure_genericTensorProduct_etale
intro m hm
let : m.IsMaximal := hm
exact
integralClosure_completeDVFFactorialRootTensorComponent_etale
base varpi hvarpi D hdegree m hm