Module

FiniteProductNormTrace.lean

Nyll.ValuedFieldTheory.Valuation.Completion.FiniteProductNormTrace

7 declarations indexed from sourceView source ↗

Module documentation

Norms and traces on finite dependent products

These algebraic lemmas are the finite-product linear algebra used in tensor-product norm and trace formulas. Mathlib has the binary trace formula and the determinant of a binary product map; the dependent finite-product versions are recorded here so that the local factors are allowed to have different field degrees.

Imports3

Mathlib.RingTheory.Norm.Basic
Mathlib.RingTheory.Trace.Basic
Mathlib.LinearAlgebra.Dimension.Constructions

Imported by5

theorem

moduleFiniteOfPi

L34 ↗

ValuationTheory.Completion.moduleFiniteOfPi

Documentation

A component of a module-valued product is finite whenever the whole product is finite. Evaluation is a surjective linear map.

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 Module

Lean source · statement

theorem moduleFiniteOfPi
    {R : Type u} [Semiring R]
    {ι : Type v} (M : ι → Type w)
    [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
    [Module.Finite R (∀ i, M i)] (i : ι) :
    Module.Finite R (M i)

theorem

algebra_lmul_prod_eq_prodMap

L47 ↗

ValuationTheory.Completion.algebra_lmul_prod_eq_prodMap

Documentation

Multiplication on a binary product is the product of the two multiplication endomorphisms.

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 Module

Lean source · statement

theorem algebra_lmul_prod_eq_prodMap
    {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] (x : S × T) :
    Algebra.lmul R (S × T) x =
      (Algebra.lmul R S x.1).prodMap (Algebra.lmul R T x.2)

theorem

algebra_norm_prod_apply

L59 ↗

ValuationTheory.Completion.algebra_norm_prod_apply

Documentation

The algebra norm on a binary product is the product of the component norms.

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 Module

Lean source · statement

theorem algebra_norm_prod_apply
    {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T]
    [Module.Free R S] [Module.Finite R S]
    [Module.Free R T] [Module.Finite R T]
    (x : S × T) :
    Algebra.norm R x = Algebra.norm R x.1 * Algebra.norm R x.2

def

piCongrLeftAlgEquiv

L70 ↗

ValuationTheory.Completion.piCongrLeftAlgEquiv

Documentation

Reindexing a dependent product is an algebra equivalence.

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 Module

Lean source · full declaration

def piCongrLeftAlgEquiv
    {R : Type*} [CommSemiring R]
    {ι ι' : Type*} (A : ι' → Type*) [∀ i, Semiring (A i)]
    [∀ i, Algebra R (A i)] (e : ι ≃ ι') :
    ((i : ι) → A (e i)) ≃ₐ[R] ((i' : ι') → A i') where
  __ := RingEquiv.piCongrLeft A e
  commutes' r := by
    funext j
    obtain ⟨i, rfl⟩ := e.surjective j
    change (Equiv.piCongrLeft A e
      (fun i => algebraMap R (A (e i)) r)) (e i) =
        algebraMap R (A (e i)) r
    exact Equiv.piCongrLeft_apply_apply A e _ i

def

piOptionEquivProdAlgEquiv

L86 ↗

ValuationTheory.Completion.piOptionEquivProdAlgEquiv

Documentation

Splitting the none coordinate from an Option-indexed dependent product is an algebra equivalence.

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 Module

Lean source · full declaration

def piOptionEquivProdAlgEquiv
    {R : Type*} [CommSemiring R]
    {ι : Type*} (A : Option ι → Type*) [∀ i, Semiring (A i)]
    [∀ i, Algebra R (A i)] :
    ((i : Option ι) → A i) ≃ₐ[R] (A none × ((i : ι) → A (some i))) where
  __ := RingEquiv.piOptionEquivProd
  commutes' _ := rfl

theorem

algebra_norm_pi_apply

L96 ↗

ValuationTheory.Completion.algebra_norm_pi_apply

Documentation

The algebra norm of an element of a finite dependent product is the product of its component norms.

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 Module

Lean source · statement

theorem algebra_norm_pi_apply
    {R : Type u} [CommRing R]
    {ι : Type v} [Fintype ι]
    (A : ι → Type w) [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    [∀ i, Module.Free R (A i)] [∀ i, Module.Finite R (A i)]
    (x : ∀ i, A i) :
    Algebra.norm R x = ∏ i, Algebra.norm R (x i)

theorem

algebra_trace_pi_apply

L147 ↗

ValuationTheory.Completion.algebra_trace_pi_apply

Documentation

The algebra trace of an element of a finite dependent product is the sum of its component traces.

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 Module

Lean source · statement

theorem algebra_trace_pi_apply
    {R : Type u} [CommRing R]
    {ι : Type v} [Fintype ι]
    (A : ι → Type w) [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    [∀ i, Module.Free R (A i)] [∀ i, Module.Finite R (A i)]
    (x : ∀ i, A i) :
    Algebra.trace R (∀ i, A i) x = ∑ i, Algebra.trace R (A i) (x i)

Module documentation

Norms and traces on finite dependent products

Declarations

moduleFiniteOfPi

algebra_lmul_prod_eq_prodMap

algebra_norm_prod_apply

piCongrLeftAlgEquiv

piOptionEquivProdAlgEquiv

algebra_norm_pi_apply

algebra_trace_pi_apply