Module

FieldSpine.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.FieldSpine

19 declarations indexed from sourceView source ↗

Module documentation

Fixed-field instance spine for rational finite-norm transport

This leaf names the finite-dimensional, scalar-tower, number-field, Galois, and quotient instances reused by the rational finite-norm transport modules. The public dependent type aliases are compiled once here.

Imports2

Imported by4

theorem

ideleClassGroupIsMulCommutative

L36 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative

Documentation

Shared commutativity proof for ordinary idèle class groups.

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
namespace RationalFiniteNormTransferInternal

Lean source · statement

theorem ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

fieldSpineIdeleClassGroupIsMulCommutative

L41 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.fieldSpineIdeleClassGroupIsMulCommutative

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
namespace RationalFiniteNormTransferInternal

Lean source · statement

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

theorem

ideleClassSubgroupNormal

L48 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.ideleClassSubgroupNormal

Documentation

Shared normality proof for subgroups of ordinary idèle class groups.

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

Lean source · statement

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

instance

fieldSpineIdeleClassSubgroupNormal

L53 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.fieldSpineIdeleClassSubgroupNormal

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

Lean source · statement

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

def

absoluteAlgebra

L60 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.absoluteAlgebra

Documentation

The canonical absolute algebra structure on a rational relative fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

def absoluteAlgebra
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    Algebra ℚ
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

theorem

absoluteFinite

L68 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.absoluteFinite

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem absoluteFinite
    (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)] :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          L (le_baseField L))

theorem

fixedFiniteDimensional

L102 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.fixedFiniteDimensional

Documentation

The finite-dimensional structure on a rational abstract fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem fixedFiniteDimensional
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))] :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K)

theorem

relativeFiniteDimensional

L119 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.relativeFiniteDimensional

Documentation

The relative finite-dimensional structure on the fixed-field extension attached to an inclusion of closed subgroups.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem relativeFiniteDimensional
    (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)] :
    FiniteDimensional
      (abstractFixedField ℚ (SeparableClosure ℚ) K)
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

theorem

relativeScalarTower

L139 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.relativeScalarTower

Documentation

The canonical scalar tower on a rational relative fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem relativeScalarTower
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    IsScalarTower ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K)
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

theorem

relativeAbsoluteFiniteDimensional

L149 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.relativeAbsoluteFiniteDimensional

Documentation

Absolute finite-dimensionality of a rational relative fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem relativeAbsoluteFiniteDimensional
    (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)] :
    FiniteDimensional ℚ
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

theorem

fixedNumberField

L172 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.fixedNumberField

Documentation

The number-field structure on a rational abstract fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem fixedNumberField
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))] :
    NumberField (abstractFixedField ℚ (SeparableClosure ℚ) K)

theorem

relativeNumberField

L188 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.relativeNumberField

Documentation

The number-field structure on a rational relative fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem relativeNumberField
    (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)] :
    NumberField
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

theorem

relativeIsGalois

L209 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.relativeIsGalois

Documentation

The Galois structure on a normal rational relative fixed field.

Source context 11 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
namespace RationalFiniteNormTransferInternal
local instance
    fieldSpineIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ideleClassGroupIsMulCommutative
local instance
    fieldSpineIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  ideleClassSubgroupNormal N

Lean source · statement

theorem relativeIsGalois
    (K L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    IsGalois
      (abstractFixedField ℚ (SeparableClosure ℚ) K)
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLK)

instance

fieldSpinePublicIdeleClassGroupIsMulCommutative

L222 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.fieldSpinePublicIdeleClassGroupIsMulCommutative

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

instance

fieldSpinePublicIdeleClassSubgroupNormal

L228 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.fieldSpinePublicIdeleClassSubgroupNormal

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

Lean source · statement

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

abbrev

rationalFiniteNormTransferBaseIdeleClass

L236 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferBaseIdeleClass

Documentation

The fixed-field idele-class type used as the domain of 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
    fieldSpinePublicIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    fieldSpinePublicIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

abbrev rationalFiniteNormTransferBaseIdeleClass
    (K : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))] : Type

abbrev

rationalFiniteNormTransferQuotientTarget

L255 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferQuotientTarget

Documentation

The additive ordinary idele-class norm quotient used as the target of 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
    fieldSpinePublicIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    fieldSpinePublicIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

abbrev rationalFiniteNormTransferQuotientTarget
    (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)] : Type

def

quotientTargetZero

L299 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferInternal.quotientTargetZero

Documentation

The canonical additive zero on the named finite-norm transfer target. Naming this instance prevents repeated typeclass reduction of the dependent fixed-field quotient.

Source context 11 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
    fieldSpinePublicIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    fieldSpinePublicIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N
namespace RationalFiniteNormTransferInternal

Lean source · statement

def quotientTargetZero
    (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)] :
    Zero (rationalFiniteNormTransferQuotientTarget
      K L hLK hnormal)

abbrev

rationalFiniteNormTransferExtensionIdeleClass

L345 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferExtensionIdeleClass

Documentation

The ordinary idele-class type of the upper fixed field in a rational 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
    fieldSpinePublicIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    fieldSpinePublicIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

abbrev rationalFiniteNormTransferExtensionIdeleClass
    (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)] : Type

Module documentation

Fixed-field instance spine for rational finite-norm transport

Declarations