Module

ClassField.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.ClassField

13 declarations indexed from sourceView source ↗

Module documentation

The abstract class-field correspondence

This file gives the inverse direction of the finite abelian classification: a norm-open subgroup produces its class field. The construction is the inverse of the order isomorphism proved by abstract class field theory, so the defining norm-subgroup equality and the two lattice formulas are consequences rather than extra assumptions.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteAbelianClassification

Imported by2

def

classField

L33 ↗

ClassFormation.FiniteAbelianSubextension.classField

Documentation

The class field belonging to a norm-open subgroup.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

def classField
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (N : NormOpenAddSubgroup A K.field) :
    FiniteAbelianSubextension K.field

theorem

classField_normSubgroup

L44 ↗

ClassFormation.FiniteAbelianSubextension.classField_normSubgroup

Documentation

The norm subgroup of the class field of N is N.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem classField_normSubgroup
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (N : NormOpenAddSubgroup A K.field) :
    (classField v hcf K N).normSubgroup A = N.1

theorem

classField_normSubgroupMap

L62 ↗

ClassFormation.FiniteAbelianSubextension.classField_normSubgroupMap

Documentation

Taking the class field is inverse to taking the norm subgroup.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem classField_normSubgroupMap
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L : FiniteAbelianSubextension K.field) :
    classField v hcf K (normSubgroupMap A L) = L

theorem

eq_classField_iff_normSubgroup_eq

L74 ↗

ClassFormation.FiniteAbelianSubextension.eq_classField_iff_normSubgroup_eq

Documentation

Characterization of the unique class field having norm subgroup N.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem eq_classField_iff_normSubgroup_eq
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L : FiniteAbelianSubextension K.field)
    (N : NormOpenAddSubgroup A K.field) :
    L = classField v hcf K N ↔ L.normSubgroup A = N.1

theorem

classField_le_classField_iff

L92 ↗

ClassFormation.FiniteAbelianSubextension.classField_le_classField_iff

Documentation

Inclusion of class fields is reverse inclusion of their defining norm subgroups.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem classField_le_classField_iff
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    classField v hcf K N₁ ≤ classField v hcf K N₂ ↔ N₂.1 ≤ N₁.1

theorem

le_classField_iff

L104 ↗

ClassFormation.FiniteAbelianSubextension.le_classField_iff

Documentation

A finite abelian extension lies in the class field of N exactly when its norm subgroup contains N.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem le_classField_iff
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L : FiniteAbelianSubextension K.field)
    (N : NormOpenAddSubgroup A K.field) :
    L ≤ classField v hcf K N ↔ N.1 ≤ L.normSubgroup A

theorem

classField_le_iff

L117 ↗

ClassFormation.FiniteAbelianSubextension.classField_le_iff

Documentation

The class field of N lies in L exactly when the norm subgroup of L lies in N.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem classField_le_iff
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (N : NormOpenAddSubgroup A K.field)
    (L : FiniteAbelianSubextension K.field) :
    classField v hcf K N ≤ L ↔ L.normSubgroup A ≤ N.1

def

normOpenInf

L130 ↗

ClassFormation.FiniteAbelianSubextension.normOpenInf

Documentation

Intersection of two norm-open subgroups, with its openness produced from finite Galois norm neighbourhoods.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

def normOpenInf
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    NormOpenAddSubgroup A K.field

def

normOpenSup

L148 ↗

ClassFormation.FiniteAbelianSubextension.normOpenSup

Documentation

Product of two norm-open subgroups, with openness produced by either of its open factors.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

def normOpenSup
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    NormOpenAddSubgroup A K.field

theorem

normOpenInf_val

L159 ↗

ClassFormation.FiniteAbelianSubextension.normOpenInf_val

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem normOpenInf_val
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    (normOpenInf K N₁ N₂).1 = N₁.1 ⊓ N₂.1

theorem

normOpenSup_val

L166 ↗

ClassFormation.FiniteAbelianSubextension.normOpenSup_val

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem normOpenSup_val
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    (normOpenSup K N₁ N₂).1 = N₁.1 ⊔ N₂.1

theorem

classField_normOpenInf

L174 ↗

ClassFormation.FiniteAbelianSubextension.classField_normOpenInf

Documentation

The class field of an intersection of norm groups is the compositum of the two class fields.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem classField_normOpenInf
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    classField (D := D) v hcf K (normOpenInf K N₁ N₂) =
      (classField (D := D) v hcf K N₁).compositum
        (classField (D := D) v hcf K N₂)

theorem

classField_normOpenSup

L194 ↗

ClassFormation.FiniteAbelianSubextension.classField_normOpenSup

Documentation

The class field of a product of norm groups is the intersection of the two class fields.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

Lean source · statement

theorem classField_normOpenSup
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (N₁ N₂ : NormOpenAddSubgroup A K.field) :
    classField (D := D) v hcf K (normOpenSup K N₁ N₂) =
      (classField (D := D) v hcf K N₁).intersection
        (classField (D := D) v hcf K N₂)

Module documentation

The abstract class-field correspondence

Declarations