NYLL
Module

Quotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.Quotient
6 declarations indexed from sourceView source ↗

Module documentation

Norm quotient maps for rational finite-norm transport

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

Imports1
Imported by5

Declarations

instance

quotientIdeleClassGroupIsMulCommutative

L31 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.quotientIdeleClassGroupIsMulCommutative
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
    quotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
instance

quotientIdeleClassSubgroupNormal

L37 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.quotientIdeleClassSubgroupNormal
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
    quotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
Lean source · statement
instance
    quotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal
def

rationalFiniteNormTransferQuotientMap

L45 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferQuotientMap
Documentation

The canonical map from ordinary idele classes to the additive norm quotient used by rational finite-norm transport.

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
    quotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    quotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N
Lean source · statement
def rationalFiniteNormTransferQuotientMap
    (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)] :
    rationalFiniteNormTransferBaseIdeleClass K →
      rationalFiniteNormTransferQuotientTarget
        K L hLK hnormal
def

rationalFiniteNormTransferNormMembership

L85 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferNormMembership
Documentation

Membership in the ordinary norm range represented by the rational finite-norm quotient.

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
    quotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    quotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N
Lean source · statement
def rationalFiniteNormTransferNormMembership
    (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) : Prop
theorem

rationalFiniteNormTransferFiniteNormClass_spec

L126 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferFiniteNormClass_spec
Documentation

A rational finite norm class is sent to the canonical quotient class of its ordinary idele-class representative.

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
    quotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    quotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N
Lean source · statement
theorem rationalFiniteNormTransferFiniteNormClass_spec
    (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)]
    (b : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K) :
    rationalFiniteNormQuotientEquivIdeleClassNormQuotient
        K L hLK hnormal
        (finiteNormClass rationalIdeleClassRepresentation K L hLK b) =
      rationalFiniteNormTransferQuotientMap
        K L hLK hnormal
        (Additive.toMul
          ((rationalAbstractFixedFieldIdeleClassEquivFixed K).symm b))
def

rationalFiniteNormTransferCanonicalFiniteNormClassZero

L156 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormClassZero
Documentation

The named zero-class input for the canonical finite-norm transfer.

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
    quotientIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    quotientIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N
Lean source · statement
def rationalFiniteNormTransferCanonicalFiniteNormClassZero
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Prop

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.