NYLL
Module

CyclicNormTower.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicNormTower
5 declarations indexed from sourceView source ↗

Module documentation

Exact norm quotients in a cyclic tower

For a tower of cyclic Galois extensions, the first map in the concrete idele-class norm-quotient sequence is injective. Together with the already available right exactness, this gives the short exact norm sequence and its exact cardinal factorization.

Imports2
Imported by1

Declarations

theorem

cyclicNormTower_relativeClassGroupIsMulCommutative

L29 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicNormTower_relativeClassGroupIsMulCommutative
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open RelativeIdeleGroup.Cohomology
Lean source · statement
theorem cyclicNormTower_relativeClassGroupIsMulCommutative
    (A B : Type) [Field A] [NumberField A] [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B)
theorem

cyclicNormTower_ideleClassGroupIsMulCommutative

L36 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicNormTower_ideleClassGroupIsMulCommutative
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open RelativeIdeleGroup.Cohomology
attribute [local instance] cyclicNormTower_relativeClassGroupIsMulCommutative
Lean source · statement
theorem cyclicNormTower_ideleClassGroupIsMulCommutative
    (A : Type) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A)
theorem

intermediateToCompositeNormQuotient_injective_of_cyclicTower

L61 ↗
GlobalClassFieldTheory.GlobalClassFields.intermediateToCompositeNormQuotient_injective_of_cyclicTower
Documentation

In a cyclic Galois tower, the norm-induced map

C_M / N_{L/M} C_L → C_K / N_{L/K} C_L

is injective.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open RelativeIdeleGroup.Cohomology
attribute [local instance] cyclicNormTower_relativeClassGroupIsMulCommutative
attribute [local instance] cyclicNormTower_ideleClassGroupIsMulCommutative
variable
    (K M L : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois M L] [IsGalois K L]
    [IsCyclic (M ≃ₐ[K] M)]
    [IsCyclic (L ≃ₐ[M] L)]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem intermediateToCompositeNormQuotient_injective_of_cyclicTower :
    Function.Injective
      (intermediateToCompositeNormQuotient K M L)
theorem

cyclicTowerNormQuotient_shortExact

L177 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicTowerNormQuotient_shortExact
Documentation

The concrete norm-quotient sequence of a cyclic Galois tower is short exact: its first map is injective, its middle image is the final kernel, and its last map is surjective.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open RelativeIdeleGroup.Cohomology
attribute [local instance] cyclicNormTower_relativeClassGroupIsMulCommutative
attribute [local instance] cyclicNormTower_ideleClassGroupIsMulCommutative
variable
    (K M L : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois M L] [IsGalois K L]
    [IsCyclic (M ≃ₐ[K] M)]
    [IsCyclic (L ≃ₐ[M] L)]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem cyclicTowerNormQuotient_shortExact :
    Function.Injective
        (intermediateToCompositeNormQuotient K M L) ∧
      MonoidHom.range
          (intermediateToCompositeNormQuotient K M L) =
        MonoidHom.ker
          (compositeToBaseNormQuotient K M L) ∧
      Function.Surjective
        (compositeToBaseNormQuotient K M L)
theorem

cyclicTowerNormQuotient_card_eq_mul

L194 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclicTowerNormQuotient_card_eq_mul
Documentation

Orders in the cyclic tower norm sequence multiply exactly.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
open RelativeIdeleGroup.Cohomology
attribute [local instance] cyclicNormTower_relativeClassGroupIsMulCommutative
attribute [local instance] cyclicNormTower_ideleClassGroupIsMulCommutative
variable
    (K M L : Type)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois M L] [IsGalois K L]
    [IsCyclic (M ≃ₐ[K] M)]
    [IsCyclic (L ≃ₐ[M] L)]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem cyclicTowerNormQuotient_card_eq_mul :
    Nat.card (TowerCompositeClassNormQuotient K M L) =
      Nat.card (IntermediateClassNormQuotient K M L) *
        Nat.card (IdeleClassNormQuotient K M)

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