NYLL
Module

ClassFieldAxiom.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.ClassFieldAxiom
5 declarations indexed from sourceView source ↗

Module documentation

Abstract reciprocity: the class field axiom

The coefficient group for a finite cyclic extension L / K is the actual fixed module A_L, descended to the actual quotient G_K / G_L. Thus the two numbers below are the orders of the Tate groups occurring in the original statement the class-field axiom, rather than cardinality data attached to an auxiliary reciprocity map.

Representation.Rep places its coefficient ring and acting group in the same universe. The shared IntegralRepGroupType boundary records the universe forced by the coefficient ring ℤ without scattering raw universe-zero declarations through the reciprocity API.

Imports1
Imported by5

Declarations

structure

ClassFieldAxiomCohomologyData

L38 ↗
ClassFormation.ClassFieldAxiomCohomologyData
Documentation

The finite cohomology data asserted at one finite cyclic extension. Finiteness is stored before either natural-valued cardinality is formed.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
open CategoryTheory
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
structure ClassFieldAxiomCohomologyData (A : Rep ℤ G)
    (K : FiniteAbstractField G) (E : FiniteCyclicSubextension K) : Prop where
  /-- The degree-zero Tate cohomology group is finite. -/
  finiteTateHZero : Finite (tateCohomology (E.fixedRepresentation A) 0)
  /-- The degree-minus-one Tate cohomology group is finite. -/
  finiteTateHMinusOne :
    Finite (tateCohomology (E.fixedRepresentation A) (-1))
  /-- Degree-zero Tate cohomology has cardinality equal to the extension degree. -/
  tateHZero_card :
    Nat.card (tateCohomology (E.fixedRepresentation A) 0) =
      (E.toFiniteAbstractExtension.degree : ℕ)
  /-- Degree-minus-one Tate cohomology is trivial by cardinality. -/
  tateHMinusOne_card :
    Nat.card (tateCohomology (E.fixedRepresentation A) (-1)) = 1
def

SatisfiesClassFieldAxiom

L60 ↗
ClassFormation.SatisfiesClassFieldAxiom
Documentation

The class-field axiom. For every finite cyclic extension L / K with K finite over the distinguished base field, #H⁰(G(L/K), A_L) = [L : K] and #H⁻¹(G(L/K), A_L) = 1.

Both the base field and the cyclic extension are bundled, so containment, finiteness, normality, and the chosen generator cannot become detached from the subgroups to which they belong.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
open CategoryTheory
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def SatisfiesClassFieldAxiom (A : Rep ℤ G) : Prop
theorem

tateHZero_card

L70 ↗
ClassFormation.SatisfiesClassFieldAxiom.tateHZero_card
Documentation

The degree-zero half of the class-field axiom for a bundled cyclic extension.

Source context 7 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
open CategoryTheory
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace SatisfiesClassFieldAxiom
variable {A : Rep ℤ G}
Lean source · statement
theorem tateHZero_card
    (hcf : SatisfiesClassFieldAxiom A)
    (K : FiniteAbstractField G) (E : FiniteCyclicSubextension K) :
    Nat.card (tateCohomology (E.fixedRepresentation A) 0) =
      (E.toFiniteAbstractExtension.degree : ℕ)
theorem

tateHMinusOne_card

L79 ↗
ClassFormation.SatisfiesClassFieldAxiom.tateHMinusOne_card
Documentation

The degree-minus-one half of the class-field axiom for a bundled cyclic extension.

Source context 7 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
open CategoryTheory
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace SatisfiesClassFieldAxiom
variable {A : Rep ℤ G}
Lean source · statement
theorem tateHMinusOne_card
    (hcf : SatisfiesClassFieldAxiom A)
    (K : FiniteAbstractField G) (E : FiniteCyclicSubextension K) :
    Nat.card (tateCohomology (E.fixedRepresentation A) (-1)) = 1
theorem

tateHMinusOne_isZero

L87 ↗
ClassFormation.SatisfiesClassFieldAxiom.tateHMinusOne_isZero
Documentation

The order-one assertion in the class-field axiom gives actual vanishing of H⁻¹(G(L/K), A_L).

Source context 7 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
open CategoryTheory
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace SatisfiesClassFieldAxiom
variable {A : Rep ℤ G}
Lean source · statement
theorem tateHMinusOne_isZero
    (hcf : SatisfiesClassFieldAxiom A)
    (K : FiniteAbstractField G) (E : FiniteCyclicSubextension K) :
    Limits.IsZero (tateCohomology (E.fixedRepresentation A) (-1))

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