Module

FrobeniusFixedFieldAction.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FrobeniusFixedFieldAction

8 declarations indexed from sourceView source ↗

Module documentation

Actions on Frobenius fixed fields

This module defines the action induced on a Frobenius fixed field and proves its compatibility with conjugate-stable actions, relative norms, inclusions, and Frobenius power sums.

Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same universe; IntegralRepGroupType names that shared boundary.

Imports2

Imported by3

def

frobeniusFixedFieldAction

L44 ↗

ClassFormation.DegreeData.frobeniusFixedFieldAction

Documentation

The action on a Frobenius fixed field induced by an element commuting with its defining generator.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def frobeniusFixedFieldAction (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q) :
    ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ) →+
      ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ)

theorem

frobeniusFixedFieldAction_coe

L88 ↗

ClassFormation.DegreeData.frobeniusFixedFieldAction_coe

Documentation

The fixed-field action has the expected ambient automorphism after coercion.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusFixedFieldAction_coe (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    (a : ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ)) :
    ((D.frobeniusFixedFieldAction A K L hLK σ q hq a :
      ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ)) : A.V) =
      A.ρ (Quotient.out q).1 a.1

theorem

frobeniusFixedFieldAction_coe_of_mk

L104 ↗

ClassFormation.DegreeData.frobeniusFixedFieldAction_coe_of_mk

Documentation

On a quotient representative, the fixed-field action coerces to the represented action.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusFixedFieldAction_coe_of_mk (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    (k : K.field.toSubgroup) (hkq : QuotientGroup.mk k = q)
    (a : ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ)) :
    ((D.frobeniusFixedFieldAction A K L hLK σ q hq a :
      ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ)) : A.V) =
      A.ρ k.1 a.1

theorem

frobeniusFixedFieldAction_eq_conjugateStableAction

L141 ↗

ClassFormation.DegreeData.frobeniusFixedFieldAction_eq_conjugateStableAction

Documentation

The fixed-field action coincides with the conjugation-stable action.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · full declaration

theorem frobeniusFixedFieldAction_eq_conjugateStableAction
    (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    (a : ambientFixedAddSubgroup A (D.frobeniusFixedField K L hLK σ)) :
    let k : K.field.toSubgroup := Quotient.out q
    let hstable : conjugateClosedSubgroup
        (D.frobeniusFixedField K L hLK σ) k.1⁻¹ =
      D.frobeniusFixedField K L hLK σ :=
      D.conjugate_frobeniusFixedField_eq_of_commutes K L hLK σ q hq
    D.frobeniusFixedFieldAction A K L hLK σ q hq a =
      conjugateStableAction A (D.frobeniusFixedField K L hLK σ)
        k.1⁻¹ hstable a := by
  dsimp only
  apply Subtype.ext
  rw [D.frobeniusFixedFieldAction_coe, conjugateStableAction_coe]
  simp

theorem

relativeNorm_frobeniusFixedFieldAction

L167 ↗

ClassFormation.DegreeData.relativeNorm_frobeniusFixedFieldAction

Documentation

Relative norm in a power-fixed-field tower is equivariant for every quotient element commuting with both defining powers.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem relativeNorm_frobeniusFixedFieldAction (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ σ' : D.FrobeniusElements K L hLK)
    (hTS : (D.frobeniusFixedField K L hLK σ').toSubgroup ≤
      (D.frobeniusFixedField K L hLK σ).toSubgroup)
    [Finite ((D.frobeniusFixedField K L hLK σ).toSubgroup ⧸
      extensionSubgroup (D.frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedField K L hLK σ') hTS)]
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    (hq' : q * σ'.1 = σ'.1 * q)
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ')) :
    relativeNorm A (D.frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedField K L hLK σ') hTS
        (D.frobeniusFixedFieldAction A K L hLK σ' q hq' a) =
      D.frobeniusFixedFieldAction A K L hLK σ q hq
        (relativeNorm A (D.frobeniusFixedField K L hLK σ)
          (D.frobeniusFixedField K L hLK σ') hTS a)

theorem

frobeniusFixedFieldAction_inclusion

L203 ↗

ClassFormation.DegreeData.frobeniusFixedFieldAction_inclusion

Documentation

Inclusion of a stabilized Frobenius fixed field intertwines its action with the actual quotient action on the maximal unramified field.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusFixedFieldAction_inclusion (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ)) :
    fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
        (D.maximalUnramifiedField L)
        (D.fieldInertia_le_frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedFieldAction A K L hLK σ q hq a) =
      D.frobeniusQuotientAction A K.field L hLK q
        (fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
          (D.maximalUnramifiedField L)
          (D.fieldInertia_le_frobeniusFixedField K L hLK σ) a)

theorem

fixedFieldPowerSum_relativeNorm

L242 ↗

ClassFormation.DegreeData.fixedFieldPowerSum_relativeNorm

Documentation

A Frobenius power sum commutes with the relative norm in a fixed-field tower whenever the quotient element stabilizes both fields.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem fixedFieldPowerSum_relativeNorm (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ σ' : D.FrobeniusElements K L hLK)
    (hTS : (D.frobeniusFixedField K L hLK σ').toSubgroup ≤
      (D.frobeniusFixedField K L hLK σ).toSubgroup)
    [Finite ((D.frobeniusFixedField K L hLK σ).toSubgroup ⧸
      extensionSubgroup (D.frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedField K L hLK σ') hTS)]
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q) (hq' : q * σ'.1 = σ'.1 * q)
    (n : ℕ)
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ')) :
    relativeNorm A (D.frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedField K L hLK σ') hTS
        (∑ i : Fin n,
          D.frobeniusFixedFieldAction A K L hLK σ'
            (q ^ i.1) (Commute.pow_left hq' i.1) a) =
      ∑ i : Fin n,
        D.frobeniusFixedFieldAction A K L hLK σ
          (q ^ i.1) (Commute.pow_left hq i.1)
          (relativeNorm A (D.frobeniusFixedField K L hLK σ)
            (D.frobeniusFixedField K L hLK σ') hTS a)

theorem

fixedFieldPowerSum_inclusion

L278 ↗

ClassFormation.DegreeData.fixedFieldPowerSum_inclusion

Documentation

The fixed-field power sum becomes the global Frobenius power sum after inclusion into the maximal unramified field.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section fixedFieldActions
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem fixedFieldPowerSum_inclusion (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q) (n : ℕ)
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ)) :
    fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
        (D.maximalUnramifiedField L)
        (D.fieldInertia_le_frobeniusFixedField K L hLK σ)
        (∑ i : Fin n,
          D.frobeniusFixedFieldAction A K L hLK σ
            (q ^ i.1) (Commute.pow_left hq i.1) a) =
      D.frobeniusPowerSum A K.field L hLK q n
        (fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
          (D.maximalUnramifiedField L)
          (D.fieldInertia_le_frobeniusFixedField K L hLK σ) a)

Module documentation

Actions on Frobenius fixed fields

Declarations