NYLL
Module

Transport.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldReciprocity.Transport
6 declarations indexed from sourceView source ↗

Module documentation

Generic transport core for Hilbert class-field reciprocity

The quotient transport and its norm-residue evaluation are compiled once in this leaf. Big/small and actual/original Hilbert reciprocity specializations reuse the named data provider without rebuilding the generic reciprocity composite.

Imports1
Imported by5

Declarations

theorem

hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

L30 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Documentation

The shared commutativity provider used by the Hilbert reciprocity leaves.

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 hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
instance

hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal

L35 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal
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
instance
    hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

hilbertClassFieldQuotientTransport_inverse_apply_with

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldQuotientTransport_inverse_apply_with
Documentation

Inverse norm-residue evaluation transported through a subgroup equality and then through an arbitrary multiplicative equivalence.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
local instance
    hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem hilbertClassFieldQuotientTransport_inverse_apply_with
    {G A I : Type} [Group G] [Group A] [Group I]
    (N H : Subgroup G) [N.Normal] [H.Normal]
    (e : Additive (G ⧸ N) ≃+ Additive A)
    (h : N = H) (f : G ⧸ H ≃* I) (c : G) :
    f (QuotientGroup.quotientMulEquivOfEq h
        (Additive.toMul
          (e.symm (e
            (Additive.ofMul (QuotientGroup.mk' N c)))))) =
      f (QuotientGroup.mk' H c)
def

hilbertClassFieldGlobalReciprocityTransportEquiv

L67 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldGlobalReciprocityTransportEquiv
Documentation

Global reciprocity followed by subgroup-equality transport and a chosen quotient equivalence.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
local instance
    hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def hilbertClassFieldGlobalReciprocityTransportEquiv
    {F E I : Type}
    [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    [Group I]
    (H : Subgroup (IdeleClassGroup F))
    (h : (_root_.ideleClassNorm F E).range = H)
    (f : IdeleClassGroup F ⧸ H ≃* I) :
    Gal(E / F) ≃* I
theorem

hilbertClassFieldGlobalReciprocityTransport_globalNormResidue

L83 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldGlobalReciprocityTransport_globalNormResidue
Documentation

Evaluation of the shared transported reciprocity equivalence on the global norm-residue symbol.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
local instance
    hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem hilbertClassFieldGlobalReciprocityTransport_globalNormResidue
    {F E I : Type}
    [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    [Group I]
    (H : Subgroup (IdeleClassGroup F))
    (h : (_root_.ideleClassNorm F E).range = H)
    (f : IdeleClassGroup F ⧸ H ≃* I)
    (c : IdeleClassGroup F) :
    hilbertClassFieldGlobalReciprocityTransportEquiv H h f
        (globalNormResidueMonoidHom F E c) =
      f (QuotientGroup.mk' H c)
def

hilbertClassFieldGlobalReciprocityTransportData

L130 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldGlobalReciprocityTransportData
Documentation

The transported equivalence and its evaluation theorem, packaged once for all four Hilbert class-field specializations.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
local instance
    hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutativeLocal
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def hilbertClassFieldGlobalReciprocityTransportData
    {F E I : Type}
    [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    [Group I]
    (H : Subgroup (IdeleClassGroup F))
    (h : (_root_.ideleClassNorm F E).range = H)
    (f : IdeleClassGroup F ⧸ H ≃* I) :
    {e : Gal(E / F) ≃* I //
      ∀ c : IdeleClassGroup F,
        e (globalNormResidueMonoidHom F E c) =
          f (QuotientGroup.mk' H c)}

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