NYLL
Module

ExponentUnit.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Intermediate.ExponentUnit
6 declarations indexed from sourceView source ↗

Module documentation

The selected intermediate-root exponent is a boundary unit

Let A be a two-parameter regular local domain with selected boundary parameter t, and let K be its fraction field. In a pure radical field extension L / K, every intermediate field F has a concrete generator β satisfying β ^ [F : K] = t. If the actual normalization of A in F is etale away from t, then [F : K] is invertible modulo t.

The proof constructs the root algebra from β; neither its identification with the normalization nor the desired unit assertion is assumed.

Imports15
Imported by5

Declarations

def

oneRootBaseChangeAlgEquiv

L47 ↗
EtaleFundamentalGroups.Kummer.oneRootBaseChangeAlgEquiv
Documentation

Base change of one pure root algebra, in the ordinary AdjoinRoot presentation.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing Polynomial
open scoped BigOperators TensorProduct
universe u v w z
Lean source · statement
def oneRootBaseChangeAlgEquiv
    {A S : Type u} [CommRing A] [CommRing S] [Algebra A S]
    (m : ℕ) (t : A) :
    S ⊗[A] AdjoinRoot (X ^ m - C t) ≃ₐ[S]
      AdjoinRoot (X ^ m - C (algebraMap A S t))
def

oneIteratedRadicalAlgEquiv

L85 ↗
EtaleFundamentalGroups.Kummer.oneIteratedRadicalAlgEquiv
Documentation

The one-stage recursive radical is the ordinary one-root algebra.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing Polynomial
open scoped BigOperators TensorProduct
universe u v w z
Lean source · full declaration
def oneIteratedRadicalAlgEquiv
    (A : Type u) [CommRing A] (m : ℕ) (t : A) :
    iteratedRadical A 1 (fun _ : Fin 1 ↦ m) (fun _ : Fin 1 ↦ t) ≃ₐ[A]
      AdjoinRoot (X ^ m - C t) := by
  let n₁ : Fin 1 → ℕ := fun _ ↦ m
  let a₁ : Fin 1 → A := fun _ ↦ t
  let T : CommAlgCat.{u} A :=
    iteratedRadical A 0 (Fin.init n₁) (Fin.init a₁)
  let pT : T[X] :=
    X ^ n₁ (Fin.last 0) -
      C (algebraMap A T (a₁ (Fin.last 0)))
  let pA : A[X] := X ^ m - C t
  let ePrefix : T ≃ₐ[A] A := AlgEquiv.refl
  change AdjoinRoot pT ≃ₐ[A] AdjoinRoot pA
  exact AdjoinRoot.mapAlgEquiv ePrefix pT pA <| by
    apply Associated.of_eq
    dsimp only [pT, pA, n₁, a₁]
    rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_C]
    rfl
theorem

awayMap_formallyUnramified_of_normalization_etale

L108 ↗
EtaleFundamentalGroups.Kummer.awayMap_formallyUnramified_of_normalization_etale
Documentation

The actual normalization being etale away from t makes the localized pure-root model formally unramified. The root model and its normalization structure are constructed from the field generator.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing Polynomial
open scoped BigOperators TensorProduct
universe u v w z
Lean source · statement
theorem awayMap_formallyUnramified_of_normalization_etale
    {A : Type u} {K : Type v} {F : Type w}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field F] [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F]
    {m : ℕ} (hm : 0 < m) {t y : A}
    (hreg : RingTheory.Sequence.IsRegular A [t, y])
    (hgen : Ideal.ofList [t, y] = maximalIdeal A)
    (β : F) (hdegree : Module.finrank K F = m)
    (hβpow : β ^ m = algebraMap K F (algebraMap A K t))
    (hβgen : IntermediateField.adjoin K {β} = ⊤)
    [Module.Finite A (integralClosure A F)]
    (hEtale : RingHom.Etale
      (R := Localization.Away t)
      (S := Localization.Away (algebraMap A (integralClosure A F) t))
      (Localization.awayMap
        (algebraMap A (integralClosure A F)) t)) :
    RingHom.FormallyUnramified
      (Localization.awayMap
        (algebraMap A (AdjoinRoot (X ^ m - C t))) t)
theorem

awayMap_formallyUnramified_of_embedded_normalization_etale

L275 ↗
EtaleFundamentalGroups.Kummer.awayMap_formallyUnramified_of_embedded_normalization_etale
Documentation

The embedded variant of awayMap_formallyUnramified_of_normalization_etale.

Here the pure-root fraction field is F, but the normalization whose etaleness is known may be taken in any finite separable overfield M of F. The proof deliberately runs purity on the tower B ⊆ F ⊆ M. Consequently no descent statement identifying the normalization in F with a subalgebra of the normalization in M is needed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing Polynomial
open scoped BigOperators TensorProduct
universe u v w z
Lean source · statement
theorem awayMap_formallyUnramified_of_embedded_normalization_etale
    {A : Type u} {K : Type v} {F : Type w} {M : Type z}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field F] [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F]
    [Field M] [Algebra K M] [Algebra A M] [IsScalarTower A K M]
    [Algebra F M] [IsScalarTower K F M] [IsScalarTower A F M]
    [FiniteDimensional F M] [Algebra.IsSeparable F M]
    {m : ℕ} (hm : 0 < m) {t y : A}
    (hreg : RingTheory.Sequence.IsRegular A [t, y])
    (hgen : Ideal.ofList [t, y] = maximalIdeal A)
    (β : F) (hdegree : Module.finrank K F = m)
    (hβpow : β ^ m = algebraMap K F (algebraMap A K t))
    (hβgen : IntermediateField.adjoin K {β} = ⊤)
    [Module.Finite A (integralClosure A M)]
    (hEtale : RingHom.Etale
      (Localization.awayMap
        (algebraMap A (integralClosure A M)) t)) :
    RingHom.FormallyUnramified
      (Localization.awayMap
        (algebraMap A (AdjoinRoot (X ^ m - C t))) t)
theorem

selectedIntermediateRootExponent_isUnit_mod

L447 ↗
EtaleFundamentalGroups.Kummer.selectedIntermediateRootExponent_isUnit_mod
Documentation

For a selected intermediate field of a pure radical extension, etaleness of its actual normalization off the selected boundary forces the intermediate degree to be a unit on that boundary component.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing Polynomial
open scoped BigOperators TensorProduct
universe u v w z
Lean source · statement
theorem selectedIntermediateRootExponent_isUnit_mod
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L]
    {t y : A}
    (hreg : RingTheory.Sequence.IsRegular A [t, y])
    (hgen : Ideal.ofList [t, y] = maximalIdeal A)
    (hCharZero : CharZero (A ⧸ Ideal.span {t}))
    (α : L)
    (hpow : α ^ Module.finrank K L =
      algebraMap K L (algebraMap A K t))
    (hαgen : IntermediateField.adjoin K {α} = ⊤)
    (F : IntermediateField K L)
    [Module.Finite A (integralClosure A F)]
    (hEtale : RingHom.Etale
      (R := Localization.Away t)
      (S := Localization.Away (algebraMap A (integralClosure A F) t))
      (Localization.awayMap
        (algebraMap A (integralClosure A F)) t)) :
    IsUnit (Module.finrank K F : A ⧸ Ideal.span {t})
theorem

selectedIntermediateRootExponent_isUnit_mod_of_embedded_normalization_etale

L587 ↗
EtaleFundamentalGroups.Kummer.selectedIntermediateRootExponent_isUnit_mod_of_embedded_normalization_etale
Documentation

Embedded-normalization form of selectedIntermediateRootExponent_isUnit_mod.

The intermediate pure-root field F need not itself carry the normalization for which Away etaleness has been proved. It is enough that F embeds as a field subextension of a finite separable field M and that the normalization of the original regular local base in M is etale off the selected parameter. This is the form used after choosing one component of the other-root tensor product.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing Polynomial
open scoped BigOperators TensorProduct
universe u v w z
Lean source · statement
theorem selectedIntermediateRootExponent_isUnit_mod_of_embedded_normalization_etale
    {A : Type u} {K : Type v} {L : Type w} {M : Type z}
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L]
    [Field M] [Algebra K M] [Algebra A M] [IsScalarTower A K M]
    {t y : A}
    (hreg : RingTheory.Sequence.IsRegular A [t, y])
    (hgen : Ideal.ofList [t, y] = maximalIdeal A)
    (hCharZero : CharZero (A ⧸ Ideal.span ({t} : Set A)))
    (α : L)
    (hpow : α ^ Module.finrank K L =
      algebraMap K L (algebraMap A K t))
    (hαgen : IntermediateField.adjoin K {α} = ⊤)
    (F : IntermediateField K L)
    [Algebra F M] [IsScalarTower K F M] [IsScalarTower A F M]
    [FiniteDimensional F M] [Algebra.IsSeparable F M]
    [Module.Finite A (integralClosure A M)]
    (hEtale : RingHom.Etale
      (Localization.awayMap
        (algebraMap A (integralClosure A M)) t)) :
    IsUnit (Module.finrank K F : A ⧸ Ideal.span ({t} : Set A))

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