Module

FrobeniusActionRemainder.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainMultiplicativity.FrobeniusActionRemainder

10 declarations indexed from sourceView source ↗

Module documentation

Frobenius action remainders

This file develops the Frobenius exponent, conjugation, quotient-action, and action-remainder identities used by reciprocity-map multiplicativity.

Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same universe, so this representation-bearing portion has G : IntegralRepGroupType.

Imports3

Imported by7

theorem

frobeniusQuotientAction_fixedFieldInclusion

L85 ↗

ClassFormation.DegreeData.frobeniusQuotientAction_fixedFieldInclusion

Documentation

A Frobenius element fixes the elements of its actual fixed field, viewed inside A_{\widetilde L}.

Source context 9 commands

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

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

Lean source · statement

theorem frobeniusQuotientAction_fixedFieldInclusion (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)
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ)) :
    D.frobeniusQuotientAction A K.field L hLK σ.1
        (fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
          (D.maximalUnramifiedField L)
          (D.fieldInertia_le_frobeniusFixedField K L hLK σ) a) =
      fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
        (D.maximalUnramifiedField L)
        (D.fieldInertia_le_frobeniusFixedField K L hLK σ) a

def

frobeniusActionRemainder_mem_degreeKernel

L144 ↗

ClassFormation.DegreeData.frobeniusActionRemainder_mem_degreeKernel

Documentation

If φ has Frobenius exponent one, its action remainder has normalized degree zero.

Source context 9 commands

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

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

Lean source · statement

theorem frobeniusActionRemainder_mem_degreeKernel (D : DegreeData 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) :
    D.frobeniusActionRemainder K L hLK φ σ ∈
      (D.extensionNormalizedDegreeContinuous K L hLK).toMonoidHom.ker

def

frobeniusExponent_actionConjugate

L187 ↗

ClassFormation.DegreeData.frobeniusExponent_actionConjugate

Documentation

Frobenius action conjugation preserves the Frobenius exponent.

Source context 9 commands

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

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

Lean source · statement

theorem frobeniusExponent_actionConjugate (D : DegreeData 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) (m : ℕ) :
    D.frobeniusExponent K L hLK
        (D.frobeniusActionConjugate K L hLK φ σ m) =
      D.frobeniusExponent K L hLK σ

theorem

conjugate_frobeniusFixedField_actionConjugate

L215 ↗

ClassFormation.DegreeData.conjugate_frobeniusFixedField_actionConjugate

Documentation

The fixed field of the left-action conjugate φᵐσφ⁻ᵐ is the corresponding conjugate of the fixed field of σ. The representative is only used to express the quotient conjugation in the ambient absolute Galois group.

Source context 9 commands

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

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

Lean source · full declaration

theorem conjugate_frobeniusFixedField_actionConjugate
    (D : DegreeData 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) (m : ℕ) :
    let q := φ.1 ^ m
    let k : K.field.toSubgroup := Quotient.out q
    conjugateClosedSubgroup
        (D.frobeniusFixedField K L hLK σ) k.1⁻¹ =
      D.frobeniusFixedField K L hLK
        (D.frobeniusActionConjugate K L hLK φ σ m) := by
  dsimp only
  let q := φ.1 ^ m
  let k : K.field.toSubgroup := Quotient.out q
  let σ' := D.frobeniusActionConjugate K L hLK φ σ m
  have hkq :
      (QuotientGroup.mk k :
        K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) = q :=
    Quotient.out_eq' q
  have hσ' : σ'.1 = q * σ.1 * q⁻¹ := by
    simp [σ', q, frobeniusActionConjugate_coe]
  ext x
  change x ∈ conjugateClosedSubgroup
      (D.frobeniusFixedField K L hLK σ) k.1⁻¹ ↔
    x ∈ D.frobeniusFixedField K L hLK σ'
  rw [conjugateClosedSubgroup_mem]
  constructor
  · intro hx
    obtain ⟨t, htClosure, htx⟩ := hx
    let xK : K.field.toSubgroup := ⟨x, by
      have htK : t.1 ∈ K.field.toSubgroup := t.2
      have htxval : t.1 = k.1⁻¹ * x * k.1 := by simpa using htx
      have hxval : x = k.1 * t.1 * k.1⁻¹ := by
        calc
          x = k.1 * (k.1⁻¹ * x * k.1) * k.1⁻¹ := by
            simp [mul_assoc]
          _ = k.1 * t.1 * k.1⁻¹ := by rw [htxval]
      rw [hxval]
      exact K.field.toSubgroup.mul_mem
        (K.field.toSubgroup.mul_mem k.2 htK) (K.field.toSubgroup.inv_mem k.2)⟩
    have htClosure' : QuotientGroup.mk t ∈
        (closedSubgroupGenerated ({σ.1} : Set
          (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK))).toSubgroup := by
      simpa [DegreeData.frobeniusClosure] using htClosure
    have hxClosure' : q * QuotientGroup.mk t * q⁻¹ ∈
        (closedSubgroupGenerated ({σ'.1} : Set
          (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK))).toSubgroup := by
      rw [hσ']
      exact (mem_closedSubgroupGenerated_conjugate_iff
        q σ.1 (QuotientGroup.mk t)).mp htClosure'
    have hxClosure : QuotientGroup.mk xK ∈
        (D.frobeniusClosure K L hLK σ').toSubgroup := by
      have hxK : xK = k * t * k⁻¹ := by
        apply Subtype.ext
        dsimp [xK]
        have htxval : t.1 = k.1⁻¹ * x * k.1 := by simpa using htx
        calc
          x = k.1 * (k.1⁻¹ * x * k.1) * k.1⁻¹ := by
            simp [mul_assoc]
          _ = k.1 * t.1 * k.1⁻¹ := by rw [htxval]
      rw [hxK]
      change (QuotientGroup.mk k :
          K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) *
          QuotientGroup.mk t * (QuotientGroup.mk k)⁻¹ ∈ _
      rw [hkq]
      simpa [DegreeData.frobeniusClosure] using hxClosure'
    exact ⟨xK, hxClosure, rfl⟩
  · intro hx
    obtain ⟨t, htClosure, htx⟩ := hx
    let yK : K.field.toSubgroup := ⟨k.1⁻¹ * x * k.1, by
      have htK : t.1 ∈ K.field.toSubgroup := t.2
      rw [← htx]
      exact K.field.toSubgroup.mul_mem
        (K.field.toSubgroup.mul_mem (K.field.toSubgroup.inv_mem k.2) htK) k.2⟩
    have htClosure' : QuotientGroup.mk t ∈
        (closedSubgroupGenerated ({σ'.1} : Set
          (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK))).toSubgroup := by
      simpa [DegreeData.frobeniusClosure] using htClosure
    have hyClosure' : QuotientGroup.mk yK ∈
        (closedSubgroupGenerated ({σ.1} : Set
          (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK))).toSubgroup := by
      apply (mem_closedSubgroupGenerated_conjugate_iff
        q σ.1 (QuotientGroup.mk yK)).mpr
      have hyK : k * yK * k⁻¹ = t := by
        apply Subtype.ext
        dsimp [yK]
        simpa [mul_assoc] using htx.symm
      have hyKq : q * QuotientGroup.mk yK * q⁻¹ =
          (QuotientGroup.mk t :
            K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) := by
        rw [← hkq]
        simpa using congrArg
          (fun z : K.field.toSubgroup =>
            (QuotientGroup.mk z :
              K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)) hyK
      rw [hyKq]
      rw [← hσ']
      exact htClosure'
    exact ⟨yK, by simpa [DegreeData.frobeniusClosure] using hyClosure', by simp [yK]⟩

theorem

frobeniusActionRemainder_mul

L328 ↗

ClassFormation.DegreeData.frobeniusActionRemainder_mul

Documentation

Left-action translation of τ₃=τ₂τ₄: conjugation moves to the second factor and the order reverses.

Source context 9 commands

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

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

Lean source · statement

theorem frobeniusActionRemainder_mul (D : DegreeData 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) :
    D.frobeniusActionRemainder K L hLK φ (σ₁ * σ₂) =
      D.frobeniusActionRemainder K L hLK φ
          (D.frobeniusActionConjugate K L hLK φ σ₂
            (D.frobeniusExponent K L hLK σ₁)) *
        D.frobeniusActionRemainder K L hLK φ σ₁

theorem

frobeniusActionRemainder_apply_fixedField

L377 ↗

ClassFormation.DegreeData.frobeniusActionRemainder_apply_fixedField

Documentation

On the fixed field of σ, the left-action remainder acts exactly as the n-th power of φ.

Source context 9 commands

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

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

Lean source · statement

theorem frobeniusActionRemainder_apply_fixedField (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)
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ)) :
    D.frobeniusQuotientAction A K.field L hLK
        (D.frobeniusActionRemainder K L hLK φ σ)
        (fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
          (D.maximalUnramifiedField L)
          (D.fieldInertia_le_frobeniusFixedField K L hLK σ) a) =
      D.frobeniusQuotientAction A K.field L hLK
        (φ.1 ^ D.frobeniusExponent K L hLK σ)
        (fixedFieldInclusion A (D.frobeniusFixedField K L hLK σ)
          (D.maximalUnramifiedField L)
          (D.fieldInertia_le_frobeniusFixedField K L hLK σ) a)

Module documentation

Frobenius action remainders

Declarations