Module

NormComparison.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.NormComparison

8 declarations indexed from sourceView source ↗

Module documentation

Relative and ordinary idele-class norms

The determinant norm on relative ideles and the ordinary idele norm give the same map after the canonical scalar-extension equivalence C(𝔸_K ⊗_K L) ≃ C_L. This comparison lets the cohomological results proved in relative coordinates be stated with the usual norm N_{L/K} : C_L → C_K.

Imports4

Imported by10

def

classEmbedding

L42 ↗

RelativeIdeleGroup.classEmbedding

Documentation

A field embedding into an ambient finite extension, descended from relative ideles to the existing relative idele class groups.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]

Lean source · statement

def classEmbedding
    (f : L →ₐ[K] M) :
    RelativeIdeleGroup.ClassGroup K L →*
      RelativeIdeleGroup.ClassGroup K M

theorem

classEmbedding_mk

L58 ↗

RelativeIdeleGroup.classEmbedding_mk

Source context 7 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
omit [FiniteDimensional K L] [FiniteDimensional K M] in

Lean source · statement

theorem classEmbedding_mk
    (f : L →ₐ[K] M)
    (a : RelativeIdeleGroup K L) :
    classEmbedding f
        (QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K M)
        (RelativeIdeleGroup.ideleEmbedding f a)

theorem

classInclusion_ideleClassNorm_eq_prod_conjugates

L70 ↗

RelativeIdeleGroup.classInclusion_ideleClassNorm_eq_prod_conjugates

Documentation

The Galois product formula after descent to relative idele classes.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]

Lean source · statement

theorem classInclusion_ideleClassNorm_eq_prod_conjugates
    [IsGalois K L]
    (c : RelativeIdeleGroup.ClassGroup K L) :
    RelativeIdeleGroup.classInclusion K L
        (RelativeIdeleGroup.classNorm K L c) =
      ∏ σ : L ≃ₐ[K] L, σ • c

instance

fixingSubextensionQuotientFintype

L96 ↗

RelativeIdeleGroup.fixingSubextensionQuotientFintype

Source context 7 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
variable [Algebra L M] [IsScalarTower K L M] [IsGalois K M]

Lean source · statement

instance fixingSubextensionQuotientFintype :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        RelativeIdeleGroup.fixingSubextension
          (K := K) (L := L) (M := M))

theorem

classInclusion_ideleClassNorm_eq_prod_embeddings

L105 ↗

RelativeIdeleGroup.classInclusion_ideleClassNorm_eq_prod_embeddings

Documentation

The embedded-subextension norm formula after descent to relative idele classes. No normality of L / K is assumed.

Source context 8 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
variable [Algebra L M] [IsScalarTower K L M] [IsGalois K M]
local instance fixingSubextensionQuotientFintype :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        RelativeIdeleGroup.fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _

Lean source · statement

theorem classInclusion_ideleClassNorm_eq_prod_embeddings
    (c : RelativeIdeleGroup.ClassGroup K L) :
    RelativeIdeleGroup.classInclusion K M
        (RelativeIdeleGroup.classNorm K L c) =
      ∏ f : L →ₐ[K] M,
        RelativeIdeleGroup.classEmbedding f c

theorem

classInclusion_ideleClassNorm_eq_prod_galoisCosets

L132 ↗

RelativeIdeleGroup.classInclusion_ideleClassNorm_eq_prod_galoisCosets

Documentation

Coset form of the embedded-subextension norm formula on relative idele classes.

Source context 8 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
variable [Algebra L M] [IsScalarTower K L M] [IsGalois K M]
local instance fixingSubextensionQuotientFintype :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        RelativeIdeleGroup.fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _

Lean source · statement

theorem classInclusion_ideleClassNorm_eq_prod_galoisCosets
    (c : RelativeIdeleGroup.ClassGroup K L) :
    RelativeIdeleGroup.classInclusion K M
        (RelativeIdeleGroup.classNorm K L c) =
      ∏ q :
          (M ≃ₐ[K] M) ⧸
            RelativeIdeleGroup.fixingSubextension
              (K := K) (L := L) (M := M),
        RelativeIdeleGroup.classEmbedding
          (RelativeIdeleGroup.cosetEquivEmbedding q) c

theorem

ordinaryIdeleClassNorm_relativeIdeleClassBaseChange

L172 ↗

Documentation

The relative determinant norm is the ordinary idele-class norm after the canonical base-change equivalence.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    {K L : Type*}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem ordinaryIdeleClassNorm_relativeIdeleClassBaseChange
    (c : RelativeIdeleGroup.ClassGroup K L) :
    _root_.ideleClassNorm K L
        (relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := L) c) =
      RelativeIdeleGroup.classNorm K L c

theorem

ordinaryIdeleClassNorm_range_eq_relative

L194 ↗

Documentation

The ordinary and relative presentations define the same norm subgroup of C_K.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
variable
    {K L : Type*}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem ordinaryIdeleClassNorm_range_eq_relative :
    (_root_.ideleClassNorm K L).range =
      (RelativeIdeleGroup.classNorm K L).range

Module documentation

Relative and ordinary idele-class norms

Declarations