Documentation

Mathlib.LinearAlgebra.PiTensorProduct.Basis

Basis for PiTensorProduct #

This file constructs a basis for PiTensorProduct given bases on the component spaces.

source
noncomputable def Basis.piTensorProduct {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Finite ι] (b : (i : ι) → Module.Basis (κ i) R (M i)) :
Module.Basis ((i : ι) → κ i) R (PiTensorProduct R fun (i : ι) => M i)

Let ι be a Finite type and M be a family of modules indexed by ι. If b i : κ i → M i is a basis for every i in ι, then fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i) is a basis of ⨂[R] i, M i.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Basis.piTensorProduct_repr_tprod_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (b : (i : ι) → Module.Basis (κ i) R (M i)) (x : (i : ι) → M i) (p : (i : ι) → κ i) :
    ((piTensorProduct b).repr ((PiTensorProduct.tprod R) x)) p = ∏ i : ι, ((b i).repr (x i)) (p i)
    source
    @[simp]
    theorem Basis.piTensorProduct_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Finite ι] (b : (i : ι) → Module.Basis (κ i) R (M i)) (p : (i : ι) → κ i) :
    (piTensorProduct b) p = ⨂ₜ[R] (i : ι), (b i) (p i)