NYLL
Module

Construction.lean

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

Module documentation

Underlying algebraic closed finite-index reciprocity

The algebraic equivalence is obtained by forgetting topology from the named continuous provider. This avoids a second specialization of the full finite global reciprocity instance tower.

Imports5
Imported by7

Declarations

theorem

closedFiniteIndexAlgebraicClassGroupIsMulCommutative

L31 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexAlgebraicClassGroupIsMulCommutative
Documentation

Canonical class-group commutativity supplies normality of the defining subgroup.

Source context 4 commands

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

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

closedFiniteIndexClassFieldGaloisEquivNormQuotient

L42 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldGaloisEquivNormQuotient
Documentation

Global reciprocity for the selected class field, stated over the original number field and directly modulo its defining subgroup.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
attribute [local instance] closedFiniteIndexAlgebraicClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
abbrev closedFiniteIndexClassFieldGaloisEquivNormQuotient
    (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.