NYLL
Module

EvaluationCore.lean

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

Module documentation

Generic evaluation core for transported reciprocity

This theorem works for an arbitrary finite abelian extension and subgroup equality. It proves the composition formula once without unfolding a domain-specific selected-field construction.

Imports1
Imported by7

Declarations

theorem

closedFiniteIndexEvaluationCoreClassGroupIsMulCommutative

L29 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexEvaluationCoreClassGroupIsMulCommutative
Documentation

Canonical class-group commutativity supplies normality in the transport formula.

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 closedFiniteIndexEvaluationCoreClassGroupIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

globalReciprocityContinuousMulEquiv_trans_quotientOfEq_apply

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.globalReciprocityContinuousMulEquiv_trans_quotientOfEq_apply
Documentation

Evaluation of global reciprocity after continuous transport along an equality between the actual norm range and a target subgroup.

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] closedFiniteIndexEvaluationCoreClassGroupIsMulCommutative
variable
    {K L : Type} [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem globalReciprocityContinuousMulEquiv_trans_quotientOfEq_apply
    (H : Subgroup (IdeleClassGroup K))
    (hNorm : (_root_.ideleClassNorm K L).range = H)
    (σ : Gal(L/K)) :
    ((globalReciprocityContinuousMulEquiv K L).trans
      (QuotientGroup.quotientContinuousMulEquivOfEq hNorm)) σ =
      QuotientGroup.quotientMulEquivOfEq hNorm
        (Additive.toMul
          ((globalNormResidueEquiv K L).symm
            (Additive.ofMul σ)))

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