Module

FrobeniusFixedFieldTower.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FrobeniusFixedFieldTower

27 declarations indexed from sourceView source ↗

Module documentation

Bundles finite towers of Frobenius fixed fields together with the normality and finiteness data needed for norm and unit calculations.

Imports2

Imported by2

def

FrobeniusFixedFieldTower

L53 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower

Documentation

A finite normal tower between two Frobenius fixed fields.

The ambient Galois extension, both Frobenius elements, the fixed-field inclusion, and exactly the finiteness hypotheses needed by the unit representation are stored once. In particular, downstream statements no longer re-thread the proof-dependent subgroup inclusions and quotient instances independently.

Source context 7 commands

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

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

Lean source · full declaration

structure FrobeniusFixedFieldTower
    (D : DegreeData G) [IsTopologicalGroup G] where
  /-- The finite-residue field in which the ambient Galois extension begins. -/
  ambientBase : DegreeData.FiniteResidueAbstractField D
  /-- The ambient Galois subextension. -/
  ambient : GaloisSubextension ambientBase.field
  /-- The Frobenius element whose fixed field is the base of the tower. -/
  baseFrobenius :
    D.FrobeniusElements ambientBase ambient.field ambient.below
  /-- The Frobenius element whose fixed field is the top of the tower. -/
  fieldFrobenius :
    D.FrobeniusElements ambientBase ambient.field ambient.below
  /-- Inclusion of the top fixed field into the base fixed field. -/
  field_le_base :
    (D.frobeniusFixedField ambientBase ambient.field ambient.below
        fieldFrobenius).toSubgroup ≤
      (D.frobeniusFixedField ambientBase ambient.field ambient.below
        baseFrobenius).toSubgroup
  /-- The relative quotient between the two fixed fields is finite. -/
  finiteQuotient :
    Finite
      ((D.frobeniusFixedField ambientBase ambient.field ambient.below
          baseFrobenius).toSubgroup ⧸
        extensionSubgroup
          (D.frobeniusFixedField ambientBase ambient.field ambient.below
            baseFrobenius)
          (D.frobeniusFixedField ambientBase ambient.field ambient.below
            fieldFrobenius)
          field_le_base)
  /-- The base fixed field is finite over the distinguished base. -/
  baseAbsoluteFinite :
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField ambientBase ambient.field ambient.below
            baseFrobenius)
          (le_baseField
            (D.frobeniusFixedField ambientBase ambient.field ambient.below
              baseFrobenius)))
  /-- The top fixed field is finite over the distinguished base. -/
  fieldAbsoluteFinite :
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField ambientBase ambient.field ambient.below
            fieldFrobenius)
          (le_baseField
            (D.frobeniusFixedField ambientBase ambient.field ambient.below
              fieldFrobenius)))
  /-- The relative subgroup between the fixed fields is normal. -/
  normal :
    (extensionSubgroup
      (D.frobeniusFixedField ambientBase ambient.field ambient.below
        baseFrobenius)
      (D.frobeniusFixedField ambientBase ambient.field ambient.below
        fieldFrobenius)
      field_le_base).Normal
  /-- The two chosen ambient Frobenius elements commute. -/
  commute :
    baseFrobenius.1 * fieldFrobenius.1 =
      fieldFrobenius.1 * baseFrobenius.1

def

base

L120 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.base

Documentation

The lower fixed field, finite over the distinguished base.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

def base (T : FrobeniusFixedFieldTower D) :
    FiniteAbstractField G

def

field

L135 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.field

Documentation

The upper fixed field, finite over the distinguished base.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

def field (T : FrobeniusFixedFieldTower D) :
    FiniteAbstractField G

def

toGaloisSubextension

L150 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.toGaloisSubextension

Documentation

The fixed-field inclusion as a bundled Galois subextension.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · full declaration

def toGaloisSubextension (T : FrobeniusFixedFieldTower D) :
    GaloisSubextension T.base.field where
  field := T.field.field
  below := T.field_le_base
  normal := T.normal

def

extension

L157 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.extension

Documentation

The finite extension between the two bundled fixed fields.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · full declaration

def extension (T : FrobeniusFixedFieldTower D) :
    FiniteAbstractFieldExtension G where
  field := T.field
  base := T.base
  below := T.field_le_base
  finiteQuotient := T.finiteQuotient

structure

Representative

L165 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.Representative

Documentation

A concrete lower-fixed-field element representing its Frobenius class.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · full declaration

structure Representative (T : FrobeniusFixedFieldTower D) where
  /-- The chosen element in the base fixed-field subgroup. -/
  element : T.extension.base.field.toSubgroup
  /-- The chosen element maps to the prescribed ambient Frobenius class. -/
  mapsToFrobenius :
    D.frobeniusFixedFieldToClosure T.ambientBase T.ambient.field
        T.ambient.below T.baseFrobenius element =
      D.frobeniusInClosure T.ambientBase T.ambient.field
        T.ambient.below T.baseFrobenius

instance

extensionNormal

L176 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.extensionNormal

Documentation

The extension subgroup of a bundled Frobenius fixed-field tower is normal.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance extensionNormal (T : FrobeniusFixedFieldTower D) :
    (extensionSubgroup T.extension.base.field T.extension.field.field
      T.extension.below).Normal

structure

CyclicGenerator

L182 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.CyclicGenerator

Documentation

A representative which generates the finite fixed-field quotient.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · full declaration

structure CyclicGenerator (T : FrobeniusFixedFieldTower D)
    extends Representative T where
  /-- Every relative Galois element is a power of the representative's class. -/
  generates :
    ∀ x :
      T.extension.base.field.toSubgroup ⧸
        extensionSubgroup T.extension.base.field T.extension.field.field
          T.extension.below,
      x ∈ Subgroup.zpowers (QuotientGroup.mk toRepresentative.element)

instance

extensionFinite

L193 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.extensionFinite

Documentation

The Galois quotient of a bundled Frobenius fixed-field extension is finite.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance extensionFinite (T : FrobeniusFixedFieldTower D) :
    Finite
      (T.extension.base.field.toSubgroup ⧸
        extensionSubgroup T.extension.base.field T.extension.field.field
          T.extension.below)

instance

baseAbsoluteFiniteInstance

L201 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.baseAbsoluteFiniteInstance

Documentation

The lower Frobenius fixed field in the tower is finite over the distinguished base field.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance baseAbsoluteFiniteInstance (T : FrobeniusFixedFieldTower D) :
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField T.ambientBase T.ambient.field T.ambient.below
            T.baseFrobenius)
          (le_baseField
            (D.frobeniusFixedField T.ambientBase T.ambient.field T.ambient.below
              T.baseFrobenius)))

instance

fieldAbsoluteFiniteInstance

L213 ↗

ClassFormation.DegreeData.FrobeniusFixedFieldTower.fieldAbsoluteFiniteInstance

Documentation

The upper Frobenius fixed field in the tower is finite over the distinguished base field.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance fieldAbsoluteFiniteInstance (T : FrobeniusFixedFieldTower D) :
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField T.ambientBase T.ambient.field T.ambient.below
            T.fieldFrobenius)
          (le_baseField
            (D.frobeniusFixedField T.ambientBase T.ambient.field T.ambient.below
              T.fieldFrobenius)))

structure

FiniteAmbientFrobeniusFixedFieldTower

L229 ↗

ClassFormation.DegreeData.FiniteAmbientFrobeniusFixedFieldTower

Documentation

A Frobenius fixed-field tower whose ambient Galois extension is finite. The additional finiteness is stored on the opaque quotient object exposed by GaloisSubextension.

Source context 7 commands

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

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

Lean source · full declaration

structure FiniteAmbientFrobeniusFixedFieldTower
    (D : DegreeData G) [IsTopologicalGroup G]
    extends FrobeniusFixedFieldTower D where
  /-- The ambient Galois quotient is finite. -/
  ambientFinite : Finite toFrobeniusFixedFieldTower.ambient.extensionQuotient

instance

ambientQuotientFinite

L242 ↗

ClassFormation.DegreeData.FiniteAmbientFrobeniusFixedFieldTower.ambientQuotientFinite

Documentation

The ambient Galois quotient stored in a finite Frobenius fixed-field tower is finite.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAmbientFrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance ambientQuotientFinite
    (T : FiniteAmbientFrobeniusFixedFieldTower D) :
    Finite T.ambient.extensionQuotient

instance

ambientRepresentedQuotientFinite

L249 ↗

ClassFormation.DegreeData.FiniteAmbientFrobeniusFixedFieldTower.ambientRepresentedQuotientFinite

Documentation

Finiteness transported to the quotient presentation required by the underlying Frobenius calculations.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FiniteAmbientFrobeniusFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance ambientRepresentedQuotientFinite
    (T : FiniteAmbientFrobeniusFixedFieldTower D) :
    Finite
      (T.ambientBase.field.toSubgroup ⧸
        extensionSubgroup T.ambientBase.field T.ambient.field
          T.ambient.below)

structure

FrobeniusPowerFixedFieldTower

L267 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower

Documentation

The power tower fixed by φⁿ² ≤ φⁿ.

Only data already required by the universal norm-descent construction is stored: the finite ambient Galois extension, a degree-one Frobenius, its positive exponent, and the three fixed-field finiteness witnesses. The fixed-field inclusion, normality, and commutation relation are consequences of the power construction.

Source context 7 commands

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

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

Lean source · full declaration

structure FrobeniusPowerFixedFieldTower
    (D : DegreeData G) [IsTopologicalGroup G] where
  /-- The finite-residue field at the base of the ambient extension. -/
  ambientBase : DegreeData.FiniteResidueAbstractField D
  /-- The finite ambient Galois subextension. -/
  ambient : FiniteGaloisSubextension ambientBase.field
  /-- A chosen degree-one Frobenius element in the ambient extension. -/
  frobenius :
    D.FrobeniusElements ambientBase ambient.field ambient.below
  /-- The chosen Frobenius has exponent one. -/
  exponent_one :
    D.frobeniusExponent ambientBase ambient.field ambient.below frobenius = 1
  /-- The positive exponent defining the first fixed field. -/
  n : ℕ
  /-- Positivity of the fixed-field exponent. -/
  n_pos : 0 < n
  /-- The fixed field of the `n`-th Frobenius power is finite over the distinguished base. -/
  baseAbsoluteFinite :
    let σ := D.frobeniusPowerOfDegreeOne ambientBase ambient.field
      ambient.below frobenius exponent_one n n_pos
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField ambientBase ambient.field ambient.below σ)
          (le_baseField
            (D.frobeniusFixedField ambientBase ambient.field ambient.below σ)))
  /-- The fixed field of the `n²`-th Frobenius power is finite over the distinguished base. -/
  fieldAbsoluteFinite :
    let σn := D.frobeniusPowerOfDegreeOne ambientBase ambient.field
      ambient.below frobenius exponent_one (n * n) (Nat.mul_pos n_pos n_pos)
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField ambientBase ambient.field ambient.below σn)
          (le_baseField
            (D.frobeniusFixedField ambientBase ambient.field ambient.below σn)))
  /-- The relative quotient between the `n`- and `n²`-power fixed fields is finite. -/
  relativeFinite :
    let σ := D.frobeniusPowerOfDegreeOne ambientBase ambient.field
      ambient.below frobenius exponent_one n n_pos
    let σn := D.frobeniusPowerOfDegreeOne ambientBase ambient.field
      ambient.below frobenius exponent_one (n * n) (Nat.mul_pos n_pos n_pos)
    let hTS := D.frobeniusPowerFixedField_le ambientBase ambient.field
      ambient.below frobenius exponent_one n n n_pos n_pos
    Finite
      ((D.frobeniusFixedField ambientBase ambient.field ambient.below σ).toSubgroup ⧸
        extensionSubgroup
          (D.frobeniusFixedField ambientBase ambient.field ambient.below σ)
          (D.frobeniusFixedField ambientBase ambient.field ambient.below σn)
          hTS)

def

ambientGalois

L323 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.ambientGalois

Documentation

Forget ambient finiteness while retaining its Galois structure.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

def ambientGalois (P : FrobeniusPowerFixedFieldTower D) :
    GaloisSubextension P.ambientBase.field

def

baseFrobenius

L328 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.baseFrobenius

Documentation

The Frobenius element φⁿ defining the lower fixed field.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

def baseFrobenius (P : FrobeniusPowerFixedFieldTower D) :
    D.FrobeniusElements P.ambientBase P.ambient.field P.ambient.below

def

fieldFrobenius

L334 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.fieldFrobenius

Documentation

The Frobenius element φⁿ² defining the upper fixed field.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

def fieldFrobenius (P : FrobeniusPowerFixedFieldTower D) :
    D.FrobeniusElements P.ambientBase P.ambient.field P.ambient.below

theorem

frobenius_commute_base

L341 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.frobenius_commute_base

Documentation

The original Frobenius commutes with its n-th power.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

theorem frobenius_commute_base (P : FrobeniusPowerFixedFieldTower D) :
    P.frobenius.1 * P.baseFrobenius.1 =
      P.baseFrobenius.1 * P.frobenius.1

theorem

frobenius_commute_field

L348 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.frobenius_commute_field

Documentation

The original Frobenius commutes with its n²-th power.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

theorem frobenius_commute_field (P : FrobeniusPowerFixedFieldTower D) :
    P.frobenius.1 * P.fieldFrobenius.1 =
      P.fieldFrobenius.1 * P.frobenius.1

theorem

field_le_base

L355 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.field_le_base

Documentation

Inclusion of the field fixed by φⁿ² into the field fixed by φⁿ.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

theorem field_le_base (P : FrobeniusPowerFixedFieldTower D) :
    (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
        P.fieldFrobenius).toSubgroup ≤
      (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
        P.baseFrobenius).toSubgroup

instance

relativeRepresentedQuotientFinite

L366 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.relativeRepresentedQuotientFinite

Documentation

Relative finiteness in the fixed-field presentation used by the Frobenius action and norm lemmas. The witness is projected from the power tower rather than requested again from callers.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance relativeRepresentedQuotientFinite
    (P : FrobeniusPowerFixedFieldTower D) :
    Finite
      ((D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
          P.baseFrobenius).toSubgroup ⧸
        extensionSubgroup
          (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
            P.baseFrobenius)
          (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
            P.fieldFrobenius)
          P.field_le_base)

instance

baseRepresentedAbsoluteFinite

L381 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.baseRepresentedAbsoluteFinite

Documentation

Absolute finiteness of the lower fixed field in the presentation used by the Frobenius action API.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance baseRepresentedAbsoluteFinite
    (P : FrobeniusPowerFixedFieldTower D) :
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
            P.baseFrobenius)
          (le_baseField
            (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
              P.baseFrobenius)))

instance

fieldRepresentedAbsoluteFinite

L395 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.fieldRepresentedAbsoluteFinite

Documentation

Absolute finiteness of the upper fixed field in the presentation used by the Frobenius action API.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · statement

instance fieldRepresentedAbsoluteFinite
    (P : FrobeniusPowerFixedFieldTower D) :
    Finite
      ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
            P.fieldFrobenius)
          (le_baseField
            (D.frobeniusFixedField P.ambientBase P.ambient.field P.ambient.below
              P.fieldFrobenius)))

def

toFrobeniusFixedFieldTower

L408 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.toFrobeniusFixedFieldTower

Documentation

The power construction as the canonical fixed-field tower bundle.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · full declaration

def toFrobeniusFixedFieldTower
    (P : FrobeniusPowerFixedFieldTower D) [T2Space G] :
    FrobeniusFixedFieldTower D where
  ambientBase := P.ambientBase
  ambient := P.ambientGalois
  baseFrobenius := P.baseFrobenius
  fieldFrobenius := P.fieldFrobenius
  field_le_base := P.field_le_base
  finiteQuotient := P.relativeFinite
  baseAbsoluteFinite := P.baseAbsoluteFinite
  fieldAbsoluteFinite := P.fieldAbsoluteFinite
  normal :=
    D.frobeniusPowerFixedField_normal P.ambientBase P.ambient.field
      P.ambient.below P.frobenius P.exponent_one P.n P.n P.n_pos P.n_pos
  commute := by
    change P.baseFrobenius.1 * P.fieldFrobenius.1 =
      P.fieldFrobenius.1 * P.baseFrobenius.1
    simpa [baseFrobenius, fieldFrobenius] using
      ((Commute.refl P.frobenius.1).pow_pow P.n (P.n * P.n)).eq

def

toFiniteAmbientFrobeniusFixedFieldTower

L430 ↗

ClassFormation.DegreeData.FrobeniusPowerFixedFieldTower.toFiniteAmbientFrobeniusFixedFieldTower

Documentation

The power tower together with the already assumed finiteness of its ambient extension.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
namespace FrobeniusPowerFixedFieldTower
variable {D : DegreeData G} [IsTopologicalGroup G]

Lean source · full declaration

def toFiniteAmbientFrobeniusFixedFieldTower
    (P : FrobeniusPowerFixedFieldTower D) [T2Space G] :
    FiniteAmbientFrobeniusFixedFieldTower D where
  toFrobeniusFixedFieldTower := P.toFrobeniusFixedFieldTower
  ambientFinite := by
    change Finite P.ambient.toGaloisSubextension.extensionQuotient
    exact Finite.of_equiv P.ambient.extensionQuotient
      P.ambient.toGaloisExtensionQuotientMulEquiv

Module documentation

Declarations