Module

FrobeniusDescent.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FrobeniusDescent

7 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: descent from the Frobenius semigroup

The two maps on G(\widetilde L/K)--restriction to G(L/K) and normalized degree--are jointly injective. This is the group-theoretic fact used when two Frobenius lifts have the same restriction and degree.

Imports2

Imported by2

def

extensionImageInInertiaQuotient

L32 ↗

ClassFormation.DegreeData.extensionImageInInertiaQuotient

Documentation

The image of G_L in G_K / I_L.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def extensionImageInInertiaQuotient (D : DegreeData G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    Subgroup (K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)

theorem

extensionImageInInertiaQuotient_isClosed

L42 ↗

ClassFormation.DegreeData.extensionImageInInertiaQuotient_isClosed

Documentation

The image of G_L in G_K / I_L is closed. This is the compact-image step implicit in the Galois correspondence used.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem extensionImageInInertiaQuotient_isClosed
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space 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)] :
    IsClosed (D.extensionImageInInertiaQuotient K.field L hLK : Set
      (K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK))

theorem

frobeniusFixedField_le_of_inertia_le_of_lift_mem

L76 ↗

ClassFormation.DegreeData.frobeniusFixedField_le_of_inertia_le_of_lift_mem

Documentation

A finite field fixed by both the relative inertia and one representative of a Frobenius lift is contained in the lift's Frobenius fixed field. This is the closed-subgroup minimality argument used in finiteness of the Frobenius fixed field.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusFixedField_le_of_inertia_le_of_lift_mem
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D) (L M : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    (hMK : M.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hMfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field M hMK)]
    (σ : D.FrobeniusElements K L hLK)
    (hI : D.extensionInertiaWithin K.field L hLK ≤
      extensionSubgroup K.field M hMK)
    (s : K.field.toSubgroup)
    (hsM : s ∈ extensionSubgroup K.field M hMK)
    (hsσ : (QuotientGroup.mk s :
      K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) = σ.1) :
    (D.frobeniusFixedField K L hLK σ).toSubgroup ≤
      M.toSubgroup

theorem

frobeniusFixedField_le_of_restriction_eq_one

L137 ↗

ClassFormation.DegreeData.frobeniusFixedField_le_of_restriction_eq_one

Documentation

If a Frobenius lift restricts trivially to L, its fixed field contains L (equivalently G_Σ ≤ G_L).

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusFixedField_le_of_restriction_eq_one
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space 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)]
    (σ : D.FrobeniusElements K L hLK)
    (hσ : D.frobeniusRestriction K L hLK σ = 1) :
    (D.frobeniusFixedField K L hLK σ).toSubgroup ≤
      L.toSubgroup

theorem

extensionRestriction_normalizedDegree_joint_injective

L185 ↗

ClassFormation.DegreeData.extensionRestriction_normalizedDegree_joint_injective

Documentation

Restriction and normalized degree jointly distinguish elements of G(\widetilde L/K).

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · full declaration

theorem extensionRestriction_normalizedDegree_joint_injective
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    Function.Injective (fun q :
        K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK =>
      (D.extensionRestriction K.field L hLK q,
        D.extensionNormalizedDegree K L hLK q)) := by
  intro q r hqr
  refine Quotient.inductionOn₂' q r ?_ hqr
  intro a b hab
  apply QuotientGroup.eq.mpr
  have hRestriction : QuotientGroup.mk a =
      (QuotientGroup.mk b :
        K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK) := by
    exact congrArg Prod.fst hab
  have hExtension : a⁻¹ * b ∈ extensionSubgroup K.field L hLK :=
    QuotientGroup.eq.mp hRestriction
  have hDegree : D.normalizedDegree K a =
      D.normalizedDegree K b :=
    congrArg Prod.snd hab
  refine ⟨hExtension, ?_⟩
  rw [← D.normalizedDegree_ker K]
  change D.normalizedDegree K (a⁻¹ * b) = 1
  rw [map_mul, map_inv, hDegree, inv_mul_cancel]

theorem

frobeniusRestriction_mul

L217 ↗

ClassFormation.DegreeData.frobeniusRestriction_mul

Documentation

frobeniusRestriction satisfies the multiplication formula D.frobeniusRestriction K L hLK (σ * τ) = D.frobeniusRestriction K L hLK σ * D.frobeniusRestriction K L hLK τ.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusRestriction_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.frobeniusRestriction K L hLK (σ * τ) =
      D.frobeniusRestriction K L hLK σ *
        D.frobeniusRestriction K L hLK τ

theorem

frobenius_eq_of_restriction_eq_of_degree_eq

L232 ↗

ClassFormation.DegreeData.frobenius_eq_of_restriction_eq_of_degree_eq

Documentation

Frobenius elements with equal restriction and equal normalized degree are equal.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobenius_eq_of_restriction_eq_of_degree_eq
    (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}
    (hRestriction :
      D.frobeniusRestriction K L hLK σ =
        D.frobeniusRestriction K L hLK τ)
    (hDegree :
      D.extensionNormalizedDegree K L hLK σ.1 =
        D.extensionNormalizedDegree K L hLK τ.1) :
    σ = τ

Module documentation

The abstract reciprocity construction: descent from the Frobenius semigroup

Declarations

extensionImageInInertiaQuotient

extensionImageInInertiaQuotient_isClosed

frobeniusFixedField_le_of_inertia_le_of_lift_mem

frobeniusFixedField_le_of_restriction_eq_one

extensionRestriction_normalizedDegree_joint_injective

frobeniusRestriction_mul

frobenius_eq_of_restriction_eq_of_degree_eq