NYLL
Module

Norm.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.Norm
10 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: norms on abstract fields

This file constructs the norm attached to a finite extension of the abstract fields. An abstract field is represented, as in, by a closed subgroup of the ambient profinite group. The norm is the sum over left cosets (the additive form of the multiplicative product), so it does not require the extension to be Galois.

Imports3
Imported by3

Declarations

def

relativeCosetAction

L38 ↗
ClassFormation.relativeCosetAction
Documentation

The value of a fixed coefficient at a left coset. This is independent of the representative precisely because the coefficient is fixed by the smaller abstract-field subgroup.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def relativeCosetAction
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (a : ambientFixedAddSubgroup A L)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) : A.V
theorem

relativeCosetAction_mk

L59 ↗
ClassFormation.relativeCosetAction_mk
Documentation

The relative coset action on a quotient representative is the corresponding group action.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeCosetAction_mk
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (a : ambientFixedAddSubgroup A L) (k : K.toSubgroup) :
    relativeCosetAction A K L hLK a (QuotientGroup.mk k) = A.ρ k.1 a.1
def

leftMulCosetEquiv

L67 ↗
ClassFormation.leftMulCosetEquiv
Documentation

Left multiplication permutes the cosets of an arbitrary subgroup.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
def leftMulCosetEquiv {G : Type*} [Group G]
    (H : Subgroup G) (g : G) : (G ⧸ H) ≃ (G ⧸ H) where
  toFun q := g • q
  invFun q := g⁻¹ • q
  left_inv q := by simp
  right_inv q := by simp
theorem

leftMulCosetEquiv_mk

L75 ↗
ClassFormation.leftMulCosetEquiv_mk
Documentation

Left multiplication sends the coset of x to the coset of g * x.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem leftMulCosetEquiv_mk {G : Type*} [Group G]
    (H : Subgroup G) (g x : G) :
    leftMulCosetEquiv H g (QuotientGroup.mk x) = QuotientGroup.mk (g * x)
def

relativeNormValue

L81 ↗
ClassFormation.relativeNormValue
Documentation

The additive norm value from A_L to the ambient module.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def relativeNormValue
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : ambientFixedAddSubgroup A L) : A.V
theorem

relativeCosetAction_add

L90 ↗
ClassFormation.relativeCosetAction_add
Documentation

The relative coset action is additive in the represented fixed element.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeCosetAction_add
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (a b : ambientFixedAddSubgroup A L)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) :
    relativeCosetAction A K L hLK (a + b) q =
      relativeCosetAction A K L hLK a q +
        relativeCosetAction A K L hLK b q
theorem

relativeCosetAction_zero

L105 ↗
ClassFormation.relativeCosetAction_zero
Documentation

Every relative coset acts trivially on the zero fixed element.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeCosetAction_zero
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) :
    relativeCosetAction A K L hLK 0 q = 0
theorem

relativeNormValue_fixed

L116 ↗
ClassFormation.relativeNormValue_fixed
Documentation

The relative norm value is fixed by the base subgroup action.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeNormValue_fixed
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : ambientFixedAddSubgroup A L) (k : K.toSubgroup) :
    A.ρ k.1 (relativeNormValue A K L hLK a) =
      relativeNormValue A K L hLK a
def

relativeNorm

L145 ↗
ClassFormation.relativeNorm
Documentation

The norm homomorphism for a finite abstract extension L | K.

In the multiplicative notation of the construction this additive sum is the product over a system of representatives of G_K / G_L. Its codomain is the actual fixed module A_K, with fixedness proved by coset reindexing.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
def relativeNorm
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    ambientFixedAddSubgroup A L →+ ambientFixedAddSubgroup A K where
  toFun a := ⟨relativeNormValue A K L hLK a,
    relativeNormValue_fixed A K L hLK a⟩
  map_zero' := by
    apply Subtype.ext
    let := Fintype.ofFinite (K.toSubgroup ⧸ extensionSubgroup K L hLK)
    simp [relativeNormValue]
  map_add' a b := by
    apply Subtype.ext
    let := Fintype.ofFinite (K.toSubgroup ⧸ extensionSubgroup K L hLK)
    simp only [AddSubgroup.coe_add, relativeNormValue]
    rw [← Finset.sum_add_distrib]
    apply Finset.sum_congr rfl
    intro q _
    exact relativeCosetAction_add A K L hLK a b q
theorem

relativeNorm_apply_coe

L167 ↗
ClassFormation.relativeNorm_apply_coe
Documentation

Coercing a relative norm gives the explicit sum over quotient representatives.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators

-- Mathlib's `Rep ℤ G` currently fixes `G` to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem relativeNorm_apply_coe
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : ambientFixedAddSubgroup A L) :
    ((relativeNorm A K L hLK a : ambientFixedAddSubgroup A K) : A.V) =
      relativeNormValue A K L hLK a

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