Module

TensorProduct.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.TensorProduct

5 declarations indexed from sourceView source ↗

Module documentation

Coprime tensor-product base change of a Galois extension

The roots-of-unity descent uses the following concrete fact. If finite field extensions M / K and L / K have coprime degrees, then M ⊗[K] L is a field. If L / K is Galois, the resulting extension over M is Galois of the same degree.

The proof constructs the field structure from linear disjointness. For Galoisness, every automorphism of L / K is extended by id_M ⊗ σ; these distinct automorphisms already account for the full dimension of the tensor product.

Imports3

Mathlib.FieldTheory.LinearDisjoint
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.LinearAlgebra.TensorProduct.Basis

Imported by2

theorem

tensorProduct_isField_of_finrank_coprime

L42 ↗

Documentation

Coprime finite field extensions are linearly disjoint, hence their tensor product is a field.

Source context 4 commands

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

open scoped TensorProduct
noncomputable section
universe u
variable
    (K M L : Type u)
    [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra K L]
    [hKM : FiniteDimensional K M]
    [hKL : FiniteDimensional K L]

Lean source · statement

theorem tensorProduct_isField_of_finrank_coprime
    (hcoprime :
      (Module.finrank K M).Coprime
        (Module.finrank K L)) :
    IsField (M ⊗[K] L)

def

tensorBaseChangeAut

L75 ↗

Documentation

Extend a K-automorphism of L to the coprime tensor base change, fixing the left factor M.

Source context 6 commands

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

open scoped TensorProduct
noncomputable section
universe u
variable
    (K M L : Type u)
    [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra K L]
    [hKM : FiniteDimensional K M]
    [hKL : FiniteDimensional K L]
section TensorAutomorphisms
variable [hGalois : IsGalois K L]

Lean source · statement

def tensorBaseChangeAut
    (σ : L ≃ₐ[K] L) :
    (M ⊗[K] L) ≃ₐ[M] (M ⊗[K] L)

theorem

tensorBaseChangeAut_tmul

L86 ↗

Source context 7 commands

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

open scoped TensorProduct
noncomputable section
universe u
variable
    (K M L : Type u)
    [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra K L]
    [hKM : FiniteDimensional K M]
    [hKL : FiniteDimensional K L]
section TensorAutomorphisms
variable [hGalois : IsGalois K L]
omit hKM hKL hGalois in

Lean source · statement

theorem tensorBaseChangeAut_tmul
    (σ : L ≃ₐ[K] L)
    (m : M) (x : L) :
    tensorBaseChangeAut K M L σ (m ⊗ₜ[K] x) =
      m ⊗ₜ[K] σ x

theorem

tensorBaseChangeAut_injective

L95 ↗

Documentation

Distinct automorphisms remain distinct after tensor base change.

Source context 7 commands

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

open scoped TensorProduct
noncomputable section
universe u
variable
    (K M L : Type u)
    [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra K L]
    [hKM : FiniteDimensional K M]
    [hKL : FiniteDimensional K L]
section TensorAutomorphisms
variable [hGalois : IsGalois K L]
omit hKM hKL hGalois in

Lean source · statement

theorem tensorBaseChangeAut_injective :
    Function.Injective (tensorBaseChangeAut K M L)

theorem

tensorProduct_isGalois_of_finrank_coprime

L113 ↗

Documentation

Galoisness survives the coprime tensor-product base change.

Source context 6 commands

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

open scoped TensorProduct
noncomputable section
universe u
variable
    (K M L : Type u)
    [Field K] [Field M] [Field L]
    [Algebra K M] [Algebra K L]
    [hKM : FiniteDimensional K M]
    [hKL : FiniteDimensional K L]
section TensorAutomorphisms
variable [hGalois : IsGalois K L]

Lean source · full declaration

theorem tensorProduct_isGalois_of_finrank_coprime
    (hcoprime :
      (Module.finrank K M).Coprime
        (Module.finrank K L)) :
    letI : Field (M ⊗[K] L) :=
      (tensorProduct_isField_of_finrank_coprime
        K M L hcoprime).toField
    IsGalois M (M ⊗[K] L) := by
  let N := M ⊗[K] L
  let : Field N :=
    (tensorProduct_isField_of_finrank_coprime
      K M L hcoprime).toField
  have hfinite : FiniteDimensional M N := by
    exact Module.Finite.of_restrictScalars_finite K M N
  let : FiniteDimensional M N := hfinite
  have hlow :
      Nat.card (L ≃ₐ[K] L) ≤
        Nat.card (N ≃ₐ[M] N) :=
    Nat.card_le_card_of_injective
      (tensorBaseChangeAut K M L)
      (tensorBaseChangeAut_injective K M L)
  have hdim :
      Module.finrank M N = Module.finrank K L := by
    exact Module.finrank_baseChange
  have hlow' :
      Module.finrank M N ≤
        Nat.card (N ≃ₐ[M] N) := by
    rw [hdim, ← IsGalois.card_aut_eq_finrank K L]
    exact hlow
  have hupp :
      Nat.card (N ≃ₐ[M] N) ≤
        Module.finrank M N := by
    rw [Nat.card_eq_fintype_card]
    exact AlgEquiv.card_le
  exact
    IsGalois.of_card_aut_eq_finrank M N
      (Nat.le_antisymm hupp hlow')

Module documentation

Coprime tensor-product base change of a Galois extension

Declarations

tensorProduct_isField_of_finrank_coprime

tensorBaseChangeAut

tensorBaseChangeAut_tmul

tensorBaseChangeAut_injective

tensorProduct_isGalois_of_finrank_coprime