Module

TowerBaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.TowerBaseChange

38 declarations indexed from sourceView source ↗

Module documentation

The fixed-bottom tower model and the actual intermediate-field model

For a tower K ⊂ M ⊂ L, IdeleClassTower presents the ideles of L as units of (𝔸_K ⊗[K] M) ⊗[M] L. Here we compare that presentation with the actual relative idele group 𝔸_M ⊗[M] L, by passing through the ordinary ideles of L.

Imports2

Imported by11

instance

towerBaseChange_towerRelativeIdeleGroupIsMulCommutative

L41 ↗

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.

Lean source · statement

instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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

towerBaseChange_relativeIdeleClassGroupIsMulCommutative

L48 ↗

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (A B : Type u) [Field A] [NumberField A]
    [Field B] [Algebra A B] :
    IsMulCommutative (RelativeIdeleGroup.ClassGroup A B)

instance

towerBaseChange_ideleClassGroupIsMulCommutative

L55 ↗

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A)

def

intermediateRelativeAdeleBaseChangeAlgEquiv

L64 ↗

Documentation

The ring-level relative-to-ordinary comparison, regarded as an equivalence of M-algebras.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison

Lean source · statement

def intermediateRelativeAdeleBaseChangeAlgEquiv :
    RelativeAdeleRing K M ≃ₐ[M]
      NumberField.AdeleRing (𝓞 M) M

def

towerActualRelativeAdeleRingEquiv

L82 ↗

Documentation

Extend the intermediate adele-ring comparison along M → L.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison

Lean source · statement

def towerActualRelativeAdeleRingEquiv :
    TowerRelativeAdeleRing K M L ≃+*
      RelativeAdeleRing M L

theorem

towerActualRelativeAdeleRingEquiv_tmul

L92 ↗

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerActualRelativeAdeleRingEquiv_tmul
    (b : RelativeAdeleRing K M)
    (x : L) :
    towerActualRelativeAdeleRingEquiv K M L (b ⊗ₜ[M] x) =
      intermediateRelativeAdeleBaseChangeAlgEquiv K M b ⊗ₜ[M] x

theorem

towerActualRelativeAdeleRingEquiv_unflatten_conjugation

L103 ↗

Documentation

Passing from the fixed-bottom tower presentation to the actual relative adele ring over the intermediate field intertwines conjugation by an automorphism of the top field.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison
omit [NumberField L] [FiniteDimensional M L] in

Lean source · statement

theorem towerActualRelativeAdeleRingEquiv_unflatten_conjugation
    (σ : L ≃ₐ[M] L)
    (z : RelativeAdeleRing K L) :
    towerActualRelativeAdeleRingEquiv K M L
        (towerRelativeAdeleUnflatten K M L
          (RelativeIdeleGroup.conjugation K L
            (σ.restrictScalars K) z)) =
      RelativeIdeleGroup.conjugation M L σ
        (towerActualRelativeAdeleRingEquiv K M L
          (towerRelativeAdeleUnflatten K M L z))

theorem

relativeAdeleBaseChangeRingEquiv_tower_finiteComponent

L123 ↗

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison

Lean source · statement

theorem relativeAdeleBaseChangeRingEquiv_tower_finiteComponent
    (z : TowerRelativeAdeleRing K M L)
    (W : HeightOneSpectrum (𝓞 L)) :
    (relativeAdeleBaseChangeRingEquiv
        (K := M) (L := L)
        (towerActualRelativeAdeleRingEquiv K M L z)).2 W =
      (relativeAdeleBaseChangeRingEquiv
        (K := K) (L := L)
        (towerRelativeAdeleRingEquiv K M L z)).2 W

theorem

relativeAdeleBaseChangeRingEquiv_tower_infiniteComponent

L236 ↗

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison

Lean source · statement

theorem relativeAdeleBaseChangeRingEquiv_tower_infiniteComponent
    (z : TowerRelativeAdeleRing K M L)
    (W : InfinitePlace L) :
    (relativeAdeleBaseChangeRingEquiv
        (K := M) (L := L)
        (towerActualRelativeAdeleRingEquiv K M L z)).1 W =
      (relativeAdeleBaseChangeRingEquiv
        (K := K) (L := L)
        (towerRelativeAdeleRingEquiv K M L z)).1 W

theorem

relativeAdeleBaseChangeRingEquiv_tower

L368 ↗

Documentation

Passing from the fixed-bottom tower presentation to ordinary adeles is independent of whether one first changes to the actual relative presentation over the intermediate field.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section RingComparison

Lean source · statement

theorem relativeAdeleBaseChangeRingEquiv_tower
    (z : TowerRelativeAdeleRing K M L) :
    relativeAdeleBaseChangeRingEquiv
        (K := M) (L := L)
        (towerActualRelativeAdeleRingEquiv K M L z) =
      relativeAdeleBaseChangeRingEquiv
        (K := K) (L := L)
        (towerRelativeAdeleRingEquiv K M L z)

def

towerRelativeIdeleViaOrdinaryMulEquiv

L395 ↗

Documentation

The comparison through ordinary ideles, recording the compatibility with the original fixed-bottom flattening construction.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
section ViaOrdinary

Lean source · statement

def towerRelativeIdeleViaOrdinaryMulEquiv :
    TowerRelativeIdeleGroup K M L ≃*
      RelativeIdeleGroup M L

theorem

towerRelativeIdeleViaOrdinaryMulEquiv_apply

L406 ↗

Source context 12 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
section ViaOrdinary
omit [FiniteDimensional K M] in

Lean source · statement

theorem towerRelativeIdeleViaOrdinaryMulEquiv_apply
    (a : TowerRelativeIdeleGroup K M L) :
    towerRelativeIdeleViaOrdinaryMulEquiv K M L a =
      (relativeIdeleBaseChangeMulEquiv
        (K := M) (L := L)).symm
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L)
          (towerRelativeIdeleEquiv K M L a))

def

towerRelativeIdeleBaseChangeMulEquiv

L421 ↗

Documentation

The fixed-bottom tower presentation of the ideles of L is canonically equivalent to the actual relative idele group over M, using the underlying adele-ring scalar-extension equivalence.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison

Lean source · statement

def towerRelativeIdeleBaseChangeMulEquiv :
    TowerRelativeIdeleGroup K M L ≃*
      RelativeIdeleGroup M L

theorem

towerRelativeIdeleBaseChangeMulEquiv_eq_viaOrdinary

L429 ↗

Documentation

The ring-level tower coherence identifies the direct tower-to-actual comparison with the comparison through ordinary ideles.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_eq_viaOrdinary
    (a : TowerRelativeIdeleGroup K M L) :
    towerRelativeIdeleBaseChangeMulEquiv K M L a =
      towerRelativeIdeleViaOrdinaryMulEquiv K M L a

theorem

relativeIdeleBaseChangeMulEquiv_tower

L451 ↗

Documentation

Scalar extension from the tower presentation to ordinary ideles is the same along the direct and intermediate-field routes.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison

Lean source · statement

theorem relativeIdeleBaseChangeMulEquiv_tower
    (a : TowerRelativeIdeleGroup K M L) :
    relativeIdeleBaseChangeMulEquiv
        (K := M) (L := L)
        (towerRelativeIdeleBaseChangeMulEquiv K M L a) =
      relativeIdeleBaseChangeMulEquiv
        (K := K) (L := L)
        (towerRelativeIdeleEquiv K M L a)

theorem

towerRelativeIdeleBaseChangeMulEquiv_principalIdele

L468 ↗

Documentation

The comparison preserves the diagonal copy of Lˣ.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_principalIdele
    (x : Lˣ) :
    towerRelativeIdeleBaseChangeMulEquiv K M L
        (TowerRelativeIdeleGroup.principalIdele K M L x) =
      RelativeIdeleGroup.principalIdele M L x

theorem

towerRelativeIdeleBaseChangeMulEquiv_unflatten_conjugation

L484 ↗

Documentation

The tower-to-actual comparison transports the restricted bottom-field conjugation to conjugation over the intermediate field.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
omit [NumberField L] [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_unflatten_conjugation
    (σ : L ≃ₐ[M] L)
    (a : RelativeIdeleGroup K L) :
    towerRelativeIdeleBaseChangeMulEquiv K M L
        ((towerRelativeIdeleEquiv K M L).symm
          (RelativeIdeleGroup.conjugationIdele K L
            (σ.restrictScalars K) a)) =
      RelativeIdeleGroup.conjugationIdele M L σ
        (towerRelativeIdeleBaseChangeMulEquiv K M L
          ((towerRelativeIdeleEquiv K M L).symm a))

theorem

towerRelativeIdeleBaseChangeMulEquiv_includeLeft

L504 ↗

Documentation

Extending an idele from the intermediate relative adele ring into the tower and then passing to the actual M-relative presentation is the ordinary relative class-field-theoretic inclusion.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_includeLeft
    (a : RelativeIdeleGroup K M) :
    towerRelativeIdeleBaseChangeMulEquiv K M L
        (Units.map
          (Algebra.TensorProduct.includeLeft
            (R := M) (S := M)
            (A := RelativeAdeleRing K M) (B := L)).toRingHom a) =
      RelativeIdeleGroup.inclusion M L
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := M) a)

theorem

towerPrincipalSubgroup_map_baseChange

L534 ↗

Documentation

The comparison maps tower principal ideles exactly onto the actual relative principal-ideles subgroup over M.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerPrincipalSubgroup_map_baseChange :
    (TowerRelativeIdeleGroup.principalSubgroup K M L).map
        (towerRelativeIdeleBaseChangeMulEquiv K M L) =
      RelativeIdeleGroup.principalSubgroup M L

def

towerRelativeIdeleClassBaseChangeMulEquiv

L549 ↗

Documentation

The fixed-bottom tower class group is canonically the actual relative idele class group of L/M.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison

Lean source · statement

def towerRelativeIdeleClassBaseChangeMulEquiv :
    TowerRelativeIdeleGroup.ClassGroup K M L ≃*
      RelativeIdeleGroup.ClassGroup M L

theorem

towerRelativeIdeleClassBaseChangeMulEquiv_mk

L561 ↗

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleClassBaseChangeMulEquiv_mk
    (a : TowerRelativeIdeleGroup K M L) :
    towerRelativeIdeleClassBaseChangeMulEquiv K M L
        (QuotientGroup.mk'
          (TowerRelativeIdeleGroup.principalSubgroup K M L) a) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup M L)
        (towerRelativeIdeleBaseChangeMulEquiv K M L a)

theorem

relativeIdeleClassBaseChangeMulEquiv_tower

L574 ↗

Documentation

Scalar extension from a fixed-bottom tower class group to the ordinary top-field idele class group is independent of the intermediate presentation.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison

Lean source · statement

theorem relativeIdeleClassBaseChangeMulEquiv_tower
    (c : RelativeIdeleGroup.ClassGroup K L) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := M) (L := L)
        (towerRelativeIdeleClassBaseChangeMulEquiv K M L
          ((TowerRelativeIdeleGroup.classGroupEquiv
            K M L).symm c)) =
      relativeIdeleClassBaseChangeMulEquiv
        (K := K) (L := L) c

theorem

towerRelativeIdeleClassBaseChangeMulEquiv_smul

L610 ↗

Documentation

The class-group comparison transports the Galois action obtained by restricting scalars from the bottom field to the natural action over the intermediate field.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section IdeleComparison
omit [NumberField L] [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleClassBaseChangeMulEquiv_smul
    (σ : L ≃ₐ[M] L)
    (c : RelativeIdeleGroup.ClassGroup K L) :
    towerRelativeIdeleClassBaseChangeMulEquiv K M L
        ((TowerRelativeIdeleGroup.classGroupEquiv K M L).symm
          ((σ.restrictScalars K) • c)) =
      σ •
        towerRelativeIdeleClassBaseChangeMulEquiv K M L
          ((TowerRelativeIdeleGroup.classGroupEquiv K M L).symm c)

def

towerActualFiniteComponent

L645 ↗

Documentation

The actual finite component of the tower model after the intermediate adele-ring comparison.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison

Lean source · statement

def towerActualFiniteComponent
    (W : HeightOneSpectrum (𝓞 M)) :
    TowerRelativeIdeleGroup K M L →*
      (W.adicCompletion M ⊗[M] L)ˣ

def

towerActualInfiniteComponent

L658 ↗

Documentation

The actual archimedean component of the tower model after the intermediate adele-ring comparison.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison

Lean source · statement

def towerActualInfiniteComponent
    (W : InfinitePlace M) :
    TowerRelativeIdeleGroup K M L →*
      (W.Completion ⊗[M] L)ˣ

theorem

towerRelativeIdeleBaseChangeMulEquiv_finiteComponent

L674 ↗

Documentation

Finite-component identification for the norm-compatible tower comparison.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_finiteComponent
    (W : HeightOneSpectrum (𝓞 M))
    (a : TowerRelativeIdeleGroup K M L) :
    RelativeIdeleGroup.finiteComponent
        (K := M) (L := L) W
        (towerRelativeIdeleBaseChangeMulEquiv K M L a) =
      towerActualFiniteComponent K M L W a

theorem

towerRelativeIdeleBaseChangeMulEquiv_infiniteComponent

L705 ↗

Documentation

Archimedean-component identification for the norm-compatible tower comparison.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_infiniteComponent
    (W : InfinitePlace M)
    (a : TowerRelativeIdeleGroup K M L) :
    RelativeIdeleGroup.infiniteComponent
        (K := M) (L := L) W
        (towerRelativeIdeleBaseChangeMulEquiv K M L a) =
      towerActualInfiniteComponent K M L W a

def

towerIntermediateFiniteComponentAlgHom

L733 ↗

Documentation

Evaluation of the fixed-bottom relative adele ring at one exact finite extension of a place of K, as an M-algebra map.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison

Lean source · statement

def towerIntermediateFiniteComponentAlgHom
    (w : HeightOneSpectrum (𝓞 K))
    (uM : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) M) :
    RelativeAdeleRing K M →ₐ[M] uM.1.Completion

def

towerIntermediateFiniteComponent

L764 ↗

Documentation

The local tensor component of a tower idele at an exact finite extension place of M.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison

Lean source · statement

def towerIntermediateFiniteComponent
    (w : HeightOneSpectrum (𝓞 K))
    (uM : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) M) :
    TowerRelativeIdeleGroup K M L →*
      (uM.1.Completion ⊗[M] L)ˣ

def

intermediateFiniteComponent

L777 ↗

Documentation

Evaluation of a relative idele over K at the same exact finite extension place of M.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison

Lean source · statement

def intermediateFiniteComponent
    (w : HeightOneSpectrum (𝓞 K))
    (uM : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) M) :
    RelativeIdeleGroup K M →* uM.1.Completionˣ

theorem

towerIntermediateFiniteComponent_norm

L788 ↗

Documentation

Determinant norm commutes with the exact finite-place component of the fixed-bottom tower model.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison
omit [NumberField M] [NumberField L] [Algebra K L] [IsScalarTower K M L] in

Lean source · statement

theorem towerIntermediateFiniteComponent_norm
    (w : HeightOneSpectrum (𝓞 K))
    (uM : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) M)
    (a : TowerRelativeIdeleGroup K M L) :
    intermediateFiniteComponent K M w uM
        (TowerRelativeIdeleGroup.norm K M L a) =
      Units.map (Algebra.norm uM.1.Completion)
        (towerIntermediateFiniteComponent K M L w uM a)

theorem

towerRelativeIdeleBaseChangeMulEquiv_norm

L808 ↗

Documentation

The actual relative-idele norm is the tower determinant norm after the intermediate relative-to-ordinary adele comparison.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section NormComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L]
    [FiniteDimensional M L] in

Lean source · statement

theorem towerRelativeIdeleBaseChangeMulEquiv_norm
    (a : TowerRelativeIdeleGroup K M L) :
    relativeIdeleBaseChangeMulEquiv
        (K := K) (L := M)
        (TowerRelativeIdeleGroup.norm K M L a) =
      RelativeIdeleGroup.norm M L
        (towerRelativeIdeleBaseChangeMulEquiv K M L a)

theorem

towerRelativeIdeleClassBaseChangeMulEquiv_classNorm

L875 ↗

Documentation

After both relative presentations are replaced by the ordinary idele class groups, the fixed-bottom tower class norm is the actual class norm for L/M.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section ClassNormComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L] in

Lean source · statement

theorem towerRelativeIdeleClassBaseChangeMulEquiv_classNorm
    (c : TowerRelativeIdeleGroup.ClassGroup K M L) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := K) (L := M)
        (TowerRelativeIdeleGroup.classNorm K M L c) =
      RelativeIdeleGroup.classNorm M L
        (towerRelativeIdeleClassBaseChangeMulEquiv K M L c)

theorem

towerClassNorm_range_map_baseChange

L893 ↗

Documentation

The fixed-bottom tower norm subgroup becomes exactly the actual L/M class-norm subgroup after base change to the ordinary class group of M.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section ClassNormComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L] in

Lean source · statement

theorem towerClassNorm_range_map_baseChange :
    (TowerRelativeIdeleGroup.classNorm K M L).range.map
        (relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := M)).toMonoidHom =
      (RelativeIdeleGroup.classNorm M L).range

def

intermediateClassNormQuotientBaseChangeMulEquiv

L927 ↗

Documentation

The fixed-bottom quotient C_M / N_{L/M} C_L is canonically the ordinary idele-class norm quotient for the actual extension L/M.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section ClassNormComparison

Lean source · statement

def intermediateClassNormQuotientBaseChangeMulEquiv :
    IntermediateClassNormQuotient K M L ≃*
      RelativeIdeleGroup.ClassNormQuotient M L

theorem

intermediateClassNormQuotientBaseChangeMulEquiv_mk

L939 ↗

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section ClassNormComparison
omit [NumberField L] [Algebra K L] [IsScalarTower K M L] in

Lean source · statement

theorem intermediateClassNormQuotientBaseChangeMulEquiv_mk
    (c : RelativeIdeleGroup.ClassGroup K M) :
    intermediateClassNormQuotientBaseChangeMulEquiv K M L
        (QuotientGroup.mk'
          (TowerRelativeIdeleGroup.classNorm K M L).range c) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.classNorm M L).range
        (relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := M) c)

theorem

ordinaryIdeleClassNorm_tower

L958 ↗

Documentation

Ordinary idele-class norms are pointwise transitive in an arbitrary finite tower of number fields. This is determinant-norm transitivity, transported through the actual relative-idele presentations over the bottom and intermediate fields.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section OrdinaryNormTower

Lean source · statement

theorem ordinaryIdeleClassNorm_tower
    (c : IdeleClassGroup L) :
    _root_.ideleClassNorm K M
        (_root_.ideleClassNorm M L c) =
      _root_.ideleClassNorm K L c

theorem

ordinaryIdeleClassNorm_range_le_of_tower

L1053 ↗

Documentation

In an arbitrary finite tower of number fields, every ordinary idele-class norm from the top field is already a norm from the intermediate field. No normality hypothesis is needed: this is determinant-norm transitivity transported from the fixed-bottom tower presentation to the ordinary idele class groups.

Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
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]

-- These canonical commutativity proofs are local to the imported tower
-- module; retain them here for the quotient-group instances.
local instance
    towerBaseChange_towerRelativeIdeleGroupIsMulCommutative
    (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
    towerBaseChange_relativeIdeleClassGroupIsMulCommutative
    (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 towerBaseChange_ideleClassGroupIsMulCommutative
    (A : Type u) [Field A] [NumberField A] :
    IsMulCommutative (IdeleClassGroup A) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section OrdinaryNormTower

Lean source · statement

theorem ordinaryIdeleClassNorm_range_le_of_tower :
    (_root_.ideleClassNorm K L).range ≤
      (_root_.ideleClassNorm K M).range

Module documentation

The fixed-bottom tower model and the actual intermediate-field model

Declarations