Module

TensorProductProductFormulas.lean

Nyll.ValuedFieldTheory.Valuation.Completion.TensorProductProductFormulas

3 declarations indexed from sourceView source ↗

Module documentation

Degree, norm, and trace through a tensor-product decomposition

These are the purely linear-algebraic implications for a finite product decomposition. They deliberately state the product terms as the components of a supplied algebra equivalence. A tensor-product decomposition identifies those components with the canonical images in L_w; no compatibility theorem is assumed here.

Imports2

Imported by2

theorem

baseChange_pi_finrank_eq_sum

L33 ↗

ValuationTheory.Completion.baseChange_pi_finrank_eq_sum

Documentation

Finite rank is the sum of the ranks of the factors in a finite dependent-product decomposition after 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

Lean source · statement

theorem baseChange_pi_finrank_eq_sum
    {K : Type u} {A : Type v} {L : Type w}
    [Field K] [Field A] [Field L] [Algebra K A] [Algebra K L]
    [FiniteDimensional K L]
    {I : Type*} [Fintype I]
    (B : I → Type*) [∀ i, Field (B i)] [∀ i, Algebra A (B i)]
    [∀ i, Module.Finite A (B i)]
    (e : A ⊗[K] L ≃ₐ[A] ∀ i, B i) :
    Module.finrank K L = ∑ i, Module.finrank A (B i)

theorem

baseChange_pi_norm_eq_prod

L50 ↗

ValuationTheory.Completion.baseChange_pi_norm_eq_prod

Documentation

The base-changed global norm is the product of the norms of the components under a finite dependent-product decomposition.

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

Lean source · statement

theorem baseChange_pi_norm_eq_prod
    {K : Type u} {A : Type v} {L : Type w}
    [Field K] [Field A] [Field L] [Algebra K A] [Algebra K L]
    [FiniteDimensional K L]
    {I : Type*} [Fintype I]
    (B : I → Type*) [∀ i, Field (B i)] [∀ i, Algebra A (B i)]
    [∀ i, Module.Finite A (B i)]
    (e : A ⊗[K] L ≃ₐ[A] ∀ i, B i) (x : L) :
    algebraMap K A (Algebra.norm K x) =
      ∏ i, Algebra.norm A (e (1 ⊗ₜ[K] x) i)

theorem

baseChange_pi_trace_eq_sum

L71 ↗

ValuationTheory.Completion.baseChange_pi_trace_eq_sum

Documentation

The base-changed global trace is the sum of the traces of the components under a finite dependent-product decomposition.

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

Lean source · statement

theorem baseChange_pi_trace_eq_sum
    {K : Type u} {A : Type v} {L : Type w}
    [Field K] [Field A] [Field L] [Algebra K A] [Algebra K L]
    [FiniteDimensional K L]
    {I : Type*} [Fintype I]
    (B : I → Type*) [∀ i, Field (B i)] [∀ i, Algebra A (B i)]
    [∀ i, Module.Finite A (B i)]
    (e : A ⊗[K] L ≃ₐ[A] ∀ i, B i) (x : L) :
    algebraMap K A (Algebra.trace K L x) =
      ∑ i, Algebra.trace A (B i) (e (1 ⊗ₜ[K] x) i)

Module documentation

Degree, norm, and trace through a tensor-product decomposition

Declarations

baseChange_pi_finrank_eq_sum

baseChange_pi_norm_eq_prod

baseChange_pi_trace_eq_sum