NYLL
Module

PrimeToCyclotomicTower.lean

Nyll.GaloisCohomology.Kummer.Concrete.PrimeToCyclotomicTower
2 declarations indexed from sourceView source ↗

Module documentation

A prime-to-p cyclotomic tower and its actual restriction kernel

Start with a prime-degree Galois extension M/F, and adjoin the p-th roots of unity to M. When the two primes differ, the resulting extension over F is finite Galois with order coprime to p. This uses the tower law and normality of the cyclotomic tower, without linear disjointness.

The cyclotomic field can be supplied by the existing exists_cyclotomic_intermediateField M Ω p. Its composite F-algebra and the F/M/E scalar tower are fixed by the caller once. No extra field, valuation, finiteness, or comparison input is needed in this boundary.

Imports11
Imported by3

Declarations

theorem

primeTo_cyclotomic_tower_data

L45 ↗
KummerTheory.primeTo_cyclotomic_tower_data
Documentation

The actual cyclotomic tower over a prime-degree Galois extension is finite Galois of order prime to p, and restriction to the lower extension is surjective. Finiteness of the lower extension is generated by its degree.

Source context 4 commands

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

namespace KummerTheory
open ValuationTheory.DiscreteValuationField
universe u v w
variable (F : Type u) (M : Type v) (E : Type w) [Field F] [Field M] [Field E]
  [Algebra F M] [Algebra F E] [Algebra M E] [IsScalarTower F M E]
Lean source · statement
theorem primeTo_cyclotomic_tower_data
    [IsGalois F M] (p r : ℕ) [Fact p.Prime] [Fact r.Prime]
    [IsCyclotomicExtension {p} M E]
    (hrp : r ≠ p) (hdegree : Module.finrank F M = r) :
    FiniteDimensional F E ∧ IsGalois F E ∧
      p.Coprime (Nat.card Gal(E/F)) ∧
        Function.Surjective (AlgEquiv.restrictNormalHom M : Gal(E/F) →* Gal(M/F))
theorem

restrictScalarsHom_range_eq_normalRestrictionKer

L75 ↗
KummerTheory.restrictScalarsHom_range_eq_normalRestrictionKer
Documentation

The image of actual scalar restriction is exactly the kernel of actual restriction to M. Thus this image is normal, with no comparison assumption; the automorphism in the kernel itself supplies the M-linear representative.

Source context 4 commands

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

namespace KummerTheory
open ValuationTheory.DiscreteValuationField
universe u v w
variable (F : Type u) (M : Type v) (E : Type w) [Field F] [Field M] [Field E]
  [Algebra F M] [Algebra F E] [Algebra M E] [IsScalarTower F M E]
Lean source · statement
theorem restrictScalarsHom_range_eq_normalRestrictionKer [Normal F M] :
    (AlgEquiv.restrictScalarsHom F : Gal(E/M) →* Gal(E/F)).range =
      (AlgEquiv.restrictNormalHom M : Gal(E/F) →* Gal(M/F)).ker

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