NYLL
Module

Tower.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.Tower
49 declarations indexed from sourceView source ↗

Module documentation

Idele-class norms in a field tower

For a tower K ⊂ M ⊂ L, keep the bottom field K fixed and write

𝔸_M = 𝔸_K ⊗[K] M, 𝔸_L = (𝔸_K ⊗[K] M) ⊗[M] L.

This gives an actual norm C_L → C_M whose composite with C_M → C_K is the tower norm. The resulting three concrete norm quotients form a natural right-exact sequence.

Imports3
Imported by10

Declarations

instance

relativeAdeleRingIntermediateAlgebra

L44 ↗
Documentation

The canonical right-factor M-algebra structure on 𝔸_K ⊗[K] M.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
instance (priority := 100)
    relativeAdeleRingIntermediateAlgebra :
    Algebra M (RelativeAdeleRing K M)
abbrev

TowerRelativeAdeleRing

L51 ↗
Documentation

The relative adele algebra of L, presented over the intermediate field while retaining the fixed bottom-field model of 𝔸_M.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
abbrev TowerRelativeAdeleRing
instance

relativeAdeleRingTopIntermediateAlgebra

L56 ↗
Documentation

The intermediate field acts on the one-step bottom-field model 𝔸_K ⊗[K] L through its embedding in L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
instance (priority := 100)
    relativeAdeleRingTopIntermediateAlgebra :
    Algebra M (RelativeAdeleRing K L)
def

intermediateAdeleInclusion

L66 ↗
Documentation

Extend the intermediate relative adele algebra along M → L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · full declaration
def intermediateAdeleInclusion :
    RelativeAdeleRing K M →ₐ[M]
      RelativeAdeleRing K L where
  __ :=
    (Algebra.TensorProduct.map
      (AlgHom.id
        (NumberField.AdeleRing (𝓞 K) K)
        (NumberField.AdeleRing (𝓞 K) K))
      (IsScalarTower.toAlgHom K M L)).toRingHom
  commutes' m := by
    change
      1 ⊗ₜ[K] algebraMap M L m =
        1 ⊗ₜ[K] algebraMap M L m
    rfl
theorem

intermediateAdeleInclusion_tmul

L84 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem intermediateAdeleInclusion_tmul
    (a : NumberField.AdeleRing (𝓞 K) K)
    (m : M) :
    intermediateAdeleInclusion K M L (a ⊗ₜ[K] m) =
      a ⊗ₜ[K] algebraMap M L m
def

topFieldToOneStep

L93 ↗
Documentation

The copy of L in the one-step relative adele algebra, regarded as an M-algebra map.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · full declaration
def topFieldToOneStep :
    L →ₐ[M] RelativeAdeleRing K L where
  __ :=
    (Algebra.TensorProduct.includeRight
      (R := K)
      (A := NumberField.AdeleRing (𝓞 K) K)
      (B := L)).toRingHom
  commutes' _ := rfl
theorem

topFieldToOneStep_apply

L106 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
omit [NumberField M] [NumberField L] [Algebra K M]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem topFieldToOneStep_apply
    (x : L) :
    topFieldToOneStep K M L x =
      (1 : NumberField.AdeleRing (𝓞 K) K) ⊗ₜ[K] x
def

towerRelativeAdeleRingEquiv

L118 ↗
Documentation

Canonical ring equivalence (𝔸_K ⊗[K] M) ⊗[M] L ≃+* 𝔸_K ⊗[K] L.

This is the standard tensor-product cancellation isomorphism: commute the two outer factors, commute the inner scalar extension, cancel the base change, and commute the remaining factors back.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def towerRelativeAdeleRingEquiv :
    TowerRelativeAdeleRing K M L ≃+*
      RelativeAdeleRing K L
def

towerRelativeAdeleFlatten

L144 ↗
Documentation

Flatten the iterated scalar extension (𝔸_K ⊗[K] M) ⊗[M] L to 𝔸_K ⊗[K] L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def towerRelativeAdeleFlatten :
    TowerRelativeAdeleRing K M L →ₐ[M]
      RelativeAdeleRing K L
theorem

towerRelativeAdeleFlatten_tmul

L160 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem towerRelativeAdeleFlatten_tmul
    (b : RelativeAdeleRing K M)
    (x : L) :
    towerRelativeAdeleFlatten K M L (b ⊗ₜ[M] x) =
      intermediateAdeleInclusion K M L b *
        topFieldToOneStep K M L x
def

bottomAdeleToTower

L179 ↗
Documentation

Embed the bottom adele algebra into the iterated tensor model.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def bottomAdeleToTower :
    NumberField.AdeleRing (𝓞 K) K →ₐ[K]
      TowerRelativeAdeleRing K M L
theorem

bottomAdeleToTower_apply

L193 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
omit [NumberField M] [NumberField L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem bottomAdeleToTower_apply
    (a : NumberField.AdeleRing (𝓞 K) K) :
    bottomAdeleToTower K M L a =
      (a ⊗ₜ[K] (1 : M)) ⊗ₜ[M] (1 : L)
def

topFieldToTower

L200 ↗
Documentation

Embed L into the iterated tensor model.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def topFieldToTower :
    L →ₐ[K] TowerRelativeAdeleRing K M L
theorem

topFieldToTower_apply

L232 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem topFieldToTower_apply
    (x : L) :
    topFieldToTower K M L x =
      (1 : RelativeAdeleRing K M) ⊗ₜ[M] x
def

towerRelativeAdeleUnflatten

L239 ↗
Documentation

Expand the one-step tensor model back to the iterated tower model.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def towerRelativeAdeleUnflatten :
    RelativeAdeleRing K L →ₐ[K]
      TowerRelativeAdeleRing K M L
theorem

towerRelativeAdeleUnflatten_tmul

L250 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem towerRelativeAdeleUnflatten_tmul
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L) :
    towerRelativeAdeleUnflatten K M L (a ⊗ₜ[K] x) =
      bottomAdeleToTower K M L a *
        topFieldToTower K M L x
def

towerRelativeAdeleAlgEquiv

L264 ↗
Documentation

The flattening equivalence as an equivalence over the bottom adele ring. This is the form needed for invariance of determinant norms.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def towerRelativeAdeleAlgEquiv :
    TowerRelativeAdeleRing K M L ≃ₐ[
      NumberField.AdeleRing (𝓞 K) K]
      RelativeAdeleRing K L
abbrev

TowerRelativeIdeleGroup

L279 ↗
Documentation

Unit group of the tower presentation of the relative adeles of L.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
abbrev TowerRelativeIdeleGroup
def

towerRelativeIdeleEquiv

L284 ↗
Documentation

The canonical equivalence from the tower presentation of the relative ideles of L to the one-step presentation over K.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
def towerRelativeIdeleEquiv :
    TowerRelativeIdeleGroup K M L ≃*
      RelativeIdeleGroup K L
instance

(anonymous instance)

L291 ↗
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
Lean source · statement
instance : IsMulCommutative (TowerRelativeIdeleGroup K M L)
instance

(anonymous instance)

L294 ↗
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L)
instance

(anonymous instance)

L297 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance : IsMulCommutative (IdeleClassGroup K)
def

principalIdele

L303 ↗
TowerRelativeIdeleGroup.principalIdele
Documentation

The diagonal copy of Lˣ in the tower relative idele group.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
Lean source · statement
def principalIdele :
    Lˣ →* TowerRelativeIdeleGroup K M L
theorem

towerRelativeIdeleEquiv_principalIdele

L314 ↗
TowerRelativeIdeleGroup.towerRelativeIdeleEquiv_principalIdele
Documentation

Flattening the tower presentation preserves the diagonal copy of Lˣ.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem towerRelativeIdeleEquiv_principalIdele
    (x : Lˣ) :
    towerRelativeIdeleEquiv K M L
        (principalIdele K M L x) =
      RelativeIdeleGroup.principalIdele K L x
def

principalSubgroup

L328 ↗
TowerRelativeIdeleGroup.principalSubgroup
Documentation

Principal ideles in the tower presentation.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
Lean source · statement
def principalSubgroup :
    Subgroup (TowerRelativeIdeleGroup K M L)
abbrev

ClassGroup

L333 ↗
TowerRelativeIdeleGroup.ClassGroup
Documentation

The idele class group of L in the tower presentation.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
Lean source · statement
abbrev ClassGroup
theorem

principalSubgroup_map_towerRelativeIdeleEquiv

L341 ↗
TowerRelativeIdeleGroup.principalSubgroup_map_towerRelativeIdeleEquiv
Documentation

The canonical equivalence maps tower principal ideles exactly onto the one-step principal-ideles subgroup.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem principalSubgroup_map_towerRelativeIdeleEquiv :
    (principalSubgroup K M L).map
        (towerRelativeIdeleEquiv K M L) =
      RelativeIdeleGroup.principalSubgroup K L
def

classGroupEquiv

L355 ↗
TowerRelativeIdeleGroup.classGroupEquiv
Documentation

Canonical equivalence between the tower and one-step presentations of the relative idele class group of L.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
Lean source · statement
def classGroupEquiv :
    ClassGroup K M L ≃*
      RelativeIdeleGroup.ClassGroup K L
theorem

classGroupEquiv_mk

L367 ↗
TowerRelativeIdeleGroup.classGroupEquiv_mk
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L]
    [FiniteDimensional K M] [FiniteDimensional M L] in
Lean source · statement
theorem classGroupEquiv_mk
    (a : TowerRelativeIdeleGroup K M L) :
    classGroupEquiv K M L
        (QuotientGroup.mk' (principalSubgroup K M L) a) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K L)
        (towerRelativeIdeleEquiv K M L a)
def

norm

L378 ↗
TowerRelativeIdeleGroup.norm
Documentation

Determinant norm from the tower presentation of 𝔸_L to 𝔸_M = 𝔸_K ⊗[K] M.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
Lean source · statement
def norm :
    TowerRelativeIdeleGroup K M L →*
      RelativeIdeleGroup K M
theorem

norm_transitive_flatten

L386 ↗
TowerRelativeIdeleGroup.norm_transitive_flatten
Documentation

Transitivity of determinant norms, after flattening the tower presentation to the one-step presentation.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L] in
Lean source · statement
theorem norm_transitive_flatten
    (a : TowerRelativeIdeleGroup K M L) :
    RelativeIdeleGroup.norm K M (norm K M L a) =
      RelativeIdeleGroup.norm K L
        (towerRelativeIdeleEquiv K M L a)
theorem

norm_fieldInclusion

L414 ↗
TowerRelativeIdeleGroup.norm_fieldInclusion
Documentation

Base change of the field norm from M to the relative adele algebra 𝔸_K ⊗[K] M.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional K M] in
Lean source · statement
theorem norm_fieldInclusion
    (x : L) :
    Algebra.norm (RelativeAdeleRing K M)
        (Algebra.TensorProduct.includeRight
          (R := M) (A := RelativeAdeleRing K M) (B := L) x) =
      algebraMap M (RelativeAdeleRing K M)
        (Algebra.norm M x)
theorem

norm_principalIdele

L438 ↗
TowerRelativeIdeleGroup.norm_principalIdele
Documentation

The tower idele norm carries a principal idele to the principal idele of the field norm.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional K M] in
Lean source · statement
theorem norm_principalIdele
    (x : Lˣ) :
    norm K M L (principalIdele K M L x) =
      RelativeIdeleGroup.principalIdele K M
        (Units.map (Algebra.norm M) x)
def

classNorm

L447 ↗
TowerRelativeIdeleGroup.classNorm
Documentation

The tower norm descended to actual idele class groups.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
Lean source · statement
def classNorm :
    ClassGroup K M L →*
      RelativeIdeleGroup.ClassGroup K M
theorem

classNorm_mk

L463 ↗
TowerRelativeIdeleGroup.classNorm_mk
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
namespace TowerRelativeIdeleGroup
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional K M] in
Lean source · statement
theorem classNorm_mk
    (a : TowerRelativeIdeleGroup K M L) :
    classNorm K M L
        (QuotientGroup.mk'
          (principalSubgroup K M L) a) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K M)
        (norm K M L a)
abbrev

IntermediateClassNormQuotient

L479 ↗
Documentation

The norm quotient C_M / N_{L/M} C_L in the fixed-bottom-field tower model.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
Lean source · statement
abbrev IntermediateClassNormQuotient
def

towerCompositeClassNorm

L484 ↗
Documentation

The composite class norm C_L → C_M → C_K in the tower model.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
Lean source · statement
def towerCompositeClassNorm :
    TowerRelativeIdeleGroup.ClassGroup K M L →*
      IdeleClassGroup K
theorem

towerCompositeClassNorm_eq_ideleClassNorm

L494 ↗
Documentation

After identifying the tower presentation with the one-step presentation, the composite tower norm is the ordinary class norm from L to K.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] in
Lean source · statement
theorem towerCompositeClassNorm_eq_ideleClassNorm
    (c : TowerRelativeIdeleGroup.ClassGroup K M L) :
    towerCompositeClassNorm K M L c =
      RelativeIdeleGroup.classNorm K L
        (TowerRelativeIdeleGroup.classGroupEquiv K M L c)
theorem

towerCompositeClassNorm_range_eq

L510 ↗
Documentation

The tower composite norm and the ordinary one-step norm have the same subgroup of norms in C_K.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] in
Lean source · statement
theorem towerCompositeClassNorm_range_eq :
    (towerCompositeClassNorm K M L).range =
      (RelativeIdeleGroup.classNorm K L).range
abbrev

TowerCompositeClassNormQuotient

L530 ↗
Documentation

The corresponding concrete quotient C_K / N_{L/K} C_L, before identifying the tower presentation of C_L with the one-step presentation.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
Lean source · statement
abbrev TowerCompositeClassNormQuotient
def

towerCompositeClassNormQuotientEquiv

L536 ↗
Documentation

Canonical identification of the tower composite norm quotient with the existing one-step norm quotient C_K / N_{L/K}C_L.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
Lean source · statement
def towerCompositeClassNormQuotientEquiv :
    TowerCompositeClassNormQuotient K M L ≃*
      RelativeIdeleGroup.ClassNormQuotient K L
def

intermediateToCompositeNormQuotient

L550 ↗
Documentation

The norm-induced first map

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

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
Lean source · statement
def intermediateToCompositeNormQuotient :
    IntermediateClassNormQuotient K M L →*
      TowerCompositeClassNormQuotient K M L
def

compositeToBaseNormQuotient

L565 ↗
Documentation

The quotient map

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

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
Lean source · statement
def compositeToBaseNormQuotient :
    TowerCompositeClassNormQuotient K M L →*
      RelativeIdeleGroup.ClassNormQuotient K M
theorem

intermediateToCompositeNormQuotient_mk

L579 ↗
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L] in
Lean source · statement
theorem intermediateToCompositeNormQuotient_mk
    (c : RelativeIdeleGroup.ClassGroup K M) :
    intermediateToCompositeNormQuotient K M L
        (QuotientGroup.mk'
          (TowerRelativeIdeleGroup.classNorm K M L).range c) =
      QuotientGroup.mk'
        (towerCompositeClassNorm K M L).range
        (RelativeIdeleGroup.classNorm K M c)
theorem

compositeToBaseNormQuotient_mk

L591 ↗
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L] in
Lean source · statement
theorem compositeToBaseNormQuotient_mk
    (c : IdeleClassGroup K) :
    compositeToBaseNormQuotient K M L
        (QuotientGroup.mk'
          (towerCompositeClassNorm K M L).range c) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.classNorm K M).range c
theorem

intermediateToCompositeNormQuotient_range_eq_ker

L602 ↗
Documentation

Exactness of the concrete tower norm-quotient sequence.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L] in
Lean source · statement
theorem intermediateToCompositeNormQuotient_range_eq_ker :
    MonoidHom.range
        (intermediateToCompositeNormQuotient K M L) =
      MonoidHom.ker
        (compositeToBaseNormQuotient K M L)
theorem

compositeToBaseNormQuotient_surjective

L638 ↗
Documentation

The last map in the tower norm-quotient sequence is onto.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L] in
Lean source · statement
theorem compositeToBaseNormQuotient_surjective :
    Function.Surjective
      (compositeToBaseNormQuotient K M L)
theorem

towerCompositeClassNormQuotient_card_le_mul

L657 ↗
Documentation

Cardinal bound supplied by the actual right-exact tower sequence:

#(C_K / N_{L/K}C_L) ≤ #(C_M / N_{L/M}C_L) · #(C_K / N_{M/K}C_M).

Only finiteness of the two outer quotients is required; finiteness of the middle quotient is constructed from exactness.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L] in
Lean source · statement
theorem towerCompositeClassNormQuotient_card_le_mul
    [Finite (IntermediateClassNormQuotient K M L)]
    [Finite (RelativeIdeleGroup.ClassNormQuotient K M)] :
    Nat.card (TowerCompositeClassNormQuotient K M L) ≤
      Nat.card (IntermediateClassNormQuotient K M L) *
        Nat.card (RelativeIdeleGroup.ClassNormQuotient K M)
theorem

ideleClassNormQuotient_card_le_mul

L709 ↗
Documentation

The tower cardinal bound in the standard one-step presentation:

#(C_K / N_{L/K}C_L) ≤ #(C_M / N_{L/M}C_L) · #(C_K / N_{M/K}C_M).

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
universe u
variable
    (K M L : Type u)
    [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]
local instance : IsMulCommutative (TowerRelativeIdeleGroup K M L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (RelativeIdeleGroup.ClassGroup K L) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance : IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormQuotientSequence
omit [NumberField M] in
Lean source · statement
theorem ideleClassNormQuotient_card_le_mul
    [Finite (IntermediateClassNormQuotient K M L)]
    [Finite (RelativeIdeleGroup.ClassNormQuotient K M)] :
    Nat.card (RelativeIdeleGroup.ClassNormQuotient K L) ≤
      Nat.card (IntermediateClassNormQuotient K M L) *
        Nat.card (RelativeIdeleGroup.ClassNormQuotient K M)

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