NYLL
Module

EmbeddingNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.EmbeddingNorm
28 declarations indexed from sourceView source ↗

Module documentation

Norms through an ambient Galois extension

This file proves the embedded-subextension determinant-norm formula. If L/K is embedded in a finite Galois extension M/K, extending the determinant norm of an element of A ⊗[K] L to A ⊗[K] M gives the product over all K-embeddings L → M.

Imports2
Imported by2

Declarations

def

embeddingToAlgebraicClosure

L39 ↗
RelativeIdeleGroup.embeddingToAlgebraicClosure
Documentation

Extend a K-embedding L → M to the algebraic closure of M.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
def embeddingToAlgebraicClosure :
    (L →ₐ[K] M) →
      (L →ₐ[K] AlgebraicClosure M)
theorem

embeddingToAlgebraicClosure_injective

L47 ↗
RelativeIdeleGroup.embeddingToAlgebraicClosure_injective
Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
omit [Algebra L M] [IsScalarTower K L M] in
Lean source · statement
theorem embeddingToAlgebraicClosure_injective :
    Function.Injective
      (embeddingToAlgebraicClosure
        (K := K) (L := L) (M := M))
theorem

embeddingToAlgebraicClosure_surjective

L57 ↗
RelativeIdeleGroup.embeddingToAlgebraicClosure_surjective
Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
theorem embeddingToAlgebraicClosure_surjective
    [FiniteDimensional K M] [Normal K M] :
    Function.Surjective
      (embeddingToAlgebraicClosure
        (K := K) (L := L) (M := M))
def

embeddingToAlgebraicClosureEquiv

L78 ↗
RelativeIdeleGroup.embeddingToAlgebraicClosureEquiv
Documentation

Embeddings of a subextension into a finite normal overfield are the same as embeddings into an algebraic closure.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
def embeddingToAlgebraicClosureEquiv
    [FiniteDimensional K M] [Normal K M] :
    (L →ₐ[K] M) ≃
      (L →ₐ[K] AlgebraicClosure M)
def

fixingSubextension

L87 ↗
RelativeIdeleGroup.fixingSubextension
Documentation

The subgroup of Gal(M/K) fixing the embedded copy of L.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
def fixingSubextension :
    Subgroup (M ≃ₐ[K] M)
def

restrictToSubextension

L92 ↗
RelativeIdeleGroup.restrictToSubextension
Documentation

Restriction of an automorphism of M/K to the embedded copy of L.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
def restrictToSubextension
    (σ : M ≃ₐ[K] M) : L →ₐ[K] M
def

liftSubextensionEmbedding

L99 ↗
RelativeIdeleGroup.liftSubextensionEmbedding
Documentation

Extend an embedding L →ₐ[K] M to an automorphism of the normal extension M/K.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
def liftSubextensionEmbedding
    [Normal K M] (f : L →ₐ[K] M) :
    M ≃ₐ[K] M
theorem

restrict_liftSubextensionEmbedding

L105 ↗
RelativeIdeleGroup.restrict_liftSubextensionEmbedding
Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
theorem restrict_liftSubextensionEmbedding
    [Normal K M] (f : L →ₐ[K] M) :
    restrictToSubextension
        (liftSubextensionEmbedding f) = f
def

cosetToEmbedding

L114 ↗
RelativeIdeleGroup.cosetToEmbedding
Documentation

The canonical map from right cosets of the fixing subgroup to embeddings of the subextension.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
def cosetToEmbedding
    [Normal K M] :
    (M ≃ₐ[K] M) ⧸
        fixingSubextension (K := K) (L := L) (M := M) →
      (L →ₐ[K] M)
def

cosetEquivEmbedding

L138 ↗
RelativeIdeleGroup.cosetEquivEmbedding
Documentation

Right cosets Gal(M/K)/Gal(M/L) are canonically the K-embeddings L → M. This is the index set in the coset form of the Galois product norm formula.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · full declaration
def cosetEquivEmbedding
    [Normal K M] :
    (M ≃ₐ[K] M) ⧸
        fixingSubextension (K := K) (L := L) (M := M) ≃
      (L →ₐ[K] M) where
  toFun := cosetToEmbedding
  invFun f :=
    (liftSubextensionEmbedding f :
      (M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M))
  right_inv f :=
    restrict_liftSubextensionEmbedding f
  left_inv q := by
    refine Quotient.inductionOn' q ?_
    intro σ
    apply QuotientGroup.eq.mpr
    change
      (liftSubextensionEmbedding
          (restrictToSubextension σ))⁻¹ * σ ∈
        (IsScalarTower.toAlgHom K L M).fieldRange.fixingSubgroup
    rw [IntermediateField.mem_fixingSubgroup_iff
      (IsScalarTower.toAlgHom K L M).fieldRange]
    intro y hy
    rcases hy with ⟨x, rfl⟩
    change
      ((liftSubextensionEmbedding
          (restrictToSubextension σ))⁻¹ * σ)
          (algebraMap L M x) =
        algebraMap L M x
    rw [AlgEquiv.mul_apply]
    have hres :=
      DFunLike.congr_fun
        (restrict_liftSubextensionEmbedding
          (restrictToSubextension σ)) x
    change
      liftSubextensionEmbedding
          (restrictToSubextension σ)
          (algebraMap L M x) =
        σ (algebraMap L M x) at hres
    rw [← hres]
    exact
      (liftSubextensionEmbedding
        (restrictToSubextension σ)).symm_apply_apply
          (algebraMap L M x)
theorem

norm_eq_prod_embeddings_in_galoisExtension

L186 ↗
RelativeIdeleGroup.norm_eq_prod_embeddings_in_galoisExtension
Documentation

The field norm of a subextension, computed in an ambient finite Galois extension, is the product over all embeddings into that extension.

Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section EmbeddingsIntoGaloisExtension
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
Lean source · statement
theorem norm_eq_prod_embeddings_in_galoisExtension
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M] (x : L) :
    algebraMap K M (Algebra.norm K x) =
      ∏ f : L →ₐ[K] M, f x
instance

(anonymous instance)

L225 ↗
Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
Lean source · statement
instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M))
def

embeddingPolynomial

L233 ↗
RelativeIdeleGroup.embeddingPolynomial
Documentation

The linear polynomial representing a chosen K-embedding L → M.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
def embeddingPolynomial
    {ι : Type z} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (f : L →ₐ[K] M) :
    MvPolynomial ι M
theorem

eval_embeddingPolynomial

L244 ↗
RelativeIdeleGroup.eval_embeddingPolynomial
Source context 9 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
omit [Algebra L M] [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M] in
Lean source · full declaration
theorem eval_embeddingPolynomial
    {ι : Type z} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (f : L →ₐ[K] M)
    (x : L) :
    MvPolynomial.eval
        (fun i ↦ algebraMap K M (b.repr x i))
        (embeddingPolynomial b f) =
      f x := by
  rw [embeddingPolynomial, map_sum]
  simp only [map_mul, MvPolynomial.eval_X,
    MvPolynomial.eval_C]
  calc
    ∑ i, algebraMap K M (b.repr x i) *
        f (b i) =
      ∑ i, f ((b.repr x i) • b i) := by
        apply Finset.sum_congr rfl
        intro i hi
        simp [Algebra.smul_def]
    _ = f (∑ i, (b.repr x i) • b i) := by
      rw [map_sum]
    _ = f x := by rw [b.sum_repr]
def

embeddingProductPolynomial

L267 ↗
RelativeIdeleGroup.embeddingProductPolynomial
Documentation

The universal product over all embeddings L →ₐ[K] M.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
def embeddingProductPolynomial
    {ι : Type z} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) :
    MvPolynomial ι M
theorem

eval_embeddingProductPolynomial

L276 ↗
RelativeIdeleGroup.eval_embeddingProductPolynomial
Source context 9 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
omit [Algebra L M] [IsScalarTower K L M]
    [FiniteDimensional K M] [IsGalois K M] in
Lean source · full declaration
theorem eval_embeddingProductPolynomial
    {ι : Type z} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (x : L) :
    MvPolynomial.eval
        (fun i ↦ algebraMap K M (b.repr x i))
        (embeddingProductPolynomial
          (M := M) b) =
      ∏ f : L →ₐ[K] M, f x := by
  simp [embeddingProductPolynomial]
theorem

map_normPolynomial_eq_embeddingProductPolynomial

L288 ↗
RelativeIdeleGroup.map_normPolynomial_eq_embeddingProductPolynomial
Documentation

The determinant-norm polynomial becomes the product of all embeddings after extending coefficients to the ambient Galois field.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
theorem map_normPolynomial_eq_embeddingProductPolynomial
    [Infinite K]
    {ι : Type z} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) :
    MvPolynomial.map (algebraMap K M)
        (normPolynomial b) =
      embeddingProductPolynomial (M := M) b
def

scalarEmbedding

L327 ↗
RelativeIdeleGroup.scalarEmbedding
Documentation

Scalar extension of an embedding L → M on tensor algebras.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
def scalarEmbedding
    (A : Type*) [CommRing A] [Algebra K A]
    (f : L →ₐ[K] M) :
    A ⊗[K] L →ₐ[A] A ⊗[K] M
theorem

scalarEmbedding_tmul

L338 ↗
RelativeIdeleGroup.scalarEmbedding_tmul
Source context 9 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
omit [Algebra L M] [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M] in
Lean source · statement
theorem scalarEmbedding_tmul
    (A : Type*) [CommRing A] [Algebra K A]
    (f : L →ₐ[K] M) (a : A) (x : L) :
    scalarEmbedding A f (a ⊗ₜ[K] x) =
      a ⊗ₜ[K] f x
theorem

eval₂_embeddingPolynomial_baseChange

L350 ↗
RelativeIdeleGroup.eval₂_embeddingPolynomial_baseChange
Documentation

Evaluation of an embedding polynomial after arbitrary scalar extension is the corresponding tensor-algebra embedding.

Source context 9 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
omit [Algebra L M] [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M] in
Lean source · full declaration
theorem eval₂_embeddingPolynomial_baseChange
    (A : Type*) [CommRing A] [Algebra K A]
    {ι : Type z} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (f : L →ₐ[K] M)
    (x : A ⊗[K] L) :
    MvPolynomial.eval₂
        ((Algebra.TensorProduct.includeRight
          (R := K) (A := A) (B := M)).toRingHom)
        (fun i ↦
          (Algebra.TensorProduct.includeLeft
            (R := K) (S := K) (A := A) (B := M))
            ((Algebra.TensorProduct.basis A b).repr x i))
        (embeddingPolynomial b f) =
      scalarEmbedding A f x := by
  simp only [embeddingPolynomial,
    MvPolynomial.eval₂_sum,
    MvPolynomial.eval₂_mul,
    MvPolynomial.eval₂_X,
    MvPolynomial.eval₂_C]
  calc
    ∑ i,
        (Algebra.TensorProduct.includeLeft
          (R := K) (S := K) (A := A) (B := M))
          ((Algebra.TensorProduct.basis A b).repr x i) *
        (Algebra.TensorProduct.includeRight
          (R := K) (A := A) (B := M))
          (f (b i)) =
      ∑ i, scalarEmbedding A f
        (((Algebra.TensorProduct.basis A b).repr x i) •
          Algebra.TensorProduct.basis A b i) := by
        apply Finset.sum_congr rfl
        intro i hi
        simp [Algebra.TensorProduct.basis_apply,
          Algebra.TensorProduct.tmul_mul_tmul,
          Algebra.smul_def]
    _ = scalarEmbedding A f
        (∑ i,
          ((Algebra.TensorProduct.basis A b).repr x i) •
            Algebra.TensorProduct.basis A b i) := by
      rw [map_sum]
    _ = scalarEmbedding A f x := by
      rw [(Algebra.TensorProduct.basis A b).sum_repr]
theorem

includeLeft_norm_eq_prod_scalarEmbeddings

L395 ↗
RelativeIdeleGroup.includeLeft_norm_eq_prod_scalarEmbeddings
Documentation

Full scalar-extension norm formula for a subextension of a finite Galois extension.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
theorem includeLeft_norm_eq_prod_scalarEmbeddings
    [Infinite K]
    (A : Type*) [CommRing A] [Algebra K A]
    [Nontrivial A] (x : A ⊗[K] L) :
    (Algebra.TensorProduct.includeLeft
      (R := K) (S := K) (A := A) (B := M))
        (Algebra.norm A x) =
      ∏ f : L →ₐ[K] M,
        scalarEmbedding A f x
theorem

includeLeft_norm_eq_prod_galoisCosets

L452 ↗
RelativeIdeleGroup.includeLeft_norm_eq_prod_galoisCosets
Documentation

Coset form of the scalar-extension formula. The product is indexed by Gal(M/K) / Gal(M/L).

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section UniversalPolynomial
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
theorem includeLeft_norm_eq_prod_galoisCosets
    [Infinite K]
    (A : Type*) [CommRing A] [Algebra K A]
    [Nontrivial A] (x : A ⊗[K] L) :
    (Algebra.TensorProduct.includeLeft
      (R := K) (S := K) (A := A) (B := M))
        (Algebra.norm A x) =
      ∏ q :
          (M ≃ₐ[K] M) ⧸
            fixingSubextension
              (K := K) (L := L) (M := M),
        scalarEmbedding A
          (cosetEquivEmbedding q) x
instance

(anonymous instance)

L497 ↗
Source context 7 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section RelativeAdeles
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [NumberField K]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
Lean source · statement
instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M))
def

adeleEmbedding

L506 ↗
RelativeIdeleGroup.adeleEmbedding
Documentation

A field embedding inside an ambient Galois extension, extended to relative adèles.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section RelativeAdeles
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [NumberField K]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
def adeleEmbedding (f : L →ₐ[K] M) :
    RelativeAdeleRing K L →ₐ[
      NumberField.AdeleRing (𝓞 K) K]
      RelativeAdeleRing K M
def

ideleEmbedding

L514 ↗
RelativeIdeleGroup.ideleEmbedding
Documentation

The induced homomorphism on relative idèles.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section RelativeAdeles
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [NumberField K]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
def ideleEmbedding (f : L →ₐ[K] M) :
    RelativeIdeleGroup K L →*
      RelativeIdeleGroup K M
theorem

adeleInclusion_norm_eq_prod_embeddings

L520 ↗
RelativeIdeleGroup.adeleInclusion_norm_eq_prod_embeddings
Documentation

The embedded-subextension adèle form of the Galois product norm formula.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section RelativeAdeles
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [NumberField K]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
theorem adeleInclusion_norm_eq_prod_embeddings
    (x : RelativeAdeleRing K L) :
    adeleInclusion K M
        (Algebra.norm
          (NumberField.AdeleRing (𝓞 K) K) x) =
      ∏ f : L →ₐ[K] M,
        adeleEmbedding f x
theorem

inclusion_norm_eq_prod_embeddings

L533 ↗
RelativeIdeleGroup.inclusion_norm_eq_prod_embeddings
Documentation

The embedded-subextension idèle form of the Galois product norm formula.

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section RelativeAdeles
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [NumberField K]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
theorem inclusion_norm_eq_prod_embeddings
    (a : RelativeIdeleGroup K L) :
    inclusion K M (norm K L a) =
      ∏ f : L →ₐ[K] M,
        ideleEmbedding f a
theorem

inclusion_norm_eq_prod_galoisCosets

L551 ↗
RelativeIdeleGroup.inclusion_norm_eq_prod_galoisCosets
Documentation

The literal coset form for arbitrary relative idèles:

i_{M/K}(N_{L/K}(a)) = ∏_{σ ∈ Gal(M/K)/Gal(M/L)} σ(a).

Source context 8 commands

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

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w z
section RelativeAdeles
variable
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [NumberField K]
    [Algebra K L] [Algebra K M] [Algebra L M]
    [IsScalarTower K L M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K M]
local instance :
    Fintype
      ((M ≃ₐ[K] M) ⧸
        fixingSubextension
          (K := K) (L := L) (M := M)) :=
  Fintype.ofFinite _
Lean source · statement
theorem inclusion_norm_eq_prod_galoisCosets
    (a : RelativeIdeleGroup K L) :
    inclusion K M (norm K L a) =
      ∏ q :
          (M ≃ₐ[K] M) ⧸
            fixingSubextension
              (K := K) (L := L) (M := M),
        ideleEmbedding
          (cosetEquivEmbedding q) a

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