NYLL
Module

IntermediateCoordinates.lean

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

Module documentation

Coordinates on intermediate fields of a pure radical extension

The intermediate-field equality is converted here into the concrete generator needed by the one-divisor normalization argument. If e = [L : K], d = [L : F], and m = [F : K], then the generator is β = α ^ d, it satisfies β ^ m = π, and m * d = e.

Imports1
Imported by2

Declarations

theorem

exists_intermediateField_generator_pow_eq_of_pureRadical

L26 ↗
EtaleFundamentalGroups.Kummer.exists_intermediateField_generator_pow_eq_of_pureRadical
Documentation

Concrete generator and degree coordinates for an intermediate field of a pure radical extension.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v w x
Lean source · statement
theorem exists_intermediateField_generator_pow_eq_of_pureRadical
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (α : L) (hα : α ≠ 0) (π : K)
    (hpow : α ^ Module.finrank K L = algebraMap K L π)
    (hgen : IntermediateField.adjoin K {α} = ⊤)
    (hroots : ∀ ζ : L, ζ ^ Module.finrank K L = 1 →
      ζ ∈ Set.range (algebraMap K L))
    (F : IntermediateField K L) :
    ∃ β : F,
      (β : L) = α ^ Module.finrank F L ∧
        β ^ Module.finrank K F = algebraMap K F π ∧
          IntermediateField.adjoin K ({(β : L)} : Set L) = F ∧
            Module.finrank K F * Module.finrank F L =
              Module.finrank K L
theorem

exists_intermediateField_generator_pow_eq_of_henselian_pureRadical

L71 ↗
EtaleFundamentalGroups.Kummer.exists_intermediateField_generator_pow_eq_of_henselian_pureRadical
Documentation

Henselian integral-model source for the concrete intermediate-field generator. The roots-of-unity condition is derived from the normal local model and the residue-field equivalence.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v w x
Lean source · statement
theorem exists_intermediateField_generator_pow_eq_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) (π : K)
    (hpow : α ^ Module.finrank K L = 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) :
    ∃ β : F,
      (β : L) = α ^ Module.finrank F L ∧
        β ^ Module.finrank K F = algebraMap K F π ∧
          IntermediateField.adjoin K ({(β : L)} : Set L) = F ∧
            Module.finrank K F * Module.finrank F L =
              Module.finrank K L

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