NYLL
Module

EvaluationValue.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldReciprocity.Topological.EvaluationValue
2 declarations indexed from sourceView source ↗

Module documentation

Named value of closed finite-index reciprocity

The expanded inverse norm-residue expression is kept behind one reducible value provider. Public evaluation statements can therefore mention the selected class-field instance tower once while remaining definitionally equivalent to the historical formula.

Imports1
Imported by7

Declarations

theorem

closedFiniteIndexEvaluationValueClassGroupIsMulCommutative

L30 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexEvaluationValueClassGroupIsMulCommutative
Documentation

Canonical class-group commutativity supplies normality for norm-range transport.

Source context 5 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
Lean source · statement
theorem closedFiniteIndexEvaluationValueClassGroupIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
abbrev

closedFiniteIndexClassFieldReciprocityValue

L41 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldReciprocityValue
Documentation

The quotient value prescribed by inverse global norm-residue reciprocity for a Galois element of the selected closed finite-index class field.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
attribute [local instance] closedFiniteIndexEvaluationValueClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
abbrev closedFiniteIndexClassFieldReciprocityValue
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (σ : Gal((closedFiniteIndexClassField
      (K := K) H hclosed)/K)) :
    IdeleClassGroup K ⧸ H

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