NYLL
Module

Construction.lean

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

Module documentation

Continuous closed finite-index class-field reciprocity

The final equivalence composes finite global reciprocity with the generic continuous transport induced by the exact norm-range equality. Equality elimination preserves the native quotient topology, so no discrete topology instances are reconstructed here.

Imports1
Imported by7

Declarations

theorem

closedFiniteIndexTopologicalClassGroupIsMulCommutative

L30 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexTopologicalClassGroupIsMulCommutative
Documentation

Canonical class-group commutativity supplies normality for the two quotients.

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

closedFiniteIndexClassFieldGaloisContinuousEquivNormQuotient

L41 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldGaloisContinuousEquivNormQuotient
Documentation

Global reciprocity for the selected class field as a homeomorphic multiplicative equivalence Gal(L / K) ≃ₜ* C_K / 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] closedFiniteIndexTopologicalClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def
    closedFiniteIndexClassFieldGaloisContinuousEquivNormQuotient
    (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.