Basis for PiTensorProduct #
This file constructs a basis for PiTensorProduct given bases on the component spaces.
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
@[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)
:
@[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)
: