Module

FiniteSubfieldTensor.lean

Nyll.ValuedFieldTheory.Valuation.Completion.FiniteSubfieldTensor

1 declaration indexed from sourceView source ↗

Module documentation

Tensor elements over finite intermediate fields

Only finitely many coefficients from the algebraic extension occur in a tensor element. Adjoining those coefficients gives a finite intermediate field over which the element is already defined.

Imports5

Mathlib.LinearAlgebra.TensorProduct.Finiteness
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.Algebraic.Integral
Mathlib.Algebra.BigOperators.Group.Finset.Basic

Imported by4

theorem

exists_finiteSubfield_tensor_lift

L27 ↗

ValuationTheory.Completion.exists_finiteSubfield_tensor_lift

Documentation

Every tensor element over an algebraic field extension lifts from a finite intermediate field, along its actual inclusion into the extension.

Source context 2 commands

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

namespace ValuationTheory.Completion
open scoped TensorProduct BigOperators

Lean source · statement

theorem exists_finiteSubfield_tensor_lift
    {K A L : Type*} [Field K] [CommRing A] [Field L]
    [Algebra K A] [Algebra K L] [Algebra.IsAlgebraic K L]
    (z : A ⊗[K] L) :
    ∃ F : IntermediateField K L, FiniteDimensional K F ∧
      ∃ w : A ⊗[K] F,
        Algebra.TensorProduct.map (R := K) (S := A) (AlgHom.id A A) F.val w = z

Module documentation

Tensor elements over finite intermediate fields

Declarations

exists_finiteSubfield_tensor_lift