Module

Representatives.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.Representatives

6 declarations indexed from sourceView source ↗

Module documentation

Representatives and comparison endpoints for rational finite-norm transport

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.FieldSpine

Imported by5

instance

representativesIdeleClassGroupIsMulCommutative

L31 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.representativesIdeleClassGroupIsMulCommutative

Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory

Lean source · statement

instance
    representativesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

representativesIdeleClassSubgroupNormal

L37 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.representativesIdeleClassSubgroupNormal

Source context 9 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    representativesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative

Lean source · statement

instance
    representativesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal

def

rationalFiniteNormTransferAbstractRepresentative

L45 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferAbstractRepresentative

Documentation

The ordinary idele-class representative obtained from abstract fixed-field inclusion.

Source context 10 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    representativesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    representativesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def rationalFiniteNormTransferAbstractRepresentative
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K)

def

rationalFiniteNormTransferCanonicalFixedRepresentative

L78 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFixedRepresentative

Documentation

The canonical fixed-field representative attached to an ordinary base idele class.

Source context 10 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    representativesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    representativesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def rationalFiniteNormTransferCanonicalFixedRepresentative
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) :
    rationalFiniteNormTransferExtensionIdeleClass K L hLK

def

rationalFiniteNormTransferOrdinaryExtensionRepresentative

L126 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferOrdinaryExtensionRepresentative

Documentation

The ordinary extension representative attached to the same base idele class.

Source context 10 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    representativesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    representativesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def rationalFiniteNormTransferOrdinaryExtensionRepresentative
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (_hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) :
    rationalFiniteNormTransferExtensionIdeleClass K L hLK

def

rationalFiniteNormTransferCanonicalAbstractExtensionEndpoint

L168 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalAbstractExtensionEndpoint

Documentation

The common additive endpoint appearing in the base-change and relative-to-ordinary comparisons.

Source context 10 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    representativesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    representativesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def rationalFiniteNormTransferCanonicalAbstractExtensionEndpoint
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (_hnormal : (extensionSubgroup K L hLK).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) :
    Additive (rationalFiniteNormTransferExtensionIdeleClass K L hLK)

Module documentation

Representatives and comparison endpoints for rational finite-norm transport

Declarations

representativesIdeleClassGroupIsMulCommutative

representativesIdeleClassSubgroupNormal

rationalFiniteNormTransferAbstractRepresentative

rationalFiniteNormTransferCanonicalFixedRepresentative

rationalFiniteNormTransferOrdinaryExtensionRepresentative

rationalFiniteNormTransferCanonicalAbstractExtensionEndpoint