Module

GlobalNormResidue.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldReciprocity.GlobalNormResidue

3 declarations indexed from sourceView source ↗

Module documentation

Norm-residue evaluation for a closed finite-index class field

This leaf proves that the selected class-field reciprocity equivalence sends the global norm-residue symbol to the corresponding quotient class.

Imports2

Imported by5

theorem

closedFiniteIndexNormResidueClassGroupIsMulCommutative

L29 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormResidueClassGroupIsMulCommutative

Documentation

Canonical class-group commutativity supplies normality for quotient evaluation.

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

theorem

quotientTransport_inverse_apply

L38 ↗

GlobalClassFieldTheory.GlobalClassFields.quotientTransport_inverse_apply

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] closedFiniteIndexNormResidueClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem quotientTransport_inverse_apply
    {G A : Type*} [Group G] [Group A]
    (N H : Subgroup G) [N.Normal] [H.Normal]
    (e : Additive (G ⧸ N) ≃+ Additive A)
    (h : N = H) (c : G) :
    QuotientGroup.quotientMulEquivOfEq h
        (Additive.toMul
          (e.symm
            (e (Additive.ofMul (QuotientGroup.mk' N c))))) =
      QuotientGroup.mk' H c

theorem

closedFiniteIndexClassFieldGaloisEquivNormQuotient_globalNormResidue

L63 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldGaloisEquivNormQuotient_globalNormResidue

Documentation

Under the direct class-field reciprocity equivalence, the global norm-residue symbol of an idèle class is its quotient class modulo H.

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] closedFiniteIndexNormResidueClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    closedFiniteIndexClassFieldGaloisEquivNormQuotient_globalNormResidue
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (c : IdeleClassGroup K) :
    closedFiniteIndexClassFieldGaloisEquivNormQuotient
        (K := K) H hclosed
        (globalNormResidueMonoidHom K
          (closedFiniteIndexClassField
            (K := K) H hclosed) c) =
      QuotientGroup.mk' H c

Module documentation

Norm-residue evaluation for a closed finite-index class field

Declarations

closedFiniteIndexNormResidueClassGroupIsMulCommutative

quotientTransport_inverse_apply

closedFiniteIndexClassFieldGaloisEquivNormQuotient_globalNormResidue