Module

FrobeniusLift.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.TotallyRamifiedCase.FrobeniusLift

13 declarations indexed from sourceView source ↗

Module documentation

Frobenius lifts for totally ramified extensions

This file constructs degree-one Frobenius lifts and the finite auxiliary Galois extension used in the totally ramified reciprocity argument.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Reduction

Imported by3

theorem

exists_degreeOneFrobeniusLiftOfTotallyRamified

L32 ↗

ClassFormation.DegreeData.exists_degreeOneFrobeniusLiftOfTotallyRamified

Documentation

Every automorphism of a totally ramified Galois extension has a Frobenius lift of exponent one.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem exists_degreeOneFrobeniusLiftOfTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : GaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    ∃ σ : D.FrobeniusElements K L.field L.below,
      D.frobeniusExponent K L.field L.below σ = 1 ∧
      L.extensionQuotientMulEquiv.symm
        (D.frobeniusRestriction K L.field L.below σ) = q

def

chosenDegreeOneFrobeniusLiftOfTotallyRamified

L116 ↗

ClassFormation.DegreeData.chosenDegreeOneFrobeniusLiftOfTotallyRamified

Documentation

In a totally ramified finite Galois extension every finite automorphism has a degree-one Frobenius lift. This is the element denoted \tilde\sigma = \sigma\varphi_L.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def chosenDegreeOneFrobeniusLiftOfTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : GaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    D.FrobeniusElements K L.field L.below

theorem

frobeniusExponent_chosenDegreeOneFrobeniusLiftOfTotallyRamified

L127 ↗

ClassFormation.DegreeData.frobeniusExponent_chosenDegreeOneFrobeniusLiftOfTotallyRamified

Documentation

The chosen Frobenius lift for a totally ramified extension has exponent one.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusExponent_chosenDegreeOneFrobeniusLiftOfTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : GaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    D.frobeniusExponent K L.field L.below
      (D.chosenDegreeOneFrobeniusLiftOfTotallyRamified
        K L hTot q) = 1

theorem

frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfTotallyRamified

L140 ↗

ClassFormation.DegreeData.frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfTotallyRamified

Documentation

The chosen degree-one Frobenius lift restricts to the prescribed automorphism.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : GaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    L.extensionQuotientMulEquiv.symm
        (D.frobeniusRestriction K L.field L.below
          (D.chosenDegreeOneFrobeniusLiftOfTotallyRamified
            K L hTot q)) = q

theorem

frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfTotallyRamified_underlying

L153 ↗

ClassFormation.DegreeData.frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfTotallyRamified_underlying

Documentation

Underlying quotient form of the Galois-bundle restriction theorem.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfTotallyRamified_underlying
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : GaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    D.frobeniusRestriction K L.field L.below
        (D.chosenDegreeOneFrobeniusLiftOfTotallyRamified
          K L hTot q) =
      L.extensionQuotientMulEquiv q

def

chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified

L169 ↗

ClassFormation.DegreeData.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified

Documentation

The degree-one lift specialized to a bundled finite Galois extension. The conversion to the non-finite Galois boundary and the quotient comparison are performed once in this definition.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    D.FrobeniusElements K L.field L.below

theorem

frobeniusExponent_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified

L182 ↗

ClassFormation.DegreeData.frobeniusExponent_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified

Documentation

The finite totally ramified Frobenius lift has exponent one.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusExponent_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    D.frobeniusExponent K L.field L.below
      (D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
        K L hTot q) = 1

theorem

frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified

L197 ↗

ClassFormation.DegreeData.frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified

Documentation

The finite totally ramified Frobenius lift restricts to the chosen automorphism.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    L.extensionQuotientMulEquiv.symm
        (D.frobeniusRestriction K L.field L.below
          (D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
            K L hTot q)) = q

theorem

frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified_underlying

L222 ↗

ClassFormation.DegreeData.frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified_underlying

Documentation

Underlying quotient form of the preceding finite-bundle theorem.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusRestriction_chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified_underlying
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    D.frobeniusRestriction K L.field L.below
        (D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
          K L hTot q) =
      L.extensionQuotientMulEquiv q

def

abstractReciprocityTotallyRamifiedFiniteGaloisExtension

L239 ↗

ClassFormation.DegreeData.abstractReciprocityTotallyRamifiedFiniteGaloisExtension

Documentation

The finite Galois extension M / K chosen. It contains both L and the degree-one Frobenius fixed field Σ, and is contained in the maximal unramified extension of L.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def abstractReciprocityTotallyRamifiedFiniteGaloisExtension
    (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    FiniteGaloisSubextension K.field

theorem

abstractReciprocityTotallyRamifiedFiniteGaloisExtension_le_L

L266 ↗

ClassFormation.DegreeData.abstractReciprocityTotallyRamifiedFiniteGaloisExtension_le_L

Documentation

The auxiliary reciprocity extension lies below the given totally ramified extension.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem abstractReciprocityTotallyRamifiedFiniteGaloisExtension_le_L
    (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    (D.abstractReciprocityTotallyRamifiedFiniteGaloisExtension
      K L hTot q).field.toSubgroup ≤ L.field.toSubgroup

theorem

abstractReciprocityTotallyRamifiedFiniteGaloisExtension_le_sigma

L290 ↗

ClassFormation.DegreeData.abstractReciprocityTotallyRamifiedFiniteGaloisExtension_le_sigma

Documentation

The auxiliary reciprocity extension is fixed by the selected automorphism.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem abstractReciprocityTotallyRamifiedFiniteGaloisExtension_le_sigma
    (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    (D.abstractReciprocityTotallyRamifiedFiniteGaloisExtension
      K L hTot q).field.toSubgroup ≤
      (D.frobeniusFixedField K L.field L.below
        (D.chosenDegreeOneFrobeniusLiftOfFiniteTotallyRamified
          K L hTot q)).toSubgroup

theorem

maximalUnramifiedField_le_abstractReciprocityTotallyRamifiedFiniteGaloisExtension

L318 ↗

ClassFormation.DegreeData.maximalUnramifiedField_le_abstractReciprocityTotallyRamifiedFiniteGaloisExtension

Documentation

The maximal unramified field lies below the auxiliary totally ramified reciprocity field.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem maximalUnramifiedField_le_abstractReciprocityTotallyRamifiedFiniteGaloisExtension
    (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hTot : L.IsTotallyRamified D)
    (q : L.extensionQuotient) :
    (D.maximalUnramifiedField L.field).toSubgroup ≤
      (D.abstractReciprocityTotallyRamifiedFiniteGaloisExtension
        K L hTot q).field.toSubgroup

Module documentation

Frobenius lifts for totally ramified extensions

Declarations