NYLL
Module

HenselianClassification.lean

Nyll.EtaleFundamentalGroups.Kummer.PureRadical.HenselianClassification
2 declarations indexed from sourceView source ↗

Module documentation

Pure-radical classification over a Henselian local base

The abstract intermediate-field theorem needs to know that the relevant roots of unity in the radical field already lie in the base field. This file produces that input from the integral local model used in the one-divisor Abhyankar argument: a Henselian base, an integral normal local algebra with the same residue field, and its fraction field.

Imports3
Imported by2

Declarations

theorem

rootOfUnity_mem_fractionBase_of_henselian_of_residue_bijective

L37 ↗
EtaleFundamentalGroups.Kummer.rootOfUnity_mem_fractionBase_of_henselian_of_residue_bijective
Documentation

A root of unity in the fraction field of an integral normal local extension with unchanged residue field comes from the fraction field of the Henselian base.

The unit condition on n makes X ^ n - 1 separable at every root. The root is first pulled into the integral closure, its residue is lifted by Hensel's lemma, and uniqueness of a simple root in the target local domain identifies the two lifts.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w x
Lean source · statement
theorem rootOfUnity_mem_fractionBase_of_henselian_of_residue_bijective
    {A : Type u} {B : Type v} {K : Type w} {L : Type x}
    [CommRing A] [CommRing B] [IsDomain B]
    [HenselianLocalRing A] [IsLocalRing B]
    [Field K] [Field L]
    [Algebra A B] [Algebra A K] [Algebra B L] [Algebra K L]
    [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
    [IsFractionRing B L] [IsIntegrallyClosed B]
    [Algebra.IsIntegral A B] [IsLocalHom (algebraMap A B)]
    {n : ℕ} (hnUnit : IsUnit (n : A))
    (hresidue : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap A B)))
    (ζ : L) (hζpow : ζ ^ n = 1) :
    ζ ∈ Set.range (algebraMap K L)
theorem

exists_intermediateField_eq_adjoin_pow_of_henselian_pureRadical

L130 ↗
EtaleFundamentalGroups.Kummer.exists_intermediateField_eq_adjoin_pow_of_henselian_pureRadical
Documentation

Henselian integral-model form of the pure-radical intermediate-field classification. The roots-of-unity hypothesis of the abstract theorem is produced from the normal local integral model and its unchanged residue field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w x
Lean source · statement
theorem exists_intermediateField_eq_adjoin_pow_of_henselian_pureRadical
    {A : Type u} {B : Type v} {K : Type w} {L : Type x}
    [CommRing A] [CommRing B] [IsDomain B]
    [HenselianLocalRing A] [IsLocalRing B]
    [Field K] [Field L]
    [Algebra A B] [Algebra A K] [Algebra B L] [Algebra K L]
    [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
    [IsFractionRing B L] [IsIntegrallyClosed B]
    [Algebra.IsIntegral A B] [IsLocalHom (algebraMap A B)]
    [FiniteDimensional K L]
    (α : L) (hα : α ≠ 0)
    (hpow : α ^ Module.finrank K L ∈ Set.range (algebraMap K L))
    (hgen : IntermediateField.adjoin K {α} = ⊤)
    (hdegreeUnit : IsUnit (Module.finrank K L : A))
    (hresidue : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap A B)))
    (F : IntermediateField K L) :
    ∃ d : ℕ, d ∣ Module.finrank K L ∧
      F = IntermediateField.adjoin K {α ^ d}

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