Module

SeparableNormProduct.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.SeparableNormProduct

3 declarations indexed from sourceView source ↗

Module documentation

Separable field norms as products of embeddings

For a finite separable extension, the field norm becomes the product over all base-field embeddings after mapping into a separably closed ambient field. The ambient field need not be a normal extension of the base field.

Imports4

Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.Norm.Transitivity
Mathlib.RingTheory.AlgebraTower

Imported by3

instance

finiteSeparableAlgHomFintypeForNormProduct

L28 ↗

LocalClassFieldTheory.finiteSeparableAlgHomFintypeForNormProduct

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory

Lean source · statement

instance finiteSeparableAlgHomFintypeForNormProduct
    {k E T : Type} [Field k] [Field E] [Field T]
    [Algebra k E] [Algebra k T]
    [FiniteDimensional k E] [Algebra.IsSeparable k E] :
    Fintype (E →ₐ[k] T)

theorem

prod_embeddings_algebraMap_powerBasisGen_eq

L37 ↗

LocalClassFieldTheory.prod_embeddings_algebraMap_powerBasisGen_eq

Documentation

The embeddings of a finite separable tower above a power-basis generator split into embeddings of the lower field and their extensions.

Source context 4 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
noncomputable local instance finiteSeparableAlgHomFintypeForNormProduct
    {k E T : Type} [Field k] [Field E] [Field T]
    [Algebra k E] [Algebra k T]
    [FiniteDimensional k E] [Algebra.IsSeparable k E] :
    Fintype (E →ₐ[k] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable k E)

Lean source · full declaration

theorem prod_embeddings_algebraMap_powerBasisGen_eq
    (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsSepClosed Ω]
    {L E : Type} [Field L] [Field E]
    [Algebra k L] [Algebra k E] [Algebra L E] [IsScalarTower k L E]
    [FiniteDimensional k L] [Algebra.IsSeparable k L]
    [Algebra.IsSeparable k E] [FiniteDimensional k E]
    (pb : PowerBasis k L) :
    ∏ σ : E →ₐ[k] Ω, σ (algebraMap L E pb.gen) =
      ((@Finset.univ (L →ₐ[k] Ω) (PowerBasis.AlgHom.fintype pb)).prod
        (fun σ => σ pb.gen)) ^ Module.finrank L E := by
  have : FiniteDimensional L E := FiniteDimensional.right k L E
  have : Algebra.IsSeparable L E :=
    Algebra.isSeparable_tower_top_of_isSeparable k L E
  let : Fintype (L →ₐ[k] Ω) := PowerBasis.AlgHom.fintype pb
  rw [Fintype.prod_equiv algHomEquivSigma
    (fun σ : E →ₐ[k] Ω => σ (algebraMap L E pb.gen))
    (fun σ => σ.1 pb.gen)]
  · rw [← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow]
    refine Finset.prod_congr rfl fun σ _ => ?_
    let : Algebra L Ω := σ.toRingHom.toAlgebra
    simp_rw [Finset.prod_const]
    congr
    rw [Finset.card_univ, Fintype.card_eq_nat_card]
    exact AlgHom.natCard_of_splits L E Ω (fun x =>
      IsSepClosed.splits_codomain _ (Algebra.IsSeparable.isSeparable L x))
  · intro σ
    change σ (algebraMap L E pb.gen) =
      (σ.comp (IsScalarTower.toAlgHom k L E)) pb.gen
    exact (AlgHom.comp_apply σ (IsScalarTower.toAlgHom k L E) pb.gen).symm

theorem

algebraMap_norm_eq_prod_embeddings_of_isSepClosed

L69 ↗

LocalClassFieldTheory.algebraMap_norm_eq_prod_embeddings_of_isSepClosed

Documentation

Mapping the norm of an element of a finite separable extension into a separably closed field gives the product of all base-field embeddings.

Source context 4 commands

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

noncomputable section
open scoped BigOperators
namespace LocalClassFieldTheory
noncomputable local instance finiteSeparableAlgHomFintypeForNormProduct
    {k E T : Type} [Field k] [Field E] [Field T]
    [Algebra k E] [Algebra k T]
    [FiniteDimensional k E] [Algebra.IsSeparable k E] :
    Fintype (E →ₐ[k] T) :=
  PowerBasis.AlgHom.fintype (Field.powerBasisOfFiniteOfSeparable k E)

Lean source · statement

theorem algebraMap_norm_eq_prod_embeddings_of_isSepClosed
    (k Ω E : Type) [Field k] [Field Ω] [Field E]
    [Algebra k Ω] [IsSepClosed Ω] [Algebra k E]
    [FiniteDimensional k E] [Algebra.IsSeparable k E]
    (x : E) :
    algebraMap k Ω (Algebra.norm k x) = ∏ σ : E →ₐ[k] Ω, σ x

Module documentation

Separable field norms as products of embeddings

Declarations

finiteSeparableAlgHomFintypeForNormProduct

prod_embeddings_algebraMap_powerBasisGen_eq

algebraMap_norm_eq_prod_embeddings_of_isSepClosed