Module

BaseChangeAdjoinRoot.lean

Nyll.ValuedFieldTheory.Valuation.Completion.BaseChangeAdjoinRoot

11 declarations indexed from sourceView source ↗

Module documentation

A primitive extension after scalar extension

If L/K has power basis generated by α, then the scalar extension A ⊗[K] L is canonically A[X]/(minpoly_K(α)). The equivalence below is the canonical algebra equivalence used in scalar-extension decompositions.

Imports4

Mathlib.FieldTheory.PrimitiveElement
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.RingTheory.AdjoinRoot
Mathlib.RingTheory.TensorProduct.Free

Imported by3

def

powerBasisBaseChange

L30 ↗

ValuationTheory.Completion.powerBasisBaseChange

Documentation

Scalar extension of a power basis.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · full declaration

def powerBasisBaseChange
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) : PowerBasis A (A ⊗[K] L) where
  gen := 1 ⊗ₜ[K] pb.gen
  dim := pb.dim
  basis := Algebra.TensorProduct.basis A pb.basis
  basis_eq_pow i := by
    rw [Algebra.TensorProduct.basis_apply, pb.basis_eq_pow]
    simp [Algebra.TensorProduct.tmul_pow]

theorem

powerBasisBaseChange_gen

L43 ↗

ValuationTheory.Completion.powerBasisBaseChange_gen

Documentation

The generator of a base-changed power basis is the tensor of one with the old generator.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem powerBasisBaseChange_gen
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    (powerBasisBaseChange (A := A) pb).gen = 1 ⊗ₜ[K] pb.gen

theorem

minpoly_map_aeval_one_tmul

L51 ↗

ValuationTheory.Completion.minpoly_map_aeval_one_tmul

Documentation

The mapped primitive polynomial vanishes at 1 ⊗ α.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem minpoly_map_aeval_one_tmul
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    Polynomial.aeval (1 ⊗ₜ[K] pb.gen : A ⊗[K] L)
      ((minpoly K pb.gen).map (algebraMap K A)) = 0

def

adjoinRootToBaseChange

L65 ↗

ValuationTheory.Completion.adjoinRootToBaseChange

Documentation

The canonical algebra map from the mapped primitive quotient to the scalar extension.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

def adjoinRootToBaseChange
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    AdjoinRoot ((minpoly K pb.gen).map (algebraMap K A)) →ₐ[A]
      A ⊗[K] L

theorem

adjoinRootToBaseChange_root

L79 ↗

ValuationTheory.Completion.adjoinRootToBaseChange_root

Documentation

The map from an adjoined-root algebra to its base change sends root to root.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem adjoinRootToBaseChange_root
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    adjoinRootToBaseChange (A := A) pb
        (AdjoinRoot.root ((minpoly K pb.gen).map (algebraMap K A))) =
      1 ⊗ₜ[K] pb.gen

theorem

adjoinRootToBaseChange_surjective

L89 ↗

ValuationTheory.Completion.adjoinRootToBaseChange_surjective

Documentation

The canonical map from the adjoined-root algebra onto its base change is surjective.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem adjoinRootToBaseChange_surjective
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    Function.Surjective (adjoinRootToBaseChange (A := A) pb)

theorem

adjoinRoot_baseChange_finrank_eq

L110 ↗

ValuationTheory.Completion.adjoinRoot_baseChange_finrank_eq

Documentation

The mapped primitive quotient and scalar extension have equal dimension.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem adjoinRoot_baseChange_finrank_eq
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    Module.finrank A
        (AdjoinRoot ((minpoly K pb.gen).map (algebraMap K A))) =
      Module.finrank A (A ⊗[K] L)

def

adjoinRootEquivBaseChange

L131 ↗

ValuationTheory.Completion.adjoinRootEquivBaseChange

Documentation

Canonical scalar-extension presentation, in the quotient-to-tensor direction.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

def adjoinRootEquivBaseChange
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    AdjoinRoot ((minpoly K pb.gen).map (algebraMap K A)) ≃ₐ[A]
      A ⊗[K] L

theorem

adjoinRootEquivBaseChange_root

L152 ↗

ValuationTheory.Completion.adjoinRootEquivBaseChange_root

Documentation

The adjoined-root/base-change equivalence preserves the distinguished root.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem adjoinRootEquivBaseChange_root
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    adjoinRootEquivBaseChange (A := A) pb
        (AdjoinRoot.root ((minpoly K pb.gen).map (algebraMap K A))) =
      1 ⊗ₜ[K] pb.gen

def

baseChangeEquivAdjoinRoot

L164 ↗

ValuationTheory.Completion.baseChangeEquivAdjoinRoot

Documentation

Canonical scalar-extension presentation of a primitive field extension.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

def baseChangeEquivAdjoinRoot
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    A ⊗[K] L ≃ₐ[A]
      AdjoinRoot ((minpoly K pb.gen).map (algebraMap K A))

theorem

baseChangeEquivAdjoinRoot_one_tmul_gen

L174 ↗

ValuationTheory.Completion.baseChangeEquivAdjoinRoot_one_tmul_gen

Documentation

The inverse base-change equivalence sends 1 ⊗ gen to the adjoined root.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct Polynomial

Lean source · statement

theorem baseChangeEquivAdjoinRoot_one_tmul_gen
    {K A L : Type*} [Field K] [Field A] [Field L]
    [Algebra K A] [Algebra K L]
    (pb : PowerBasis K L) :
    baseChangeEquivAdjoinRoot (A := A) pb (1 ⊗ₜ[K] pb.gen) =
      AdjoinRoot.root ((minpoly K pb.gen).map (algebraMap K A))

Module documentation

A primitive extension after scalar extension

Declarations