Module

OrdinaryNormClassField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.OrdinaryNormClassField

28 declarations indexed from sourceView source ↗

Module documentation

Class fields from ordinary idele-class norm neighbourhoods

An actual finite Galois norm subgroup contained in an ordinary idele-class subgroup makes the transported subgroup norm-open in the rational absolute class formation. Finite abelian classification then constructs its class field. The final theorem below transports the result back to the ordinary idele class group of the actual fixed field, so its conclusion is an equality of genuine determinant-norm ranges.

Imports6

Imported by2

def

ordinaryNormClassFieldIdeleClassCommGroup

L41 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldIdeleClassCommGroup

Documentation

Fix the canonical quotient group before converting fixed-field equivalences to additive homomorphisms.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity

Lean source · statement

def ordinaryNormClassFieldIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)

theorem

addSubgroup_map_map_eq_of_comp_eq

L48 ↗

GlobalClassFieldTheory.GlobalClassFields.addSubgroup_map_map_eq_of_comp_eq

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup

Lean source · statement

theorem addSubgroup_map_map_eq_of_comp_eq
    {A B C : Type*} [AddGroup A] [AddGroup B] [AddGroup C]
    (S : AddSubgroup A) (f : A →+ B) (g : B →+ C) (h : A →+ C)
    (hcomp : g.comp f = h) :
    (S.map f).map g = S.map h

theorem

numberFieldTowerFixedBaseFiniteDimensionalPackage

L65 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerFixedBaseFiniteDimensionalPackage

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem numberFieldTowerFixedBaseFiniteDimensionalPackage :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))

theorem

numberFieldTowerFixedBaseNumberFieldPackage

L75 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerFixedBaseNumberFieldPackage

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem numberFieldTowerFixedBaseNumberFieldPackage :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))

instance

numberFieldTowerFixedBaseFiniteDimensional

L89 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerFixedBaseFiniteDimensional

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))

instance

numberFieldTowerFixedBaseNumberField

L97 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerFixedBaseNumberField

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L))

def

ordinaryNormOpenSubgroup

L106 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormOpenSubgroup

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

def ordinaryNormOpenSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    ClassFormation.FiniteAbelianSubextension.NormOpenAddSubgroup
      rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)

theorem

ordinaryNormOpenSubgroup_val

L119 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormOpenSubgroup_val

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

theorem ordinaryNormOpenSubgroup_val
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    (ordinaryNormOpenSubgroup K L H hLH).1 =
      H.toAddSubgroup.map
        (numberFieldTowerIdeleClassEquivAmbientFixed K L).toAddMonoidHom

theorem

numberFieldTowerIdeleClassEquivAmbientFixed_symm_apply

L130 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerIdeleClassEquivAmbientFixed_symm_apply

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L
section FixedBaseTransport
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem numberFieldTowerIdeleClassEquivAmbientFixed_symm_apply
    (c : Additive (IdeleClassGroup K)) :
    (rationalAbstractFixedFieldIdeleClassEquivFixed
        (numberFieldTowerBaseSubgroup K L)).symm
      (numberFieldTowerIdeleClassEquivAmbientFixed K L c) =
        MulEquiv.toAdditive
          (ideleClassCongr
            (numberFieldTowerAbstractBaseFieldEquiv K L)) c

theorem

numberFieldTowerIdeleClassEquivAmbientFixed_comp

L150 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerIdeleClassEquivAmbientFixed_comp

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L
section FixedBaseTransport
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem numberFieldTowerIdeleClassEquivAmbientFixed_comp :
    (rationalAbstractFixedFieldIdeleClassEquivFixed
        (numberFieldTowerBaseSubgroup K L)).symm.toAddMonoidHom.comp
      (numberFieldTowerIdeleClassEquivAmbientFixed K L).toAddMonoidHom =
        (MulEquiv.toAdditive
          (ideleClassCongr
            (numberFieldTowerAbstractBaseFieldEquiv K L)))

theorem

numberFieldTowerBaseTransport_isOpen_of_normRange_le_core

L163 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerBaseTransport_isOpen_of_normRange_le_core

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L
section FixedBaseTransport

Lean source · statement

theorem numberFieldTowerBaseTransport_isOpen_of_normRange_le_core
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    IsOpen
      (((H.toAddSubgroup).map
        (MulEquiv.toAdditive
          (ideleClassCongr
            (numberFieldTowerAbstractBaseFieldEquiv
              K L))).toAddMonoidHom :
        AddSubgroup
          (Additive
            (IdeleClassGroup
              (abstractFixedField ℚ (SeparableClosure ℚ)
                (numberFieldTowerBaseSubgroup K L))))) :
        Set
          (Additive
            (IdeleClassGroup
              (abstractFixedField ℚ (SeparableClosure ℚ)
                (numberFieldTowerBaseSubgroup K L)))))

theorem

exists_finiteAbelianSubextension_normSubgroup_eq_of_normRange_le

L231 ↗

GlobalClassFieldTheory.GlobalClassFields.exists_finiteAbelianSubextension_normSubgroup_eq_of_normRange_le

Documentation

A finite Galois norm neighbourhood inside an ordinary idele-class subgroup produces a finite abelian subextension whose abstract norm subgroup is exactly the transported ordinary subgroup.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

theorem exists_finiteAbelianSubextension_normSubgroup_eq_of_normRange_le
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    ∃ M : FiniteAbelianSubextension
        (numberFieldTowerBaseSubgroup K L),
      M.normSubgroup rationalIdeleClassRepresentation =
        (H.toAddSubgroup).map
          (numberFieldTowerIdeleClassEquivAmbientFixed
            K L).toAddMonoidHom

theorem

numberFieldTowerBaseTransport_isOpen_of_normRange_le

L264 ↗

GlobalClassFieldTheory.GlobalClassFields.numberFieldTowerBaseTransport_isOpen_of_normRange_le

Documentation

The ordinary subgroup transported from K to its compatible embedded fixed-field copy is open whenever it contains an actual finite Galois norm subgroup. This is the concrete comparison between the norm topology and the usual idele-class topology at the chosen realization.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · full declaration

theorem numberFieldTowerBaseTransport_isOpen_of_normRange_le
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    let B := numberFieldTowerBaseSubgroup K L
    let F := abstractFixedField ℚ (SeparableClosure ℚ) B
    IsOpen
      (((H.toAddSubgroup).map
        (MulEquiv.toAdditive
          (ideleClassCongr
            (numberFieldTowerAbstractBaseFieldEquiv
              K L))).toAddMonoidHom :
        AddSubgroup (Additive (IdeleClassGroup F))) :
        Set (Additive (IdeleClassGroup F))) := by
  exact
    numberFieldTowerBaseTransport_isOpen_of_normRange_le_core
      K L H hLH

def

ordinaryNormClassFieldSubextension

L284 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldSubextension

Documentation

The finite abelian subextension selected from an ordinary norm neighbourhood. This is the unique choice point for the realization API below.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

def ordinaryNormClassFieldSubextension
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    FiniteAbelianSubextension (numberFieldTowerBaseSubgroup K L)

theorem

ordinaryNormClassFieldSubextension_normSubgroup

L293 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldSubextension_normSubgroup

Documentation

The selected subextension has the prescribed abstract norm subgroup.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

theorem ordinaryNormClassFieldSubextension_normSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    (ordinaryNormClassFieldSubextension K L H hLH).normSubgroup
        rationalIdeleClassRepresentation =
      H.toAddSubgroup.map
        (numberFieldTowerIdeleClassEquivAmbientFixed
          K L).toAddMonoidHom

abbrev

ordinaryNormClassFieldBase

L307 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldBase

Documentation

The canonical fixed-field copy of the base used by every ordinary norm-neighbourhood realization in the ambient extension L / K.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

abbrev ordinaryNormClassFieldBase : Type

instance

ordinaryNormClassFieldBaseFiniteDimensional

L312 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldBaseFiniteDimensional

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

instance ordinaryNormClassFieldBaseFiniteDimensional :
    FiniteDimensional ℚ (ordinaryNormClassFieldBase K L)

instance

ordinaryNormClassFieldBaseNumberField

L317 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldBaseNumberField

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

instance ordinaryNormClassFieldBaseNumberField :
    NumberField (ordinaryNormClassFieldBase K L)

abbrev

ordinaryNormClassFieldExtension

L323 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldExtension

Documentation

The actual relative fixed field of the selected ordinary class-field subextension.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

abbrev ordinaryNormClassFieldExtension
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) : Type

instance

ordinaryNormClassFieldExtensionFiniteDimensional

L329 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldExtensionFiniteDimensional

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

instance ordinaryNormClassFieldExtensionFiniteDimensional
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    FiniteDimensional (ordinaryNormClassFieldBase K L)
      (ordinaryNormClassFieldExtension K L H hLH)

instance

ordinaryNormClassFieldScalarTower

L342 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldScalarTower

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

instance ordinaryNormClassFieldScalarTower
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    IsScalarTower ℚ (ordinaryNormClassFieldBase K L)
      (ordinaryNormClassFieldExtension K L H hLH)

instance

ordinaryNormClassFieldAbsoluteFiniteDimensional

L349 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldAbsoluteFiniteDimensional

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

instance ordinaryNormClassFieldAbsoluteFiniteDimensional
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    FiniteDimensional ℚ
      (ordinaryNormClassFieldExtension K L H hLH)

instance

ordinaryNormClassFieldExtensionNumberField

L357 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldExtensionNumberField

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

instance ordinaryNormClassFieldExtensionNumberField
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    NumberField (ordinaryNormClassFieldExtension K L H hLH)

instance

ordinaryNormClassFieldExtensionIsGalois

L364 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldExtensionIsGalois

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

instance ordinaryNormClassFieldExtensionIsGalois
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    IsGalois (ordinaryNormClassFieldBase K L)
      (ordinaryNormClassFieldExtension K L H hLH)

instance

ordinaryNormClassFieldExtensionIsAbelianGalois

L376 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldExtensionIsAbelianGalois

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

instance ordinaryNormClassFieldExtensionIsAbelianGalois
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    IsAbelianGalois (ordinaryNormClassFieldBase K L)
      (ordinaryNormClassFieldExtension K L H hLH)

abbrev

ordinaryNormClassFieldBaseEquiv

L386 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldBaseEquiv

Documentation

The canonical equivalence from the original base to the selected fixed-field base.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

abbrev ordinaryNormClassFieldBaseEquiv :
    K ≃ₐ[ℚ] ordinaryNormClassFieldBase K L

theorem

ordinaryNormClassFieldBaseIdeleClassTransport_comp

L391 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassFieldBaseIdeleClassTransport_comp

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · full declaration

theorem ordinaryNormClassFieldBaseIdeleClassTransport_comp :
    let B := numberFieldTowerBaseSubgroup K L
    let eFixed := rationalAbstractFixedFieldIdeleClassEquivFixed B
    let eBase :=
      MulEquiv.toAdditive
        (ideleClassCongr (ordinaryNormClassFieldBaseEquiv K L))
    let eTower := numberFieldTowerIdeleClassEquivAmbientFixed K L
    eFixed.symm.toAddMonoidHom.comp eTower.toAddMonoidHom =
      eBase.toAddMonoidHom := by
  exact numberFieldTowerIdeleClassEquivAmbientFixed_comp K L

theorem

ordinaryNormClassField_ideleClassNorm_range

L404 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryNormClassField_ideleClassNorm_range

Documentation

The determinant-norm range of the selected ordinary class field is the original subgroup transported to the canonical fixed-field base.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
attribute [local instance] ordinaryNormClassFieldIdeleClassCommGroup
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

/- The fixed-field typeclass data used by the topology comparison are kept
behind named constants.  This prevents every consumer from rebuilding the
same finite-dimensional and number-field proof terms while reducing the
dependent fixed-field type. -/
noncomputable local instance
    numberFieldTowerFixedBaseFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseFiniteDimensionalPackage K L
noncomputable local instance numberFieldTowerFixedBaseNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ)
        (numberFieldTowerBaseSubgroup K L)) :=
  numberFieldTowerFixedBaseNumberFieldPackage K L

Lean source · statement

theorem ordinaryNormClassField_ideleClassNorm_range
    (H : Subgroup (IdeleClassGroup K))
    (hLH : (_root_.ideleClassNorm K L).range ≤ H) :
    (_root_.ideleClassNorm
      (ordinaryNormClassFieldBase K L)
      (ordinaryNormClassFieldExtension K L H hLH)).range.toAddSubgroup =
        H.toAddSubgroup.map
          (MulEquiv.toAdditive
            (ideleClassCongr
              (ordinaryNormClassFieldBaseEquiv K L))).toAddMonoidHom

Module documentation

Class fields from ordinary idele-class norm neighbourhoods

Declarations