NYLL
Module

RelativeNormDoubleCoset.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.RelativeNormDoubleCoset
10 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: the double-coset decomposition of a relative norm

The norm calculation in the proof of transfer--norm naturality partitions the left cosets for an extension by the orbits of an intermediate subgroup. This file constructs that partition from Mathlib's class-formula equivalence and reindexes the actual relative norm along it.

Imports3
Imported by2

Declarations

theorem

mem_relativeNormDoubleCoset_stabilizer_iff

L42 ↗
ClassFormation.mem_relativeNormDoubleCoset_stabilizer_iff
Documentation

Membership in the stabilizer of a left coset is the literal conjugate intersection condition. For the representative t⁻¹ this reads k' ∈ K' ∩ t⁻¹ S t, the subgroup occurring in the classical double-coset norm calculation.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section doubleCosetEquivalences
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem mem_relativeNormDoubleCoset_stabilizer_iff
    (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (t : K.toSubgroup)
    (k' : extensionSubgroup K K' hK'K) :
    k' ∈ MulAction.stabilizer (extensionSubgroup K K' hK'K)
        (QuotientGroup.mk t :
          K.toSubgroup ⧸ extensionSubgroup K S hSK) ↔
      t.1⁻¹ * k'.1.1 * t.1 ∈ S.toSubgroup
def

relativeNormDoubleCosetEquiv

L67 ↗
ClassFormation.relativeNormDoubleCosetEquiv
Documentation

The class-formula decomposition of the left cosets for S | K into orbits under the subgroup belonging to K' | K and the corresponding stabilizer cosets. These orbits are the double cosets used.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section doubleCosetEquivalences
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def relativeNormDoubleCosetEquiv
    (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup) :
    (K.toSubgroup ⧸ extensionSubgroup K S hSK) ≃
      Σ q : Quotient (orbitRel (extensionSubgroup K K' hK'K)
        (K.toSubgroup ⧸ extensionSubgroup K S hSK)),
        (extensionSubgroup K K' hK'K) ⧸
          MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out
theorem

relativeNormDoubleCosetEquiv_symm_apply

L83 ↗
ClassFormation.relativeNormDoubleCosetEquiv_symm_apply
Documentation

The inverse class-formula map is left multiplication of the selected orbit representative by the selected stabilizer-coset representative.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section doubleCosetEquivalences
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeNormDoubleCosetEquiv_symm_apply
    (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (q : Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)))
    (r : (extensionSubgroup K K' hK'K) ⧸
      MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out) :
    (relativeNormDoubleCosetEquiv K K' S hSK hK'K).symm ⟨q, r⟩ =
      r.out • q.out
theorem

chosenOrbitClassEquiv_symm_apply

L121 ↗
ClassFormation.chosenOrbitClassEquiv_symm_apply
Documentation

The class-formula inverse for an arbitrary chosen representative of each orbit. This form is used in transfer--norm naturality to choose the norm representative t⁻¹ attached to a transfer representative t.

Source context 6 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
Lean source · statement
theorem chosenOrbitClassEquiv_symm_apply
    {M : Type*} {X : Type*} [Group M] [MulAction M X]
    {φ : Quotient (orbitRel M X) → X}
    (hφ : Function.LeftInverse Quotient.mk'' φ)
    (q : Quotient (orbitRel M X))
    (r : M ⧸ stabilizer M (φ q)) :
    (MulAction.selfEquivSigmaOrbitsQuotientStabilizer' M X hφ).symm
        ⟨q, r⟩ = r.out • φ q
theorem

relativeNorm_eq_sum_chosenOrbit_of_fintype

L150 ↗
ClassFormation.relativeNorm_eq_sum_chosenOrbit_of_fintype
Documentation

The relative norm reindexed by arbitrary chosen representatives of the intermediate-subgroup orbits.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section relativeNormFormulas

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeNorm_eq_sum_chosenOrbit_of_fintype
    (A : Rep ℤ G) (K S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (M : Subgroup K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    {φ : Quotient (orbitRel M
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)) →
        (K.toSubgroup ⧸ extensionSubgroup K S hSK)}
    (hφ : Function.LeftInverse Quotient.mk'' φ)
    [Fintype (Quotient (orbitRel M
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)))]
    [(q : Quotient (orbitRel M
      (K.toSubgroup ⧸ extensionSubgroup K S hSK))) →
      Fintype (M ⧸ stabilizer M (φ q))]
    (a : ambientFixedAddSubgroup A S) :
    ((relativeNorm A K S hSK a : ambientFixedAddSubgroup A K) : A.V) =
      ∑ q, ∑ r, relativeCosetAction A K S hSK a
        ((MulAction.selfEquivSigmaOrbitsQuotientStabilizer'
          M (K.toSubgroup ⧸ extensionSubgroup K S hSK) hφ).symm ⟨q, r⟩)
def

relativeNormDoubleCosetSigmaFintype

L181 ↗
ClassFormation.relativeNormDoubleCosetSigmaFintype
Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section relativeNormFormulas

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def relativeNormDoubleCosetSigmaFintype
    (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)] :
    Fintype (Σ q : Quotient (orbitRel
      (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)),
      (extensionSubgroup K K' hK'K) ⧸
        MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out)
def

relativeNormDoubleCosetOrbitFintype

L198 ↗
ClassFormation.relativeNormDoubleCosetOrbitFintype
Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section relativeNormFormulas

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def relativeNormDoubleCosetOrbitFintype
    (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)] :
    Fintype (Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)))
def

relativeNormDoubleCosetStabilizerFintype

L216 ↗
ClassFormation.relativeNormDoubleCosetStabilizerFintype
Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section relativeNormFormulas

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def relativeNormDoubleCosetStabilizerFintype
    (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    (q : Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK))) :
    Fintype ((extensionSubgroup K K' hK'K) ⧸
      MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out)
theorem

relativeNorm_eq_sum_doubleCoset_of_fintype

L239 ↗
ClassFormation.relativeNorm_eq_sum_doubleCoset_of_fintype
Documentation

The double-coset norm formula with caller-supplied finite enumerations of the orbit set and the stabilizer cosets. This form is convenient in arguments which already obtained those enumerations from a transfer formula; the result is independent of their ordering.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section relativeNormFormulas

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeNorm_eq_sum_doubleCoset_of_fintype
    (A : Rep ℤ G) (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    [Fintype (Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)))]
    [(q : Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK))) →
      Fintype ((extensionSubgroup K K' hK'K) ⧸
        MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out)]
    (a : ambientFixedAddSubgroup A S) :
    ((relativeNorm A K S hSK a : ambientFixedAddSubgroup A K) : A.V) =
      ∑ q, ∑ r, relativeCosetAction A K S hSK a
        ((relativeNormDoubleCosetEquiv K K' S hSK hK'K).symm ⟨q, r⟩)
theorem

relativeNorm_eq_sum_doubleCoset

L270 ↗
ClassFormation.relativeNorm_eq_sum_doubleCoset
Documentation

The actual norm N_{S/K} reindexed first by intermediate-subgroup orbits and then by stabilizer cosets. This is the additive form of the double-coset product decomposition in the proof of transfer--norm naturality.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
noncomputable section
open scoped BigOperators
open CyclicCohomology MulAction
section relativeNormFormulas

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
theorem relativeNorm_eq_sum_doubleCoset
    (A : Rep ℤ G) (K K' S : ClosedSubgroup G)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    (a : ambientFixedAddSubgroup A S) :
    let Ω := Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK))
    letI : Fintype Ω :=
      relativeNormDoubleCosetOrbitFintype K K' S hSK hK'K
    letI (q : Ω) : Fintype ((extensionSubgroup K K' hK'K) ⧸
        MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out) :=
      relativeNormDoubleCosetStabilizerFintype K K' S hSK hK'K q
    ((relativeNorm A K S hSK a : ambientFixedAddSubgroup A K) : A.V) =
      ∑ q, ∑ r, relativeCosetAction A K S hSK a
        ((relativeNormDoubleCosetEquiv K K' S hSK hK'K).symm ⟨q, r⟩) := by
  dsimp only
  let := Fintype.ofFinite
    (K.toSubgroup ⧸ extensionSubgroup K S hSK)
  let : Fintype (Quotient (orbitRel
      (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK))) :=
    relativeNormDoubleCosetOrbitFintype K K' S hSK hK'K
  let (q : Quotient (orbitRel (extensionSubgroup K K' hK'K)
      (K.toSubgroup ⧸ extensionSubgroup K S hSK))) :
      Fintype ((extensionSubgroup K K' hK'K) ⧸
        MulAction.stabilizer (extensionSubgroup K K' hK'K) q.out) :=
    relativeNormDoubleCosetStabilizerFintype K K' S hSK hK'K q
  exact relativeNorm_eq_sum_doubleCoset_of_fintype
    A K K' S hSK hK'K a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.