Module

RestrictionCosets.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.TotallyRamifiedCase.RestrictionCosets

9 declarations indexed from sourceView source ↗

Module documentation

Restriction transport for finite Galois subextensions

This file constructs quotient restriction maps, their coset equivalences, and the compatible relative actions and norms used in ramified towers.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Reduction

Imported by3

def

bundledRestrictionHom

L31 ↗

ClassFormation.FiniteGaloisSubextension.bundledRestrictionHom

Documentation

Restriction between the named finite Galois quotient boundaries.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · statement

def bundledRestrictionHom
    {K : ClosedSubgroup G}
    (M L : FiniteGaloisSubextension K)
    (hML : M.field.toSubgroup ≤ L.field.toSubgroup) :
    M.extensionQuotient →* L.extensionQuotient

def

abstractReciprocityRestrictionCosetMap

L43 ↗

ClassFormation.FiniteGaloisSubextension.abstractReciprocityRestrictionCosetMap

Documentation

The coset map from the lower maximal-unramified quotient to a totally ramified quotient.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · full declaration

def abstractReciprocityRestrictionCosetMap
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup) :
    let M₀ := M.maximalUnramifiedSubextension D
    let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
      M.field_le_intermediateField (M.inertiaImage D)
    (M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) →
      (E.base.toSubgroup ⧸ E.subgroup) := by
  let S := M.inertiaImage D
  let M₀ := M.maximalUnramifiedSubextension D
  let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
    M.field_le_intermediateField S
  let hM₀K : M₀.toSubgroup ≤ E.base.toSubgroup :=
    M.intermediateField_le_base S
  exact Quotient.map'
    (fun x : M₀.toSubgroup =>
      (⟨x.1, hM₀K x.2⟩ : E.base.toSubgroup))
    (by
      intro x y hxy
      rw [QuotientGroup.leftRel_apply] at hxy ⊢
      exact hME hxy)

theorem

abstractReciprocityRestrictionCosetMap_bijective

L69 ↗

ClassFormation.FiniteGaloisSubextension.abstractReciprocityRestrictionCosetMap_bijective

Documentation

The restriction coset map is bijective when the upper extension is totally ramified and the auxiliary field contains the relevant inertia.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · statement

theorem abstractReciprocityRestrictionCosetMap_bijective
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    (hTot : E.IsTotallyRamified D)
    (hInertia : ∀ i : E.base.toSubgroup,
      i ∈ D.fieldInertiaWithin E.base →
      i.1 ∈ E.field.toSubgroup → i.1 ∈ M.field.toSubgroup) :
    Function.Bijective (M.abstractReciprocityRestrictionCosetMap D E hME)

def

abstractReciprocityRestrictionCosetEquiv

L156 ↗

ClassFormation.FiniteGaloisSubextension.abstractReciprocityRestrictionCosetEquiv

Documentation

The equivalence induced by the totally ramified restriction coset map.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · full declaration

def abstractReciprocityRestrictionCosetEquiv
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    (hTot : E.IsTotallyRamified D)
    (hInertia : ∀ i : E.base.toSubgroup,
      i ∈ D.fieldInertiaWithin E.base →
      i.1 ∈ E.field.toSubgroup → i.1 ∈ M.field.toSubgroup) :
    let M₀ := M.maximalUnramifiedSubextension D
    let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
      M.field_le_intermediateField (M.inertiaImage D)
    (M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) ≃
      E.quotient :=
  Equiv.ofBijective (M.abstractReciprocityRestrictionCosetMap D E hME)
    (M.abstractReciprocityRestrictionCosetMap_bijective
      D E hME hTot hInertia)

def

abstractReciprocityRestrictionMulEquiv

L176 ↗

ClassFormation.FiniteGaloisSubextension.abstractReciprocityRestrictionMulEquiv

Documentation

The multiplicative restriction equivalence from the lower Galois group to the original totally ramified quotient.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · full declaration

def abstractReciprocityRestrictionMulEquiv
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    [hEnormal :
      (extensionSubgroup E.base E.field E.below).Normal]
    (hTot : E.IsTotallyRamified D)
    (hInertia : ∀ i : E.base.toSubgroup,
      i ∈ D.fieldInertiaWithin E.base →
      i.1 ∈ E.field.toSubgroup → i.1 ∈ M.field.toSubgroup) :
    let S := M.inertiaImage D
    let N := M.lowerFiniteGalois S
    letI : (extensionSubgroup
        (M.maximalUnramifiedSubextension D) M.field N.below).Normal :=
      N.normal
    letI : Group E.quotient := by
      change Group
        (E.base.toSubgroup ⧸ extensionSubgroup E.base E.field E.below)
      infer_instance
    N.extensionQuotient ≃*
      E.quotient := by
  let S := M.inertiaImage D
  let M₀ := M.maximalUnramifiedSubextension D
  let N := M.lowerFiniteGalois S
  let hM₀K : M₀.toSubgroup ≤ E.base.toSubgroup :=
    M.intermediateField_le_base S
  letI : (extensionSubgroup M₀ M.field N.below).Normal := N.normal
  letI : Group E.quotient := by
    change Group
      (E.base.toSubgroup ⧸ extensionSubgroup E.base E.field E.below)
    infer_instance
  let r : N.extensionQuotient →*
      E.quotient :=
    QuotientGroup.map
      (extensionSubgroup M₀ M.field N.below)
      (extensionSubgroup E.base E.field E.below)
      (Subgroup.inclusion hM₀K)
      (by
        intro m hm
        exact hME hm)
  apply MulEquiv.ofBijective r
  have hr : (r : N.extensionQuotient →
      E.quotient) =
      M.abstractReciprocityRestrictionCosetMap D E hME := by
    funext x
    refine Quotient.inductionOn' x ?_
    intro m
    rfl
  rw [hr]
  exact M.abstractReciprocityRestrictionCosetMap_bijective
    D E hME hTot hInertia

theorem

relativeCosetAction_abstractReciprocityRestrictionCosetEquiv

L231 ↗

ClassFormation.FiniteGaloisSubextension.relativeCosetAction_abstractReciprocityRestrictionCosetEquiv

Documentation

Relative coset actions are transported by the restriction coset equivalence.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · full declaration

theorem relativeCosetAction_abstractReciprocityRestrictionCosetEquiv
    (A : Rep ℤ G) (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    (hTot : E.IsTotallyRamified D)
    (hInertia : ∀ i : E.base.toSubgroup,
      i ∈ D.fieldInertiaWithin E.base →
      i.1 ∈ E.field.toSubgroup → i.1 ∈ M.field.toSubgroup)
    (a : ambientFixedAddSubgroup A E.field)
    (r : let M₀ := M.maximalUnramifiedSubextension D
      let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
        M.field_le_intermediateField (M.inertiaImage D)
      M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) :
    let M₀ := M.maximalUnramifiedSubextension D
    let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
      M.field_le_intermediateField (M.inertiaImage D)
    relativeCosetAction A M₀ M.field hMM₀
        (fixedFieldInclusion A E.field M.field hME a) r =
      relativeCosetAction A E.base E.field E.below a
        (M.abstractReciprocityRestrictionCosetEquiv
          D E hME hTot hInertia r) := by
  let S := M.inertiaImage D
  let M₀ := M.maximalUnramifiedSubextension D
  let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
    M.field_le_intermediateField S
  let hM₀K : M₀.toSubgroup ≤ E.base.toSubgroup :=
    M.intermediateField_le_base S
  refine Quotient.inductionOn' r ?_
  intro x
  rfl

theorem

abstractReciprocity_relativeNorm_fixedFieldInclusion

L265 ↗

ClassFormation.FiniteGaloisSubextension.abstractReciprocity_relativeNorm_fixedFieldInclusion

Documentation

Relative norm commutes with fixed-field inclusion along the totally ramified restriction equivalence.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · full declaration

theorem abstractReciprocity_relativeNorm_fixedFieldInclusion
    (A : Rep ℤ G) (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteAbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    (hTot : E.IsTotallyRamified D)
    (hInertia : ∀ i : E.base.toSubgroup,
      i ∈ D.fieldInertiaWithin E.base →
      i.1 ∈ E.field.toSubgroup → i.1 ∈ M.field.toSubgroup)
    (a : ambientFixedAddSubgroup A E.field) :
    let M₀ := M.maximalUnramifiedSubextension D
    let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
      M.field_le_intermediateField (M.inertiaImage D)
    let hM₀K : M₀.toSubgroup ≤ E.base.toSubgroup :=
      M.intermediateField_le_base (M.inertiaImage D)
    letI : Finite
        (M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) :=
      M.extension_over_intermediate_finite (M.inertiaImage D)
    relativeNorm A M₀ M.field hMM₀
        (fixedFieldInclusion A E.field M.field hME a) =
      fixedFieldInclusion A E.base M₀ hM₀K
        (relativeNorm A E.base E.field E.below a) := by
  let S := M.inertiaImage D
  let M₀ := M.maximalUnramifiedSubextension D
  let hMM₀ : M.field.toSubgroup ≤ M₀.toSubgroup :=
    M.field_le_intermediateField S
  let hM₀K : M₀.toSubgroup ≤ E.base.toSubgroup :=
    M.intermediateField_le_base S
  let hMfinite : Finite
      (M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) :=
    M.extension_over_intermediate_finite S
  let : Finite
      (E.base.toSubgroup ⧸ extensionSubgroup E.base E.field E.below) :=
    E.finiteQuotient
  let e : (M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) ≃
      (E.base.toSubgroup ⧸ extensionSubgroup E.base E.field E.below) :=
    M.abstractReciprocityRestrictionCosetEquiv
      D E.toAbstractExtension hME hTot hInertia
  apply Subtype.ext
  let : Fintype
      (M₀.toSubgroup ⧸ extensionSubgroup M₀ M.field hMM₀) :=
    Fintype.ofFinite _
  let : Fintype
      (E.base.toSubgroup ⧸ extensionSubgroup E.base E.field E.below) :=
    Fintype.ofFinite _
  change (∑ r, relativeCosetAction A M₀ M.field hMM₀
      (fixedFieldInclusion A E.field M.field hME a) r) =
    ∑ q, relativeCosetAction A E.base E.field E.below a q
  calc
    ∑ r, relativeCosetAction A M₀ M.field hMM₀
        (fixedFieldInclusion A E.field M.field hME a) r =
      ∑ r, relativeCosetAction A E.base E.field E.below a (e r) := by
        apply Fintype.sum_congr
        intro r
        exact M.relativeCosetAction_abstractReciprocityRestrictionCosetEquiv
          A D E.toAbstractExtension hME hTot hInertia a r
    _ = ∑ q, relativeCosetAction A E.base E.field E.below a q :=
      e.sum_comp (relativeCosetAction A E.base E.field E.below a)

theorem

commute_of_same_restriction_of_inertia_le

L326 ↗

ClassFormation.FiniteGaloisSubextension.commute_of_same_restriction_of_inertia_le

Documentation

Two auxiliary quotient elements commute when they have the same restriction and the auxiliary field contains the inertia subgroup.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · statement

theorem commute_of_same_restriction_of_inertia_le
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    (hIE : (D.fieldInertia E.field).toSubgroup ≤ M.field.toSubgroup)
    [hEnormal :
      (extensionSubgroup E.base E.field E.below).Normal]
    (g t : E.base.toSubgroup ⧸
      extensionSubgroup E.base M.field M.below)
    (hres : abstractReciprocityRestriction
        E.base E.field M.field hME E.below g =
      abstractReciprocityRestriction
        E.base E.field M.field hME E.below t) :
    Commute g t

theorem

relativeCosetAction_eq_of_restriction_eq

L412 ↗

ClassFormation.FiniteGaloisSubextension.relativeCosetAction_eq_of_restriction_eq

Documentation

Equal restrictions induce equal relative coset actions on elements fixed by the upper field.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open KummerTheory
open CyclicCohomology

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension

Lean source · statement

theorem relativeCosetAction_eq_of_restriction_eq
    (A : Rep ℤ G) (E : DegreeData.AbstractExtension G)
    (M : FiniteGaloisSubextension E.base)
    (hME : M.field.toSubgroup ≤ E.field.toSubgroup)
    [hEnormal :
      (extensionSubgroup E.base E.field E.below).Normal]
    (a : ambientFixedAddSubgroup A E.field)
    (g t : E.base.toSubgroup ⧸
      extensionSubgroup E.base M.field M.below)
    (hres : abstractReciprocityRestriction
        E.base E.field M.field hME E.below g =
      abstractReciprocityRestriction
        E.base E.field M.field hME E.below t) :
    relativeCosetAction A E.base M.field M.below
        (fixedFieldInclusion A E.field M.field hME a) g =
      relativeCosetAction A E.base M.field M.below
        (fixedFieldInclusion A E.field M.field hME a) t

Module documentation

Restriction transport for finite Galois subextensions

Declarations