NYLL
Module

AlgEquiv.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.AlgEquiv
61 declarations indexed from sourceView source ↗

Module documentation

Relative idele classes under an isomorphic realization

If two finite extensions of a number field are isomorphic over the base, their tensor-product presentations of the relative adeles are canonically isomorphic. This file descends that canonical isomorphism to relative ideles and idele classes and records compatibility with the determinant norm.

The construction is the direct tensor-product congruence

𝔸_K ⊗[K] L ≃ 𝔸_K ⊗[K] M

induced by an algebra equivalence L ≃ₐ[K] M. In particular, no second model of relative adeles or of the idele-class norm is introduced.

Imports5
Imported by18

Declarations

def

relativeAdeleCongr

L52 ↗
Documentation

A base-field algebra equivalence between two realizations of a finite extension induces the canonical equivalence between their relative adele algebras.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
def relativeAdeleCongr
    (e : L ≃ₐ[K] M) :
    RelativeAdeleRing K L ≃ₐ[
      NumberField.AdeleRing (𝓞 K) K]
      RelativeAdeleRing K M
theorem

relativeAdeleCongr_tmul

L60 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeAdeleCongr_tmul
    (e : L ≃ₐ[K] M)
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L) :
    relativeAdeleCongr (K := K) e (a ⊗ₜ[K] x) =
      a ⊗ₜ[K] e x
def

relativeIdeleCongr

L70 ↗
Documentation

The canonical transport of relative ideles along an isomorphic realization of the top field.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
def relativeIdeleCongr
    (e : L ≃ₐ[K] M) :
    RelativeIdeleGroup K L ≃*
      RelativeIdeleGroup K M
theorem

relativeIdeleCongr_coe

L78 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeIdeleCongr_coe
    (e : L ≃ₐ[K] M)
    (a : RelativeIdeleGroup K L) :
    ((relativeIdeleCongr (K := K) e a :
        RelativeIdeleGroup K M) :
      RelativeAdeleRing K M) =
        relativeAdeleCongr (K := K) e
          (a : RelativeAdeleRing K L)
theorem

relativeIdeleCongr_eq_smul

L90 ↗
Documentation

For an automorphism of the top field, canonical relative-idele transport is the actual Galois action.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeIdeleCongr_eq_smul
    (σ : L ≃ₐ[K] L)
    (a : RelativeIdeleGroup K L) :
    relativeIdeleCongr (K := K) σ a = σ • a
theorem

relativeIdeleCongr_principalIdele

L99 ↗
Documentation

Transport of relative ideles sends a principal idele to the principal idele of the transported field unit.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeIdeleCongr_principalIdele
    (e : L ≃ₐ[K] M)
    (x : Lˣ) :
    relativeIdeleCongr (K := K) e
        (RelativeIdeleGroup.principalIdele K L x) =
      RelativeIdeleGroup.principalIdele K M
        (Units.mapEquiv e.toMulEquiv x)
theorem

relativeIdelePrincipalSubgroup_map_congr

L115 ↗
Documentation

The canonical transport identifies the two principal-relative-idele subgroups.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeIdelePrincipalSubgroup_map_congr
    (e : L ≃ₐ[K] M) :
    (RelativeIdeleGroup.principalSubgroup K L).map
        (relativeIdeleCongr (K := K) e) =
      RelativeIdeleGroup.principalSubgroup K M
def

relativeIdeleClassCongr

L139 ↗
Documentation

The relative idele class group is unchanged when the top field is replaced by an isomorphic realization.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
def relativeIdeleClassCongr
    (e : L ≃ₐ[K] M) :
    RelativeIdeleGroup.ClassGroup K L ≃*
      RelativeIdeleGroup.ClassGroup K M
theorem

relativeIdeleClassCongr_mk

L151 ↗
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeIdeleClassCongr_mk
    (e : L ≃ₐ[K] M)
    (a : RelativeIdeleGroup K L) :
    relativeIdeleClassCongr (K := K) e
        (QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K M)
        (relativeIdeleCongr (K := K) e a)
theorem

classEmbedding_relativeIdeleClassCongr

L165 ↗
RelativeIdeleGroup.classEmbedding_relativeIdeleClassCongr
Documentation

Transporting a relative idèle class along an equivalence and then embedding it into a third relative idèle class group is the same as embedding along the composite field embedding.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem RelativeIdeleGroup.classEmbedding_relativeIdeleClassCongr
    {N : Type*} [Field N] [Algebra K N]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [FiniteDimensional K N]
    (e : L ≃ₐ[K] M)
    (f : M →ₐ[K] N)
    (c : RelativeIdeleGroup.ClassGroup K L) :
    RelativeIdeleGroup.classEmbedding f
        (relativeIdeleClassCongr (K := K) e c) =
      RelativeIdeleGroup.classEmbedding
        (f.comp e.toAlgHom) c
theorem

relativeIdeleCongr_norm

L214 ↗
Documentation

The determinant norm on relative ideles is invariant under replacement of the top field by an isomorphic realization.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
Lean source · statement
theorem relativeIdeleCongr_norm
    (e : L ≃ₐ[K] M)
    (a : RelativeIdeleGroup K L) :
    RelativeIdeleGroup.norm K M
        (relativeIdeleCongr (K := K) e a) =
      RelativeIdeleGroup.norm K L a
theorem

relativeIdeleClassCongr_ideleClassNorm

L247 ↗
Documentation

The descended idele-class norm is invariant under the canonical transport of the relative idele class group.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Norm
variable [FiniteDimensional K L] [FiniteDimensional K M]
Lean source · statement
theorem relativeIdeleClassCongr_ideleClassNorm
    (e : L ≃ₐ[K] M)
    (c : RelativeIdeleGroup.ClassGroup K L) :
    RelativeIdeleGroup.classNorm K M
        (relativeIdeleClassCongr (K := K) e c) =
      RelativeIdeleGroup.classNorm K L c
theorem

ideleClassNorm_range_algEquiv

L267 ↗
Documentation

Isomorphic realizations of a finite extension have the same actual idele-class norm subgroup in 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
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Norm
variable [FiniteDimensional K L] [FiniteDimensional K M]
Lean source · statement
theorem ideleClassNorm_range_algEquiv
    (e : L ≃ₐ[K] M) :
    (RelativeIdeleGroup.classNorm K M).range =
      (RelativeIdeleGroup.classNorm K L).range
theorem

ideleClassNorm_index_algEquiv

L292 ↗
Documentation

The idele-class norm index is invariant under an isomorphic realization of the top field.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Norm
variable [FiniteDimensional K L] [FiniteDimensional K M]
Lean source · statement
theorem ideleClassNorm_index_algEquiv
    (e : L ≃ₐ[K] M) :
    (RelativeIdeleGroup.classNorm K M).range.index =
      (RelativeIdeleGroup.classNorm K L).range.index
def

adeleCongr

L311 ↗
Documentation

The canonical transport of ordinary adele rings along an equivalence of number fields. It is the existing relative-adele transport over ℚ, conjugated by the relative-to-ordinary scalar-extension equivalences.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
def adeleCongr
    (e : K ≃ₐ[ℚ] M) :
    NumberField.AdeleRing (𝓞 K) K ≃+*
      NumberField.AdeleRing (𝓞 M) M
theorem

relativeAdeleBaseChangeRingEquiv_relativeAdeleCongr

L323 ↗
Documentation

The relative-to-ordinary scalar-extension comparison is natural for transport of the top number field.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem relativeAdeleBaseChangeRingEquiv_relativeAdeleCongr
    (e : K ≃ₐ[ℚ] M)
    (z : RelativeAdeleRing ℚ K) :
    relativeAdeleBaseChangeRingEquiv
        (K := ℚ) (L := M)
        (relativeAdeleCongr (K := ℚ) e z) =
      adeleCongr e
        (relativeAdeleBaseChangeRingEquiv
          (K := ℚ) (L := K) z)
theorem

adeleCongr_algebraMap

L348 ↗
Documentation

Transport of ordinary adeles carries the diagonal field embedding to the diagonal field embedding.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem adeleCongr_algebraMap
    (e : K ≃ₐ[ℚ] M)
    (x : K) :
    adeleCongr e
        (algebraMap K
          (NumberField.AdeleRing (𝓞 K) K) x) =
      algebraMap M
        (NumberField.AdeleRing (𝓞 M) M) (e x)
def

finitePlaceCongr

L382 ↗
Documentation

The permutation of finite places induced by an equivalence of number fields.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
def finitePlaceCongr
    (e : K ≃ₐ[ℚ] M) :
    HeightOneSpectrum (𝓞 K) ≃
      HeightOneSpectrum (𝓞 M)
theorem

finitePlaceCongr_asIdeal

L392 ↗
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
omit [NumberField K] [NumberField M] in
Lean source · statement
theorem finitePlaceCongr_asIdeal
    (e : K ≃ₐ[ℚ] M)
    (v : HeightOneSpectrum (𝓞 K)) :
    (finitePlaceCongr e v).asIdeal =
      v.asIdeal.map
        (NumberField.RingOfIntegers.mapRingEquiv
          e.toRingEquiv)
theorem

finitePlaceBelow_eq_finitePlaceCongr_symm

L402 ↗
Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · full declaration
theorem finitePlaceBelow_eq_finitePlaceCongr_symm
    (e : K ≃ₐ[ℚ] M)
    (W : HeightOneSpectrum (𝓞 M)) :
    letI : Algebra K M := e.toRingHom.toAlgebra
    finitePlaceBelow (K := K) W =
      (finitePlaceCongr e).symm W := by
  apply HeightOneSpectrum.ext
  rfl
def

finitePlaceAdicCompletionCongrHom

L413 ↗
Documentation

The canonical map between corresponding finite completions induced by an equivalence of number fields.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
def finitePlaceAdicCompletionCongrHom
    (e : K ≃ₐ[ℚ] M)
    (W : HeightOneSpectrum (𝓞 M)) :
    ((finitePlaceCongr e).symm W).adicCompletion K →+*
      W.adicCompletion M
theorem

adeleCongr_finiteComponent

L426 ↗
Documentation

On finite coordinates, canonical adelic transport is the completion map at the corresponding finite places.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem adeleCongr_finiteComponent
    (e : K ≃ₐ[ℚ] M)
    (a : NumberField.AdeleRing (𝓞 K) K)
    (W : HeightOneSpectrum (𝓞 M)) :
    (adeleCongr e a).2 W =
      finitePlaceAdicCompletionCongrHom e W
        (a.2 ((finitePlaceCongr e).symm W))
def

ideleCongr

L540 ↗
Documentation

The canonical transport of ordinary ideles along an equivalence of number fields. It is obtained from the existing relative-idele transport over ℚ and the canonical relative-to-ordinary base-change equivalences.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
def ideleCongr
    (e : K ≃ₐ[ℚ] M) :
    IdeleGroup K ≃* IdeleGroup M
theorem

relativeIdeleBaseChangeMulEquiv_relativeIdeleCongr

L549 ↗
Documentation

The relative-to-ordinary scalar-extension comparison is natural for transport of relative ideles along an equivalence of their top fields.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem relativeIdeleBaseChangeMulEquiv_relativeIdeleCongr
    (e : K ≃ₐ[ℚ] M)
    (a : RelativeIdeleGroup ℚ K) :
    relativeIdeleBaseChangeMulEquiv
        (K := ℚ) (L := M)
        (relativeIdeleCongr (K := ℚ) e a) =
      ideleCongr e
        (relativeIdeleBaseChangeMulEquiv
          (K := ℚ) (L := K) a)
theorem

relativeIdeleBaseChangeMulEquiv_smul_congr

L573 ↗
Documentation

Under the actual Galois action on relative ideles, the relative-to-ordinary scalar-extension comparison is equivariant for the canonical transport of ordinary ideles.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem relativeIdeleBaseChangeMulEquiv_smul_congr
    {E : Type*} [Field E] [NumberField E] [Algebra ℚ E]
    (σ : E ≃ₐ[ℚ] E)
    (a : RelativeIdeleGroup ℚ E) :
    relativeIdeleBaseChangeMulEquiv
        (K := ℚ) (L := E) (σ • a) =
      ideleCongr σ
        (relativeIdeleBaseChangeMulEquiv
          (K := ℚ) (L := E) a)
theorem

ideleCongr_finiteComponent

L590 ↗
Documentation

On finite coordinates, canonical idelic transport is the completion map at the corresponding finite places.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ideleCongr_finiteComponent
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K)
    (W : HeightOneSpectrum (𝓞 M)) :
    IdeleGroup.finiteComponent W (ideleCongr e a) =
      Units.map
        (finitePlaceAdicCompletionCongrHom e W).toMonoidHom
        (IdeleGroup.finiteComponent
          ((finitePlaceCongr e).symm W) a)
theorem

finitePlaceCongr_ramificationIdx

L609 ↗
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
omit [NumberField K] in
Lean source · full declaration
theorem finitePlaceCongr_ramificationIdx
    (e : K ≃ₐ[ℚ] M)
    (W : HeightOneSpectrum (𝓞 M)) :
    letI : Algebra K M := e.toRingHom.toAlgebra
    ((finitePlaceCongr e).symm W).asIdeal.ramificationIdx'
        W.asIdeal = 1 := by
  let : Algebra K M := e.toRingHom.toAlgebra
  let w : HeightOneSpectrum (𝓞 K) :=
    (finitePlaceCongr e).symm W
  have hmap :
      w.asIdeal.map (algebraMap (𝓞 K) (𝓞 M)) =
        W.asIdeal := by
    change
      w.asIdeal.map
          (NumberField.RingOfIntegers.mapRingEquiv
            e.toRingEquiv) =
        W.asIdeal
    rw [← finitePlaceCongr_asIdeal e w]
    simp [w]
  rw [← hmap]
  exact
    Ideal.ramificationIdx'_map_self_eq_one
      (p := w.asIdeal)
      (by rw [hmap]; exact W.isPrime.ne_top)
      (by rw [hmap]; exact W.ne_bot)
theorem

ideleCongr_localOrder

L637 ↗
Documentation

Normalized local orders are unchanged by transport along a number-field equivalence.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ideleCongr_localOrder
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K)
    (W : HeightOneSpectrum (𝓞 M)) :
    (FiniteIdeleGroup.localOrder W
        (IdeleGroup.finiteComponent W
          (ideleCongr e a))).toAdd =
      (FiniteIdeleGroup.localOrder
        ((finitePlaceCongr e).symm W)
        (IdeleGroup.finiteComponent
          ((finitePlaceCongr e).symm W) a)).toAdd
theorem

ideleCongr_mem_integralAtFinitePlaces_iff

L672 ↗
Documentation

An idele is integral at every finite place exactly when its transport along a number-field equivalence is.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ideleCongr_mem_integralAtFinitePlaces_iff
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K) :
    ideleCongr e a ∈
        IdeleGroup.integralAtFinitePlaces (K := M) ↔
      a ∈ IdeleGroup.integralAtFinitePlaces (K := K)
theorem

ideleIntegralAtFinitePlaces_map_congr

L715 ↗
Documentation

Transport along a number-field equivalence identifies the subgroups of ideles integral at every finite place.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ideleIntegralAtFinitePlaces_map_congr
    (e : K ≃ₐ[ℚ] M) :
    (IdeleGroup.integralAtFinitePlaces (K := K)).map
        (ideleCongr e).toMonoidHom =
      IdeleGroup.integralAtFinitePlaces (K := M)
theorem

ideleCongr_principalIdele

L737 ↗
Documentation

Transport along a number-field equivalence carries the diagonal idele to the diagonal idele of the transported field unit.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ideleCongr_principalIdele
    (e : K ≃ₐ[ℚ] M)
    (x : Kˣ) :
    ideleCongr e (IdeleGroup.principalIdele K x) =
      IdeleGroup.principalIdele M
        (Units.mapEquiv e.toMulEquiv x)
theorem

idelePrincipalSubgroup_map_congr

L751 ↗
Documentation

The ordinary principal-idele subgroups are identified by transport along a number-field equivalence.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem idelePrincipalSubgroup_map_congr
    (e : K ≃ₐ[ℚ] M) :
    (IdeleGroup.principalSubgroup K).map
        (ideleCongr e) =
      IdeleGroup.principalSubgroup M
theorem

ordinaryIdealClassSubgroup_map_congr

L773 ↗
Documentation

Transport along a number-field equivalence identifies the subgroups defining the ordinary ideal-class quotients.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ordinaryIdealClassSubgroup_map_congr
    (e : K ≃ₐ[ℚ] M) :
    (IdeleGroup.ordinaryIdealClassSubgroup (K := K)).map
        (ideleCongr e).toMonoidHom =
      IdeleGroup.ordinaryIdealClassSubgroup (K := M)
def

ideleClassCongr

L794 ↗
Documentation

The canonical transport of ordinary idele classes along an equivalence of number fields. This descends ideleCongr; it does not introduce a second idele-class quotient.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
def ideleClassCongr
    (e : K ≃ₐ[ℚ] M) :
    IdeleClassGroup K ≃* IdeleClassGroup M
theorem

ideleClassCongr_mk

L806 ↗
Documentation

The ordinary idele-class transport is induced by ideleCongr on quotient representatives.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ideleClassCongr_mk
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K) :
    ideleClassCongr e
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      QuotientGroup.mk'
        (IdeleGroup.principalSubgroup M)
        (ideleCongr e a)
theorem

relativeIdeleClassBaseChangeMulEquiv_relativeIdeleClassCongr

L820 ↗
Documentation

The relative-to-ordinary scalar-extension comparison is natural for transport of relative idèle classes along an equivalence of their top fields.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem
    relativeIdeleClassBaseChangeMulEquiv_relativeIdeleClassCongr
    (e : K ≃ₐ[ℚ] M)
    (c : RelativeIdeleGroup.ClassGroup ℚ K) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := ℚ) (L := M)
        (relativeIdeleClassCongr (K := ℚ) e c) =
      ideleClassCongr e
        (relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := K) c)
instance

(anonymous instance)

L852 ↗
Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section GaloisBaseChangeNaturality
variable {E : Type} [Field E] [NumberField E] [Algebra ℚ E]
Lean source · statement
instance :
    MulDistribMulAction (E ≃ₐ[ℚ] E)
      (RelativeIdeleGroup.ClassGroup ℚ E)
theorem

relativeIdeleClassBaseChangeMulEquiv_smul_congr

L860 ↗
Documentation

The actual Galois action on relative idele classes becomes canonical ordinary idele-class transport under the relative-to-ordinary scalar-extension comparison.

Source context 12 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section GaloisBaseChangeNaturality
variable {E : Type} [Field E] [NumberField E] [Algebra ℚ E]
local instance :
    MulDistribMulAction (E ≃ₐ[ℚ] E)
      (RelativeIdeleGroup.ClassGroup ℚ E) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction ℚ E
Lean source · statement
theorem relativeIdeleClassBaseChangeMulEquiv_smul_congr
    (σ : E ≃ₐ[ℚ] E)
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := ℚ) (L := E) (σ • c) =
      ideleClassCongr σ
        (relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := E) c)
theorem

ordinaryIdealClassSubgroup_image_map_ideleClassCongr

L891 ↗
Documentation

On idele class groups, transport identifies the images of the ordinary ideal-class subgroups. This is the subgroup-level naturality used by the small Hilbert class field.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem ordinaryIdealClassSubgroup_image_map_ideleClassCongr
    (e : K ≃ₐ[ℚ] M) :
    (Subgroup.map
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K))
        (IdeleGroup.ordinaryIdealClassSubgroup (K := K))).map
          (ideleClassCongr e).toMonoidHom =
      Subgroup.map
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup M))
        (IdeleGroup.ordinaryIdealClassSubgroup (K := M))
theorem

relativeAdeleBaseChangeRingEquiv_self_tmul_one

L915 ↗
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
omit [Algebra ℚ K] in
Lean source · statement
theorem
    relativeAdeleBaseChangeRingEquiv_self_tmul_one
    (a : NumberField.AdeleRing (𝓞 K) K) :
    relativeAdeleBaseChangeRingEquiv
        (K := K) (L := K) (a ⊗ₜ[K] (1 : K)) =
      a
theorem

relativeAdeleBaseChangeRingEquiv_self_symm_apply

L954 ↗
Source context 10 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
omit [Algebra ℚ K] in
Lean source · statement
theorem
    relativeAdeleBaseChangeRingEquiv_self_symm_apply
    (a : NumberField.AdeleRing (𝓞 K) K) :
    (relativeAdeleBaseChangeRingEquiv
        (K := K) (L := K)).symm a =
      a ⊗ₜ[K] (1 : K)
theorem

rationalAdeleExtension_eq_adeleCongr

L968 ↗
Documentation

Scalar extension from ℚ to a realization algebra-equivalent to ℚ is the canonical transport of ordinary adele rings.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem rationalAdeleExtension_eq_adeleCongr
    (e : ℚ ≃ₐ[ℚ] M)
    (a : NumberField.AdeleRing (𝓞 ℚ) ℚ) :
    relativeAdeleBaseChangeRingEquiv
        (K := ℚ) (L := M)
        (RelativeIdeleGroup.adeleInclusion ℚ M a) =
      adeleCongr e a
theorem

rationalIdeleExtension_eq_ideleCongr

L989 ↗
Documentation

Scalar extension from ℚ to a realization algebra-equivalent to ℚ is the canonical transport of ordinary ideles.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem rationalIdeleExtension_eq_ideleCongr
    (e : ℚ ≃ₐ[ℚ] M) :
    IdeleGroup.extension ℚ M =
      (ideleCongr e).toMonoidHom
theorem

rationalIdeleClassExtension_eq_ideleClassCongr

L1014 ↗
Documentation

Scalar extension from ℚ to a realization algebra-equivalent to ℚ is the canonical transport of ordinary idele classes.

Source context 9 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
Lean source · statement
theorem rationalIdeleClassExtension_eq_ideleClassCongr
    (e : ℚ ≃ₐ[ℚ] M) :
    ideleClassExtension ℚ M =
      (ideleClassCongr e).toMonoidHom
def

relativeAdeleMapOfCompatibleEquiv

L1047 ↗
Documentation

The tensor-product map induced by compatible equivalences of both fields in a finite extension. The coefficient-ring equivalence is kept explicit so the inverse uses that exact equivalence rather than a second choice.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
def relativeAdeleMapOfCompatibleEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eA :
      NumberField.AdeleRing (𝓞 K) K ≃+*
        NumberField.AdeleRing (𝓞 K') K')
    (hA : ∀ x : K,
      eA
          (algebraMap K
            (NumberField.AdeleRing (𝓞 K) K) x) =
        algebraMap K'
          (NumberField.AdeleRing (𝓞 K') K') (eK x))
    (eL : L ≃ₐ[ℚ] L')
    (hL : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    RelativeAdeleRing K L →+*
      RelativeAdeleRing K' L'
theorem

relativeAdeleMapOfCompatibleEquiv_tmul

L1102 ↗
Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
theorem relativeAdeleMapOfCompatibleEquiv_tmul
    (eK : K ≃ₐ[ℚ] K')
    (eA :
      NumberField.AdeleRing (𝓞 K) K ≃+*
        NumberField.AdeleRing (𝓞 K') K')
    (hA : ∀ x : K,
      eA
          (algebraMap K
            (NumberField.AdeleRing (𝓞 K) K) x) =
        algebraMap K'
          (NumberField.AdeleRing (𝓞 K') K') (eK x))
    (eL : L ≃ₐ[ℚ] L')
    (hL : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L) :
    relativeAdeleMapOfCompatibleEquiv
        eK eA hA eL hL (a ⊗ₜ[K] x) =
      eA a ⊗ₜ[K'] eL x
def

relativeAdeleCongrOfAlgEquiv

L1139 ↗
Documentation

Compatible equivalences of number-field extensions induce the canonical equivalence of their relative adele rings.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
def relativeAdeleCongrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    RelativeAdeleRing K L ≃+*
      RelativeAdeleRing K' L'
theorem

relativeAdeleCongrOfAlgEquiv_tmul

L1254 ↗
Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
theorem relativeAdeleCongrOfAlgEquiv_tmul
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (a : NumberField.AdeleRing (𝓞 K) K)
    (x : L) :
    relativeAdeleCongrOfAlgEquiv eK eL h
        (a ⊗ₜ[K] x) =
      adeleCongr eK a ⊗ₜ[K'] eL x
def

relativeIdeleCongrOfAlgEquiv

L1271 ↗
Documentation

Compatible equivalences of number-field extensions induce the canonical equivalence of their relative idele groups.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
def relativeIdeleCongrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    RelativeIdeleGroup K L ≃*
      RelativeIdeleGroup K' L'
theorem

relativeIdeleCongrOfAlgEquiv_principalIdele

L1283 ↗
Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
theorem relativeIdeleCongrOfAlgEquiv_principalIdele
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (x : Lˣ) :
    relativeIdeleCongrOfAlgEquiv eK eL h
        (RelativeIdeleGroup.principalIdele K L x) =
      RelativeIdeleGroup.principalIdele K' L'
        (Units.mapEquiv eL.toMulEquiv x)
theorem

relativeIdelePrincipalSubgroup_map_congrOfAlgEquiv

L1304 ↗
Documentation

The semilinear relative-idele transport identifies the principal subgroups.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
theorem relativeIdelePrincipalSubgroup_map_congrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    (RelativeIdeleGroup.principalSubgroup K L).map
        (relativeIdeleCongrOfAlgEquiv eK eL h) =
      RelativeIdeleGroup.principalSubgroup K' L'
def

relativeIdeleClassCongrOfAlgEquiv

L1332 ↗
Documentation

Compatible equivalences of number-field extensions induce the canonical equivalence of their existing relative idele class groups.

Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
def relativeIdeleClassCongrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    RelativeIdeleGroup.ClassGroup K L ≃*
      RelativeIdeleGroup.ClassGroup K' L'
theorem

relativeIdeleClassCongrOfAlgEquiv_mk

L1348 ↗
Source context 11 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
Lean source · statement
theorem relativeIdeleClassCongrOfAlgEquiv_mk
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (a : RelativeIdeleGroup K L) :
    relativeIdeleClassCongrOfAlgEquiv eK eL h
        (QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a) =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K' L')
        (relativeIdeleCongrOfAlgEquiv eK eL h a)
theorem

relativeAdeleCongrOfAlgEquiv_norm

L1372 ↗
Documentation

Determinant norms on relative adele rings commute with compatible equivalences of both fields in the extension.

Source context 14 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
omit [FiniteDimensional K L] [FiniteDimensional K' L'] in
Lean source · statement
theorem relativeAdeleCongrOfAlgEquiv_norm
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (z : RelativeAdeleRing K L) :
    adeleCongr eK
        (Algebra.norm
          (NumberField.AdeleRing (𝓞 K) K) z) =
      Algebra.norm
        (NumberField.AdeleRing (𝓞 K') K')
        (relativeAdeleCongrOfAlgEquiv eK eL h z)
theorem

relativeIdeleCongrOfAlgEquiv_norm

L1411 ↗
Documentation

The relative idele norm commutes with compatible equivalences of number-field extensions.

Source context 14 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
omit [FiniteDimensional K L] [FiniteDimensional K' L'] in
Lean source · statement
theorem relativeIdeleCongrOfAlgEquiv_norm
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (a : RelativeIdeleGroup K L) :
    ideleCongr eK (RelativeIdeleGroup.norm K L a) =
      RelativeIdeleGroup.norm K' L'
        (relativeIdeleCongrOfAlgEquiv eK eL h a)
theorem

relativeIdeleClassCongrOfAlgEquiv_ideleClassNorm

L1435 ↗
Documentation

The descended relative idele-class norm commutes with compatible equivalences of number-field extensions.

Source context 15 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
variable [IsGalois K L] [IsGalois K' L']
omit [IsGalois K L] [IsGalois K' L'] in
Lean source · statement
theorem relativeIdeleClassCongrOfAlgEquiv_ideleClassNorm
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (c : RelativeIdeleGroup.ClassGroup K L) :
    ideleClassCongr eK
        (RelativeIdeleGroup.classNorm K L c) =
      RelativeIdeleGroup.classNorm K' L'
        (relativeIdeleClassCongrOfAlgEquiv
          eK eL h c)
theorem

relativeIdeleClassNorm_range_map_congrOfAlgEquiv

L1458 ↗
Documentation

Under compatible equivalences of number-field extensions, the relative class-norm subgroup is carried exactly to the relative class-norm subgroup of the transported extension.

Source context 15 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
variable [IsGalois K L] [IsGalois K' L']
omit [IsGalois K L] [IsGalois K' L'] in
Lean source · statement
theorem relativeIdeleClassNorm_range_map_congrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    (RelativeIdeleGroup.classNorm K L).range.map
        (ideleClassCongr eK).toMonoidHom =
      (RelativeIdeleGroup.classNorm K' L').range
theorem

ordinaryIdeleClassNorm_range_map_congrOfAlgEquiv

L1491 ↗
Documentation

Under compatible equivalences of finite Galois number-field extensions, the ordinary class-norm subgroup is carried exactly to the ordinary class-norm subgroup of the transported extension.

Source context 15 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
variable [IsGalois K L] [IsGalois K' L']
omit [FiniteDimensional K L] [FiniteDimensional K' L']
  [IsGalois K L] [IsGalois K' L'] in
Lean source · statement
theorem ordinaryIdeleClassNorm_range_map_congrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    (_root_.ideleClassNorm K L).range.map
        (ideleClassCongr eK).toMonoidHom =
      (_root_.ideleClassNorm K' L').range
instance

normIdeleClassGroup_isMulCommutative

L1509 ↗
Source context 14 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
variable [IsGalois K L] [IsGalois K' L']
Lean source · statement
instance normIdeleClassGroup_isMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

ordinaryIdeleClassNormQuotientCongrOfAlgEquiv

L1517 ↗
Documentation

Compatible equivalences of finite Galois number-field extensions induce the canonical equivalence of their ordinary idele-class norm quotients.

Source context 15 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
variable [IsGalois K L] [IsGalois K' L']
local instance normIdeleClassGroup_isMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  IsMulCommutative.of_comm (fun a b => mul_comm a b)
Lean source · statement
def ordinaryIdeleClassNormQuotientCongrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      (IdeleClassGroup K' ⧸
        (_root_.ideleClassNorm K' L').range)
theorem

ordinaryIdeleClassNormQuotientCongrOfAlgEquiv_mk

L1539 ↗
Documentation

On an ordinary idele-class representative, transport of norm quotients is induced by the existing idele-class transport.

Source context 16 commands

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

open scoped NumberField TensorProduct
open NumberField
open IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
universe u v w
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [Field M] [Algebra K M]
section Absolute
variable
    {K : Type u} {M : Type w}
    [Field K] [NumberField K] [Algebra ℚ K]
    [Field M] [NumberField M] [Algebra ℚ M]
section RelativeTowerCongr
variable
    {K L K' L' : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [Field K'] [NumberField K']
    [Field L'] [NumberField L'] [Algebra K' L']
section Norm
variable
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
variable [IsGalois K L] [IsGalois K' L']
local instance normIdeleClassGroup_isMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  IsMulCommutative.of_comm (fun a b => mul_comm a b)
omit [FiniteDimensional K L] [FiniteDimensional K' L']
  [IsGalois K L] [IsGalois K' L'] in
Lean source · statement
theorem ordinaryIdeleClassNormQuotientCongrOfAlgEquiv_mk
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (c : IdeleClassGroup K) :
    ordinaryIdeleClassNormQuotientCongrOfAlgEquiv
        eK eL h
        (QuotientGroup.mk'
          (_root_.ideleClassNorm K L).range c) =
      QuotientGroup.mk'
        (_root_.ideleClassNorm K' L').range
        (ideleClassCongr eK c)

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