Module

ZeroTransport.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.ZeroTransport

8 declarations indexed from sourceView source ↗

Module documentation

Zero-class transport to norm membership

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

Imports3

Imported by2

instance

zeroTransportIdeleClassGroupIsMulCommutative

L33 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.zeroTransportIdeleClassGroupIsMulCommutative

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

zeroTransportIdeleClassSubgroupNormal

L39 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.zeroTransportIdeleClassSubgroupNormal

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative

Lean source · statement

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

def

rationalFiniteNormTransferCanonicalFiniteNormClassZero_implies_finiteNormRepresentativeQuotientZero

L46 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormClassZero_implies_finiteNormRepresentativeQuotientZero

Documentation

Internal finite-norm-class-zero to quotient-zero step.

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    zeroTransportIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
rationalFiniteNormTransferCanonicalFiniteNormClassZero_implies_finiteNormRepresentativeQuotientZero
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hincludeCanonical :
      rationalFiniteNormTransferCanonicalFiniteNormClassZero
        K H L hHK hLH c) :
    RationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZeroData
      K H L hHK hLH hLHnormal c

def

rationalFiniteNormTransferFiniteNormRepresentativeQuotientZero_implies_targetZero

L122 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferFiniteNormRepresentativeQuotientZero_implies_targetZero

Documentation

Internal evaluation of the quotient equivalence at zero.

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    zeroTransportIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferFiniteNormRepresentativeQuotientZero_implies_targetZero
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hincludeCanonical :
      rationalFiniteNormTransferCanonicalFiniteNormClassZero
        K H L hHK hLH c) :
    RationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZeroData
      (hKfinite := hKfinite) (hKHfinite := hKHfinite)
      (hHLfinite := hHLfinite)
      K H L hHK hLH hLHnormal c

def

rationalFiniteNormTransferFiniteNormRepresentativeTargetZero_implies_membership

L188 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferFiniteNormRepresentativeTargetZero_implies_membership

Documentation

Internal quotient-target zero to absolute norm-membership step.

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    zeroTransportIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferFiniteNormRepresentativeTargetZero_implies_membership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hincludeCanonical :
      rationalFiniteNormTransferCanonicalFiniteNormClassZero
        K H L hHK hLH c) :
    RationalFiniteNormTransferCanonicalFiniteNormRepresentativeMembershipData
      (hKfinite := hKfinite) (hKHfinite := hKHfinite)
      (hHLfinite := hHLfinite)
      K H L hHK hLH hLHnormal c

def

rationalFiniteNormTransferFiniteNormRepresentativeMembership_implies_canonicalAbsoluteMembership

L273 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferFiniteNormRepresentativeMembership_implies_canonicalAbsoluteMembership

Documentation

Internal replacement of the absolute finite-norm representative by the canonical ordinary extension 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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    zeroTransportIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferFiniteNormRepresentativeMembership_implies_canonicalAbsoluteMembership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hincludeCanonical :
      rationalFiniteNormTransferCanonicalFiniteNormClassZero
        K H L hHK hLH c) :
    RationalFiniteNormTransferCanonicalAbsoluteNormMembershipData
      (hKfinite := hKfinite) (hKHfinite := hKHfinite)
      (hHLfinite := hHLfinite)
      K H L hHK hLH hHKnormal hLHnormal c

theorem

rationalFiniteNormTransferCanonicalAbsoluteMembership_implies_relativeMembership

L346 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalAbsoluteMembership_implies_relativeMembership

Documentation

Internal transport of the canonical absolute norm membership to the relative ordinary-extension field spine.

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    zeroTransportIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

theorem
    rationalFiniteNormTransferCanonicalAbsoluteMembership_implies_relativeMembership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hincludeCanonical :
      rationalFiniteNormTransferCanonicalFiniteNormClassZero
        K H L hHK hLH c) :
    rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
      K H L hHK hLH hHKnormal hLHnormal c

theorem

rationalFiniteNormTransferCanonicalFiniteNormClassZero_implies_normMembership

L433 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormClassZero_implies_normMembership

Documentation

A zero canonical finite-norm class forces the ordinary idele class extended to the intermediate fixed field to lie in the relative norm range.

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
    zeroTransportIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    zeroTransportIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

theorem
    rationalFiniteNormTransferCanonicalFiniteNormClassZero_implies_normMembership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hincludeCanonical :
      rationalFiniteNormTransferCanonicalFiniteNormClassZero
        K H L hHK hLH c) :
    rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
      K H L hHK hLH hHKnormal hLHnormal c

Module documentation

Zero-class transport to norm membership

Declarations