NYLL
Module

BaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.BaseChange
24 declarations indexed from sourceView source ↗

Module documentation

Base change of idele-class norms along a pushout square

For a pushout square of finite extensions

K  ─→  M
│       │
↓       ↓
L  ─→  N

this file constructs the maps on relative ideles and idele classes that occur after adjoining roots of unity. Keeping the bottom adele ring fixed makes the norm square an actual determinant-norm base-change identity.

Imports3
Imported by7

Declarations

instance

(anonymous instance)

L53 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
Lean source · statement
instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C)
instance

(anonymous instance)

L58 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B)
instance

(anonymous instance)

L63 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A)
abbrev

BaseChangedRelativeAdeleRing

L70 ↗
Documentation

The scalar extension of the one-step K-presentation of the relative adeles of L from the bottom adele ring to 𝔸_K ⊗[K] M.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
abbrev BaseChangedRelativeAdeleRing
def

pushoutTowerAdeleEquiv

L81 ↗
Documentation

For a pushout N = M ⊗[K] L, the tower presentation

(𝔸_K ⊗[K] M) ⊗[M] N

is canonically the scalar extension

(𝔸_K ⊗[K] M) ⊗[K] L.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def pushoutTowerAdeleEquiv :
    TowerRelativeAdeleRing K M N ≃ₐ[
      RelativeAdeleRing K M]
      BaseChangedRelativeAdeleRing K M L
def

baseChangedRelativeAdeleMap

L110 ↗
Documentation

Scalar extension of coefficients from the bottom adele ring to 𝔸_K ⊗[K] M, while retaining the top field L.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def baseChangedRelativeAdeleMap :
    RelativeAdeleRing K L →ₐ[K]
      BaseChangedRelativeAdeleRing K M L
def

pushoutTowerAdeleInclusion

L122 ↗
Documentation

Inclusion from the relative adeles of L/K to the tower presentation of the relative adeles of N/M, induced by the pushout square.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def pushoutTowerAdeleInclusion :
    RelativeAdeleRing K L →+*
      TowerRelativeAdeleRing K M N
theorem

pushoutTowerAdeleInclusion_tmul

L132 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [NumberField N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N] in
Lean source · statement
theorem pushoutTowerAdeleInclusion_tmul
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L) :
    pushoutTowerAdeleInclusion K M L N (a ⊗ₜ[K] x) =
      (a ⊗ₜ[K] (1 : M)) ⊗ₜ[M]
        algebraMap L N x
def

pushoutTowerIdeleInclusion

L158 ↗
Documentation

Inclusion on unit groups induced by a pushout square of fields.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def pushoutTowerIdeleInclusion :
    RelativeIdeleGroup K L →*
      TowerRelativeIdeleGroup K M N
theorem

pushoutTowerIdeleInclusion_principalIdele

L169 ↗
Documentation

The pushout inclusion sends a principal idele of L to the principal idele of its image in N.

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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [NumberField N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N] in
Lean source · statement
theorem pushoutTowerIdeleInclusion_principalIdele
    (x : Lˣ) :
    pushoutTowerIdeleInclusion K M L N
        (RelativeIdeleGroup.principalIdele K L x) =
      TowerRelativeIdeleGroup.principalIdele K M N
        (Units.map (algebraMap L N) x)
theorem

pushoutTowerIdeleNorm_inclusion

L189 ↗
Documentation

Determinant norms commute with the pushout inclusion. This is the idele-level norm square used after adjoining roots of unity.

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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [NumberField N]
    [FiniteDimensional K M] [FiniteDimensional M N]
    [FiniteDimensional L N] in
Lean source · statement
theorem pushoutTowerIdeleNorm_inclusion
    (a : RelativeIdeleGroup K L) :
    TowerRelativeIdeleGroup.norm K M N
        (pushoutTowerIdeleInclusion K M L N a) =
      RelativeIdeleGroup.inclusion K M
        (RelativeIdeleGroup.norm K L a)
def

pushoutTowerClassInclusion

L230 ↗
Documentation

The pushout inclusion descended to relative idele class groups.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def pushoutTowerClassInclusion :
    RelativeIdeleGroup.ClassGroup K L →*
      TowerRelativeIdeleGroup.ClassGroup K M N
theorem

pushoutTowerClassInclusion_mk

L248 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [NumberField N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N] in
Lean source · statement
theorem pushoutTowerClassInclusion_mk
    (a : RelativeIdeleGroup K L) :
    pushoutTowerClassInclusion K M L N
        (QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a) =
      QuotientGroup.mk'
        (TowerRelativeIdeleGroup.principalSubgroup K M N)
        (pushoutTowerIdeleInclusion K M L N a)
theorem

pushoutTowerClassNorm_inclusion

L262 ↗
Documentation

The determinant-norm square after adjoining the pushout field, descended to actual relative 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [NumberField N]
    [FiniteDimensional K M] [FiniteDimensional L N] in
Lean source · statement
theorem pushoutTowerClassNorm_inclusion
    (c : RelativeIdeleGroup.ClassGroup K L) :
    TowerRelativeIdeleGroup.classNorm K M N
        (pushoutTowerClassInclusion K M L N c) =
      RelativeIdeleGroup.classInclusion K M
        (RelativeIdeleGroup.classNorm K L c)
def

pushoutNormQuotientMap

L286 ↗
Documentation

The map on degree-zero class-norm quotients induced by the pushout inclusion.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def pushoutNormQuotientMap :
    RelativeIdeleGroup.ClassNormQuotient K L →*
      IntermediateClassNormQuotient K M N
theorem

pushoutNormQuotientMap_mk

L302 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [NumberField N]
    [FiniteDimensional K M] [FiniteDimensional L N] in
Lean source · statement
theorem pushoutNormQuotientMap_mk
    (c : IdeleClassGroup K) :
    pushoutNormQuotientMap K M L N
        (QuotientGroup.mk' (RelativeIdeleGroup.classNorm K L).range c) =
      QuotientGroup.mk'
        (TowerRelativeIdeleGroup.classNorm K M N).range
        (RelativeIdeleGroup.classInclusion K M c)
theorem

ideleClassNorm_classInclusion

L314 ↗
Documentation

Norm followed by class inclusion is the extension-degree power on the base idele class 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] in
Lean source · statement
theorem ideleClassNorm_classInclusion
    (c : IdeleClassGroup K) :
    RelativeIdeleGroup.classNorm K M
        (RelativeIdeleGroup.classInclusion K M c) =
      c ^ Module.finrank K M
def

changeIntermediateClassGroupEquiv

L334 ↗
Documentation

Change the chosen intermediate field in the tower presentation of the relative idele class group of N, keeping the bottom field K fixed.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def changeIntermediateClassGroupEquiv :
    TowerRelativeIdeleGroup.ClassGroup K M N ≃*
      TowerRelativeIdeleGroup.ClassGroup K L N
theorem

towerCompositeClassNorm_changeIntermediate

L343 ↗
Documentation

Changing the intermediate tower presentation does not change the composite class norm to K.

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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [Algebra.IsPushout K M L N] in
Lean source · statement
theorem towerCompositeClassNorm_changeIntermediate
    (c : TowerRelativeIdeleGroup.ClassGroup K M N) :
    towerCompositeClassNorm K L N
        (changeIntermediateClassGroupEquiv K M L N c) =
      towerCompositeClassNorm K M N c
theorem

towerCompositeClassNorm_mem_ideleClassNormRange

L355 ↗
Documentation

Every composite norm through M is, after changing the tower presentation, already a norm through 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [Algebra.IsPushout K M L N] in
Lean source · statement
theorem towerCompositeClassNorm_mem_ideleClassNormRange
    (c : TowerRelativeIdeleGroup.ClassGroup K M N) :
    towerCompositeClassNorm K M N c ∈
      (RelativeIdeleGroup.classNorm K L).range
def

pushoutNormQuotientNormBack

L367 ↗
Documentation

Norm back from the pushout target quotient to the original class-norm quotient.

Source context 8 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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def pushoutNormQuotientNormBack :
    IntermediateClassNormQuotient K M N →*
      RelativeIdeleGroup.ClassNormQuotient K L
theorem

pushoutNormQuotientNormBack_mk

L382 ↗
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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] [Algebra.IsPushout K M L N] in
Lean source · statement
theorem pushoutNormQuotientNormBack_mk
    (c : RelativeIdeleGroup.ClassGroup K M) :
    pushoutNormQuotientNormBack K M L N
        (QuotientGroup.mk'
          (TowerRelativeIdeleGroup.classNorm K M N).range c) =
      QuotientGroup.mk' (RelativeIdeleGroup.classNorm K L).range
        (RelativeIdeleGroup.classNorm K M c)
theorem

pushoutNormQuotientNormBack_comp_map

L394 ↗
Documentation

The norm-back composite is the [M:K]-power map on the original class-norm quotient.

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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] in
Lean source · statement
theorem pushoutNormQuotientNormBack_comp_map
    (q : RelativeIdeleGroup.ClassNormQuotient K L) :
    pushoutNormQuotientNormBack K M L N
        (pushoutNormQuotientMap K M L N q) =
      q ^ Module.finrank K M
theorem

pushoutNormQuotientMap_injective_of_pow_injective

L412 ↗
Documentation

If the [M:K]-power map on the original norm quotient is injective, then so is the map induced by the pushout inclusion.

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 N : Type u)
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Field N] [NumberField N]
    [Algebra K M] [Algebra K L]
    [Algebra M N] [Algebra L N] [Algebra K N]
    [IsScalarTower K M N] [IsScalarTower K L N]
    [Algebra.IsPushout K M L N]
    [FiniteDimensional K M] [FiniteDimensional K L]
    [FiniteDimensional M N] [FiniteDimensional L N]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance (A B C : Type u) [Field A] [NumberField A]
    [Field B] [Field C] [Algebra A B] [Algebra B C] :
    IsMulCommutative (TowerRelativeIdeleGroup A B C) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField M] [NumberField L] in
Lean source · full declaration
theorem pushoutNormQuotientMap_injective_of_pow_injective
    (hpow :
      Function.Injective
        (fun q : RelativeIdeleGroup.ClassNormQuotient K L =>
          q ^ Module.finrank K M)) :
    Function.Injective (pushoutNormQuotientMap K M L N) := by
  intro x y hxy
  apply hpow
  change
    x ^ Module.finrank K M =
      y ^ Module.finrank K M
  rw [← pushoutNormQuotientNormBack_comp_map K M L N x,
    ← pushoutNormQuotientNormBack_comp_map K M L N y,
    hxy]

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