Module

FrobeniusQuotientDescent.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FrobeniusQuotientDescent

13 declarations indexed from sourceView source ↗

Module documentation

Frobenius quotient descent

This module constructs the Frobenius quotient representation, identifies its Birkhoff sums with Frobenius power sums, and proves the finite-support descent from the maximal unramified field.

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

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.UniversalNormDescent

Imported by3

theorem

frobeniusQuotientAction_coe_out

L43 ↗

ClassFormation.DegreeData.frobeniusQuotientAction_coe_out

Documentation

Underlying coefficient of the actual quotient action, expressed through the chosen quotient representative.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusQuotientAction_coe_out (D : DegreeData G) (A : Rep ℤ G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (q : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    (D.frobeniusQuotientAction A K L hLK q a).1 =
      A.ρ (Quotient.out q).1 a.1

def

frobeniusQuotientActionLinearMap

L64 ↗

ClassFormation.DegreeData.frobeniusQuotientActionLinearMap

Documentation

The linear action of G(\widetilde L/K) on A_{\widetilde L}. This packages the concrete quotient action from the Frobenius norm-identity lemma in the form needed by the Tate-cohomology calculation.

Source context 10 commands

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

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

Lean source · full declaration

def frobeniusQuotientActionLinearMap (D : DegreeData G)
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (q : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK) :
    ambientFixedAddSubgroup A (D.maximalUnramifiedField L) →ₗ[ℤ]
      ambientFixedAddSubgroup A (D.maximalUnramifiedField L) where
  toFun := D.frobeniusQuotientAction A K L hLK q
  map_add' a b := by
    refine Quotient.inductionOn' q ?_
    intro k
    apply Subtype.ext
    change A.ρ k.1 (a.1 + b.1) = A.ρ k.1 a.1 + A.ρ k.1 b.1
    exact map_add (A.ρ k.1) _ _
  map_smul' n a := by
    refine Quotient.inductionOn' q ?_
    intro k
    apply Subtype.ext
    change A.ρ k.1 (n • a.1) = n • A.ρ k.1 a.1
    exact map_zsmul (A.ρ k.1) n a.1

def

frobeniusQuotientRepresentation

L87 ↗

ClassFormation.DegreeData.frobeniusQuotientRepresentation

Documentation

The actual G(\widetilde L/K)-representation on A_{\widetilde L} used in the universal norm-descent lemma.

Source context 10 commands

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

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

Lean source · statement

def frobeniusQuotientRepresentation (D : DegreeData G)
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    Rep ℤ (K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)

theorem

frobeniusQuotientRepresentation_apply

L109 ↗

ClassFormation.DegreeData.frobeniusQuotientRepresentation_apply

Documentation

The Frobenius quotient representation evaluates by the chosen quotient action.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusQuotientRepresentation_apply (D : DegreeData G)
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (q : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    (D.frobeniusQuotientRepresentation A K L hLK).ρ q a =
      D.frobeniusQuotientAction A K L hLK q a

theorem

birkhoffSum_eq_frobeniusPowerSum

L120 ↗

ClassFormation.DegreeData.birkhoffSum_eq_frobeniusPowerSum

Documentation

The Birkhoff sum of the quotient action is the corresponding sum of Frobenius powers.

Source context 10 commands

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

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

Lean source · statement

theorem birkhoffSum_eq_frobeniusPowerSum (D : DegreeData G)
    (A : Rep ℤ G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (φ : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK) (n : ℕ)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    birkhoffSum
        ((D.frobeniusQuotientRepresentation A K L hLK).ρ φ) id n a =
      D.frobeniusPowerSum A K L hLK φ n a

theorem

frobeniusPowerSum_add

L139 ↗

ClassFormation.DegreeData.frobeniusPowerSum_add

Documentation

A Frobenius power sum splits into its first n terms and a translated block of m terms.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusPowerSum_add (D : DegreeData G) (A : Rep ℤ G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (φ : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
    (n m : ℕ)
    (x : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    D.frobeniusPowerSum A K L hLK φ (n + m) x =
      D.frobeniusPowerSum A K L hLK φ n x +
        D.frobeniusPowerSum A K L hLK φ m
          (D.frobeniusQuotientAction A K L hLK (φ ^ n) x)

theorem

frobeniusPowerSum_action_sub

L167 ↗

ClassFormation.DegreeData.frobeniusPowerSum_action_sub

Documentation

Actual additive telescoping identity for the Frobenius power sum.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusPowerSum_action_sub (D : DegreeData G)
    (A : Rep ℤ G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (φ : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK) (n : ℕ)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    D.frobeniusQuotientAction A K L hLK φ
        (D.frobeniusPowerSum A K L hLK φ n a) -
        D.frobeniusPowerSum A K L hLK φ n a =
      D.frobeniusQuotientAction A K L hLK (φ ^ n) a - a

theorem

frobeniusPowerSum_sub_universalNormDescent

L204 ↗

ClassFormation.DegreeData.frobeniusPowerSum_sub_universalNormDescent

Documentation

The difference of Frobenius power sums is represented by universal norm descent.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusPowerSum_sub_universalNormDescent (D : DegreeData G) (A : Rep ℤ G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (φ : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
    (n : ℕ)
    (x y : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    D.frobeniusPowerSum A K L hLK φ n (x - y) =
      D.frobeniusPowerSum A K L hLK φ n x -
        D.frobeniusPowerSum A K L hLK φ n y

theorem

frobeniusPowerSum_eq_nsmul_of_fixed

L225 ↗

ClassFormation.DegreeData.frobeniusPowerSum_eq_nsmul_of_fixed

Documentation

An orbit sum of an element fixed by its first translate is scalar multiplication by the orbit length.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusPowerSum_eq_nsmul_of_fixed (D : DegreeData G) (A : Rep ℤ G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (q : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
    (n : ℕ)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField L))
    (ha : D.frobeniusQuotientAction A K L hLK q a = a) :
    D.frobeniusPowerSum A K L hLK q n a = n • a

theorem

maximalUnramifiedNorm_frobeniusQuotientAction

L248 ↗

ClassFormation.DegreeData.maximalUnramifiedNorm_frobeniusQuotientAction

Documentation

Equivariance of N_{\widetilde L/\widetilde K} expressed inside A_{\widetilde L}.

Source context 10 commands

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

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

Lean source · full declaration

theorem maximalUnramifiedNorm_frobeniusQuotientAction (D : DegreeData G)
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (q : K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField L)) :
    letI : Finite
        ((D.maximalUnramifiedField K).toSubgroup ⧸
          extensionSubgroup (D.maximalUnramifiedField K)
            (D.maximalUnramifiedField L)
            (D.maximalUnramifiedField_mono hLK)) :=
      D.maximalUnramifiedExtension_finite K L hLK
    fixedFieldInclusion A (D.maximalUnramifiedField K)
        (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
        (relativeNorm A (D.maximalUnramifiedField K)
          (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
          (D.frobeniusQuotientAction A K L hLK q a)) =
      D.frobeniusQuotientAction A K L hLK q
        (fixedFieldInclusion A (D.maximalUnramifiedField K)
          (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
          (relativeNorm A (D.maximalUnramifiedField K)
            (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
            a)) := by
  let : Finite
      ((D.maximalUnramifiedField K).toSubgroup ⧸
        extensionSubgroup (D.maximalUnramifiedField K)
          (D.maximalUnramifiedField L)
          (D.maximalUnramifiedField_mono hLK)) :=
    D.maximalUnramifiedExtension_finite K L hLK
  apply Subtype.ext
  exact D.relativeNorm_frobeniusQuotientAction A K L hLK q a

theorem

frobeniusQuotientAction_fixed_of_degreeZero

L283 ↗

ClassFormation.DegreeData.frobeniusQuotientAction_fixed_of_degreeZero

Documentation

A degree-zero element acts trivially on an element already defined over \widetilde K.

Source context 10 commands

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

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

Lean source · statement

theorem frobeniusQuotientAction_fixed_of_degreeZero (D : DegreeData G)
    (A : Rep ℤ G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : D.extensionNormalizedDegree K L hLK q = 1)
    (a : ambientFixedAddSubgroup A (D.maximalUnramifiedField K.field)) :
    D.frobeniusQuotientAction A K.field L hLK q
        (fixedFieldInclusion A (D.maximalUnramifiedField K.field)
          (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK) a) =
      fixedFieldInclusion A (D.maximalUnramifiedField K.field)
        (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK) a

theorem

maximalUnramifiedNorm_fixed_of_hstar

L319 ↗

ClassFormation.DegreeData.maximalUnramifiedNorm_fixed_of_hstar

Documentation

Applying N_{\widetilde L/\widetilde K} to equation (*) kills all degree-zero differences. Hence the norm of u is fixed by the chosen degree-one Frobenius element.

Source context 10 commands

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

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

Lean source · full declaration

theorem maximalUnramifiedNorm_fixed_of_hstar (D : DegreeData G)
    (A : Rep ℤ G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    {ι : Type v} (s : Finset ι)
    (φ : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (τ : ι →
      (D.extensionNormalizedDegreeContinuous K L hLK).toMonoidHom.ker)
    (u : ambientFixedAddSubgroup A (D.maximalUnramifiedField L))
    (uᵢ : ι → ambientFixedAddSubgroup A (D.maximalUnramifiedField L))
    (hstar : D.frobeniusQuotientAction A K.field L hLK φ u - u =
      ∑ i ∈ s,
        (D.frobeniusQuotientAction A K.field L hLK (τ i).1 (uᵢ i) - uᵢ i)) :
    letI : Finite
        ((D.maximalUnramifiedField K.field).toSubgroup ⧸
          extensionSubgroup (D.maximalUnramifiedField K.field)
            (D.maximalUnramifiedField L)
            (D.maximalUnramifiedField_mono hLK)) :=
      D.maximalUnramifiedExtension_finite K.field L hLK
    let N := relativeNorm A (D.maximalUnramifiedField K.field)
      (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
    let b := fixedFieldInclusion A (D.maximalUnramifiedField K.field)
      (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK) (N u)
    D.frobeniusQuotientAction A K.field L hLK φ b = b := by
  dsimp only
  let : Finite
      ((D.maximalUnramifiedField K.field).toSubgroup ⧸
        extensionSubgroup (D.maximalUnramifiedField K.field)
          (D.maximalUnramifiedField L)
          (D.maximalUnramifiedField_mono hLK)) :=
    D.maximalUnramifiedExtension_finite K.field L hLK
  let N := relativeNorm A (D.maximalUnramifiedField K.field)
    (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
  let J := fixedFieldInclusion A (D.maximalUnramifiedField K.field)
    (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK)
  have hnorm := congrArg (J.comp N) hstar
  simp only [map_sub, map_sum] at hnorm
  change J (N (D.frobeniusQuotientAction A K.field L hLK φ u)) - J (N u) =
    ∑ i ∈ s,
      (J (N (D.frobeniusQuotientAction A K.field L hLK (τ i).1 (uᵢ i))) -
        J (N (uᵢ i))) at hnorm
  have hφEquiv :
      J (N (D.frobeniusQuotientAction A K.field L hLK φ u)) =
        D.frobeniusQuotientAction A K.field L hLK φ (J (N u)) := by
    simpa [J, N] using
      D.maximalUnramifiedNorm_frobeniusQuotientAction A K.field L hLK φ u
  rw [hφEquiv] at hnorm
  have hzero (i : ι) :
      J (N (D.frobeniusQuotientAction A K.field L hLK (τ i).1 (uᵢ i))) =
        J (N (uᵢ i)) := by
    calc
      J (N (D.frobeniusQuotientAction A K.field L hLK (τ i).1 (uᵢ i))) =
          D.frobeniusQuotientAction A K.field L hLK (τ i).1 (J (N (uᵢ i))) := by
        simpa [J, N] using
          D.maximalUnramifiedNorm_frobeniusQuotientAction
            A K.field L hLK (τ i).1 (uᵢ i)
      _ = J (N (uᵢ i)) := by
        simpa [J, N] using D.frobeniusQuotientAction_fixed_of_degreeZero
          A K L hLK (τ i).1 (τ i).2 (N (uᵢ i))
  simp_rw [hzero] at hnorm
  have hnormzero :
      D.frobeniusQuotientAction A K.field L hLK φ (J (N u)) - J (N u) = 0 := by
    simpa only [sub_self, Finset.sum_const_zero] using hnorm
  simpa [J, N] using sub_eq_zero.mp hnormzero

theorem

descend_maximalUnramified_fixed_of_finiteSupport

L390 ↗

ClassFormation.DegreeData.descend_maximalUnramified_fixed_of_finiteSupport

Documentation

A \widetilde K-fixed element with finite Galois support descends to K as soon as it is fixed by a degree-one Frobenius lift. The proof is the finite-quotient argument implicit: the finite degree-quotient decomposition writes each element of Gal(P/K) as a positive Frobenius power up to inertia.

Source context 10 commands

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

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

Lean source · statement

theorem descend_maximalUnramified_fixed_of_finiteSupport (D : DegreeData G)
    (A : Rep ℤ G) [IsTopologicalGroup 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)
    (hφ : D.frobeniusExponent K L hLK φ = 1)
    (P : FiniteIntermediateField (D.maximalUnramifiedField L) K.field)
    [hPnormal : (extensionSubgroup K.field P.field P.below).Normal]
    (aI : ambientFixedAddSubgroup A (D.maximalUnramifiedField K.field))
    (aP : ambientFixedAddSubgroup A P.field)
    (hsupport :
      fixedFieldInclusion A P.field (D.maximalUnramifiedField L) P.above aP =
        fixedFieldInclusion A (D.maximalUnramifiedField K.field)
          (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK) aI)
    (hfixed :
      D.frobeniusQuotientAction A K.field L hLK φ.1
          (fixedFieldInclusion A (D.maximalUnramifiedField K.field)
            (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK) aI) =
        fixedFieldInclusion A (D.maximalUnramifiedField K.field)
          (D.maximalUnramifiedField L) (D.maximalUnramifiedField_mono hLK) aI) :
    ∃ aK : ambientFixedAddSubgroup A K.field,
      fixedFieldInclusion A K.field (D.maximalUnramifiedField K.field)
        (D.maximalUnramifiedField_le K.field) aK = aI

Module documentation

Frobenius quotient descent

Declarations