Module

NormSubgroup.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.NormSubgroup

36 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: norm subgroups for infinite extensions

For an infinite abstract extension E | K, the abstract class-field construction defines N_{E|K} A_E as the intersection of the norm images from all finite intermediate fields. This file records that definition literally.

Imports2

Imported by3

structure

FiniteIntermediateField

L36 ↗

ClassFormation.FiniteIntermediateField

Documentation

A finite intermediate field M of an abstract extension E | K. Contravariantly, its subgroup lies between G_E and G_K.

Source context 7 commands

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

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

Lean source · full declaration

structure FiniteIntermediateField (E K : ClosedSubgroup G) where
  /-- The closed subgroup representing the intermediate field. -/
  field : ClosedSubgroup G
  /-- The extension endpoint lies below the intermediate-field subgroup. -/
  above : E.toSubgroup ≤ field.toSubgroup
  /-- The intermediate-field subgroup lies below the base endpoint. -/
  below : field.toSubgroup ≤ K.toSubgroup
  /-- The intermediate field has finite degree over the base endpoint. -/
  finite : Finite
    (K.toSubgroup ⧸ extensionSubgroup K field below)

def

base

L50 ↗

ClassFormation.FiniteIntermediateField.base

Documentation

The base field itself is a finite intermediate field.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section finiteIntermediateFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · full declaration

def base (E K : ClosedSubgroup G) (hEK : E.toSubgroup ≤ K.toSubgroup) :
    FiniteIntermediateField E K where
  field := K
  above := hEK
  below := le_rfl
  finite := by
    have htop : extensionSubgroup K K le_rfl = ⊤ := by
      ext x
      constructor
      · intro _
        trivial
      · intro _
        exact x.2
    rw [htop]
    infer_instance

def

finiteIntermediateNormRange

L76 ↗

ClassFormation.finiteIntermediateNormRange

Documentation

The norm image from a finite intermediate field M to K.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

def finiteIntermediateNormRange
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    (M : FiniteIntermediateField E K) :
    AddSubgroup (ambientFixedAddSubgroup A K)

def

infiniteNormSubgroup

L86 ↗

ClassFormation.infiniteNormSubgroup

Documentation

The norm subgroup for a possibly infinite extension: N_{E|K} A_E = ⋂_M N_{M|K} A_M, where M runs through the finite intermediate fields.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

def infiniteNormSubgroup
    (A : Rep ℤ G) (E K : ClosedSubgroup G) :
    AddSubgroup (ambientFixedAddSubgroup A K)

theorem

mem_infiniteNormSubgroup_iff

L94 ↗

ClassFormation.mem_infiniteNormSubgroup_iff

Documentation

Membership in the infinite norm subgroup is characterized by norms from every finite level.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

theorem mem_infiniteNormSubgroup_iff
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    a ∈ infiniteNormSubgroup A E K ↔
      ∀ M : FiniteIntermediateField E K,
        a ∈ finiteIntermediateNormRange A E K M

def

InfiniteNormQuotient

L107 ↗

ClassFormation.InfiniteNormQuotient

Documentation

The quotient A_K / N_{E|K} A_E used by the reciprocity map.

This public object is opaque: clients use infiniteNormClass, InfiniteNormQuotient.induction_on, or infiniteNormQuotientLift instead of depending on the concrete quotient representation.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

def InfiniteNormQuotient
    (A : Rep ℤ G) (E K : ClosedSubgroup G)

instance

infiniteNormQuotientAddCommGroup

L112 ↗

ClassFormation.infiniteNormQuotientAddCommGroup

Documentation

The additive group structure on the infinite norm quotient.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

instance infiniteNormQuotientAddCommGroup
    (A : Rep ℤ G) (E K : ClosedSubgroup G) :
    AddCommGroup (InfiniteNormQuotient A E K)

def

infiniteNormQuotientConcreteEquiv

L119 ↗

ClassFormation.infiniteNormQuotientConcreteEquiv

Documentation

The explicit boundary to the concrete quotient implementation.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

def infiniteNormQuotientConcreteEquiv
    (A : Rep ℤ G) (E K : ClosedSubgroup G) :
    InfiniteNormQuotient A E K ≃+
      ambientFixedAddSubgroup A K ⧸ infiniteNormSubgroup A E K

def

infiniteNormClass

L127 ↗

ClassFormation.infiniteNormClass

Documentation

The canonical class map into the infinite norm quotient.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

def infiniteNormClass
    (A : Rep ℤ G) (E K : ClosedSubgroup G) :
    ambientFixedAddSubgroup A K →+
      InfiniteNormQuotient A E K

theorem

infiniteNormQuotientConcreteEquiv_infiniteNormClass

L137 ↗

ClassFormation.infiniteNormQuotientConcreteEquiv_infiniteNormClass

Documentation

The concrete infinite-norm quotient equivalence sends a class to its canonical quotient class.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

theorem infiniteNormQuotientConcreteEquiv_infiniteNormClass
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    infiniteNormQuotientConcreteEquiv A E K (infiniteNormClass A E K a) =
      QuotientAddGroup.mk' (infiniteNormSubgroup A E K) a

theorem

infiniteNormClass_eq_zero_iff

L146 ↗

ClassFormation.infiniteNormClass_eq_zero_iff

Documentation

An infinite norm class vanishes exactly when its representative lies in the norm subgroup.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

theorem infiniteNormClass_eq_zero_iff
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    infiniteNormClass A E K a = 0 ↔
      a ∈ infiniteNormSubgroup A E K

theorem

infiniteNormClass_surjective

L155 ↗

ClassFormation.infiniteNormClass_surjective

Documentation

Every infinite norm-quotient class has an ambient representative.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

theorem infiniteNormClass_surjective
    (A : Rep ℤ G) (E K : ClosedSubgroup G) :
    Function.Surjective (infiniteNormClass A E K)

theorem

induction_on

L166 ↗

ClassFormation.InfiniteNormQuotient.induction_on

Documentation

Eliminate an infinite norm-quotient class through an ambient representative.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

theorem InfiniteNormQuotient.induction_on
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    {motive : InfiniteNormQuotient A E K → Prop}
    (q : InfiniteNormQuotient A E K)
    (h : ∀ a, motive (infiniteNormClass A E K a)) : motive q

def

infiniteNormQuotientLift

L175 ↗

ClassFormation.infiniteNormQuotientLift

Documentation

Descend an additive homomorphism that kills the infinite norm subgroup.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

def infiniteNormQuotientLift
    {B : Type*} [AddCommGroup B]
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    (f : ambientFixedAddSubgroup A K →+ B)
    (hf : infiniteNormSubgroup A E K ≤ f.ker) :
    InfiniteNormQuotient A E K →+ B

theorem

infiniteNormQuotientLift_infiniteNormClass

L187 ↗

ClassFormation.infiniteNormQuotientLift_infiniteNormClass

Documentation

Lifting the canonical infinite norm class recovers its representative in the concrete quotient.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section infiniteNorms

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

Lean source · statement

theorem infiniteNormQuotientLift_infiniteNormClass
    {B : Type*} [AddCommGroup B]
    (A : Rep ℤ G) (E K : ClosedSubgroup G)
    (f : ambientFixedAddSubgroup A K →+ B)
    (hf : infiniteNormSubgroup A E K ≤ f.ker)
    (a : ambientFixedAddSubgroup A K) :
    infiniteNormQuotientLift A E K f hf (infiniteNormClass A E K a) = f a

def

maximalUnramifiedField

L206 ↗

ClassFormation.DegreeData.maximalUnramifiedField

Documentation

The maximal unramified extension \widetilde L, represented by I_L = G_L ∩ ker(d).

Source context 8 commands

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

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

Lean source · statement

def maximalUnramifiedField (D : DegreeData G) (L : ClosedSubgroup G) :
    ClosedSubgroup G

theorem

maximalUnramifiedField_eq_fieldInertia

L213 ↗

ClassFormation.DegreeData.maximalUnramifiedField_eq_fieldInertia

Documentation

The implementation theorem identifying the maximal unramified field with absolute inertia. Downstream code should use this theorem instead of unfolding maximalUnramifiedField.

Source context 8 commands

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

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

Lean source · statement

theorem maximalUnramifiedField_eq_fieldInertia
    (D : DegreeData G) (L : ClosedSubgroup G) :
    D.maximalUnramifiedField L = D.fieldInertia L

theorem

mem_maximalUnramifiedField_iff

L221 ↗

ClassFormation.DegreeData.mem_maximalUnramifiedField_iff

Documentation

Membership in the maximal unramified field is the expected inertia condition.

Source context 8 commands

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

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

Lean source · statement

theorem mem_maximalUnramifiedField_iff
    (D : DegreeData G) (L : ClosedSubgroup G) (g : G) :
    g ∈ D.maximalUnramifiedField L ↔ g ∈ L ∧ D.degree g = 1

theorem

maximalUnramifiedField_le

L228 ↗

ClassFormation.DegreeData.maximalUnramifiedField_le

Documentation

Every finite unramified field lies below the maximal unramified field.

Source context 8 commands

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

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

Lean source · statement

theorem maximalUnramifiedField_le (D : DegreeData G) (L : ClosedSubgroup G) :
    (D.maximalUnramifiedField L).toSubgroup ≤ L.toSubgroup

theorem

maximalUnramifiedField_le_of_le

L234 ↗

ClassFormation.DegreeData.maximalUnramifiedField_le_of_le

Documentation

A field containing all finite unramified fields contains the maximal unramified field.

Source context 8 commands

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

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

Lean source · statement

theorem maximalUnramifiedField_le_of_le (D : DegreeData G)
    {L K : ClosedSubgroup G} (hLK : L.toSubgroup ≤ K.toSubgroup) :
    (D.maximalUnramifiedField L).toSubgroup ≤ K.toSubgroup

theorem

maximalUnramifiedField_mono

L240 ↗

ClassFormation.DegreeData.maximalUnramifiedField_mono

Documentation

Monotonicity of maximal unramified fields.

Source context 8 commands

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

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

Lean source · statement

theorem maximalUnramifiedField_mono (D : DegreeData G)
    {K L : ClosedSubgroup G} (hLK : L.toSubgroup ≤ K.toSubgroup) :
    (D.maximalUnramifiedField L).toSubgroup ≤
      (D.maximalUnramifiedField K).toSubgroup

theorem

extensionSubgroup_maximalUnramifiedField

L251 ↗

ClassFormation.DegreeData.extensionSubgroup_maximalUnramifiedField

Documentation

Inside G_K, the absolute subgroup of \widetilde L is the relative inertia subgroup.

Source context 8 commands

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

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

Lean source · statement

theorem extensionSubgroup_maximalUnramifiedField (D : DegreeData G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup) :
    extensionSubgroup K (D.maximalUnramifiedField L)
        (D.maximalUnramifiedField_le_of_le hLK) =
      D.extensionInertiaWithin K L hLK

theorem

extensionSubgroup_maximalUnramifiedField_normal

L273 ↗

ClassFormation.DegreeData.extensionSubgroup_maximalUnramifiedField_normal

Documentation

The subgroup representing the maximal unramified field is normal in the base subgroup.

Source context 8 commands

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

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

Lean source · statement

theorem extensionSubgroup_maximalUnramifiedField_normal (D : DegreeData G)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    (extensionSubgroup K (D.maximalUnramifiedField L)
      (D.maximalUnramifiedField_le_of_le hLK)).Normal

def

maximalUnramifiedNormSubgroup

L293 ↗

ClassFormation.DegreeData.maximalUnramifiedNormSubgroup

Documentation

N_{\widetilde L|K} A_{\widetilde L} in the reciprocity construction.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

def maximalUnramifiedNormSubgroup (D : DegreeData G) (A : Rep ℤ G)
    (K L : ClosedSubgroup G) :
    AddSubgroup (ambientFixedAddSubgroup A K)

theorem

maximalUnramifiedNormSubgroup_eq_infiniteNormSubgroup

L300 ↗

ClassFormation.DegreeData.maximalUnramifiedNormSubgroup_eq_infiniteNormSubgroup

Documentation

The maximal-unramified norm subgroup is the infinite norm subgroup for the maximal unramified field.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem maximalUnramifiedNormSubgroup_eq_infiniteNormSubgroup
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G) :
    D.maximalUnramifiedNormSubgroup A K L =
      infiniteNormSubgroup A (D.maximalUnramifiedField L) K

theorem

mem_maximalUnramifiedNormSubgroup_iff

L308 ↗

ClassFormation.DegreeData.mem_maximalUnramifiedNormSubgroup_iff

Documentation

Membership in the maximal unramified norm subgroup is characterized levelwise.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem mem_maximalUnramifiedNormSubgroup_iff
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    a ∈ D.maximalUnramifiedNormSubgroup A K L ↔
      a ∈ infiniteNormSubgroup A (D.maximalUnramifiedField L) K

def

MaximalUnramifiedNormQuotient

L319 ↗

ClassFormation.DegreeData.MaximalUnramifiedNormQuotient

Documentation

A_K / N_{\widetilde L|K} A_{\widetilde L}.

This is an opaque public object, not a reducible alias for the infinite norm quotient.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

def MaximalUnramifiedNormQuotient (D : DegreeData G) (A : Rep ℤ G)
    (K L : ClosedSubgroup G)

instance

maximalUnramifiedNormQuotientAddCommGroup

L324 ↗

ClassFormation.DegreeData.maximalUnramifiedNormQuotientAddCommGroup

Documentation

The additive group structure on the maximal-unramified norm quotient.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

instance maximalUnramifiedNormQuotientAddCommGroup
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G) :
    AddCommGroup (D.MaximalUnramifiedNormQuotient A K L)

def

maximalUnramifiedNormQuotientInfiniteEquiv

L331 ↗

ClassFormation.DegreeData.maximalUnramifiedNormQuotientInfiniteEquiv

Documentation

The explicit boundary to the corresponding infinite norm quotient.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

def maximalUnramifiedNormQuotientInfiniteEquiv
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G) :
    D.MaximalUnramifiedNormQuotient A K L ≃+
      InfiniteNormQuotient A (D.maximalUnramifiedField L) K

def

maximalUnramifiedNormClass

L339 ↗

ClassFormation.DegreeData.maximalUnramifiedNormClass

Documentation

The canonical class map into the maximal-unramified norm quotient.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

def maximalUnramifiedNormClass
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G) :
    ambientFixedAddSubgroup A K →+
      D.MaximalUnramifiedNormQuotient A K L

theorem

maximalUnramifiedNormQuotientInfiniteEquiv_maximalUnramifiedNormClass

L348 ↗

ClassFormation.DegreeData.maximalUnramifiedNormQuotientInfiniteEquiv_maximalUnramifiedNormClass

Documentation

The infinite quotient equivalence preserves the canonical maximal-unramified norm class.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem maximalUnramifiedNormQuotientInfiniteEquiv_maximalUnramifiedNormClass
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    D.maximalUnramifiedNormQuotientInfiniteEquiv A K L
        (D.maximalUnramifiedNormClass A K L a) =
      infiniteNormClass A (D.maximalUnramifiedField L) K a

theorem

maximalUnramifiedNormClass_eq_zero_iff

L358 ↗

ClassFormation.DegreeData.maximalUnramifiedNormClass_eq_zero_iff

Documentation

A maximal-unramified norm class vanishes exactly on its defining norm subgroup.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem maximalUnramifiedNormClass_eq_zero_iff
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    D.maximalUnramifiedNormClass A K L a = 0 ↔
      a ∈ D.maximalUnramifiedNormSubgroup A K L

theorem

maximalUnramifiedNormClass_surjective

L367 ↗

ClassFormation.DegreeData.maximalUnramifiedNormClass_surjective

Documentation

Every maximal-unramified norm class has an ambient representative.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem maximalUnramifiedNormClass_surjective
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G) :
    Function.Surjective (D.maximalUnramifiedNormClass A K L)

theorem

induction_on

L378 ↗

ClassFormation.DegreeData.MaximalUnramifiedNormQuotient.induction_on

Documentation

Eliminate a maximal-unramified norm class through an ambient representative.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem MaximalUnramifiedNormQuotient.induction_on
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G)
    {motive : D.MaximalUnramifiedNormQuotient A K L → Prop}
    (q : D.MaximalUnramifiedNormQuotient A K L)
    (h : ∀ a, motive (D.maximalUnramifiedNormClass A K L a)) : motive q

def

maximalUnramifiedNormQuotientLift

L387 ↗

ClassFormation.DegreeData.maximalUnramifiedNormQuotientLift

Documentation

Descend an additive homomorphism that kills the maximal-unramified norm subgroup.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

def maximalUnramifiedNormQuotientLift
    {B : Type*} [AddCommGroup B]
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (f : ambientFixedAddSubgroup A K →+ B)
    (hf : D.maximalUnramifiedNormSubgroup A K L ≤ f.ker) :
    D.MaximalUnramifiedNormQuotient A K L →+ B

theorem

maximalUnramifiedNormQuotientLift_maximalUnramifiedNormClass

L400 ↗

ClassFormation.DegreeData.maximalUnramifiedNormQuotientLift_maximalUnramifiedNormClass

Documentation

The quotient lift sends a maximal-unramified norm class back to its representative.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section maximalUnramifiedNorms

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

Lean source · statement

theorem maximalUnramifiedNormQuotientLift_maximalUnramifiedNormClass
    {B : Type*} [AddCommGroup B]
    (D : DegreeData G) (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (f : ambientFixedAddSubgroup A K →+ B)
    (hf : D.maximalUnramifiedNormSubgroup A K L ≤ f.ker)
    (a : ambientFixedAddSubgroup A K) :
    D.maximalUnramifiedNormQuotientLift A K L f hf
        (D.maximalUnramifiedNormClass A K L a) = f a

Module documentation

The abstract reciprocity construction: norm subgroups for infinite extensions

Declarations