# Bases for the product of modules #

source
def Module.Basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') :
Basis (ι ⊕ ι') R (M × M')

`Basis.prod` maps an `ι`-indexed basis for `M` and an `ι'`-indexed basis for `M'` to an `ι ⊕ ι'`-index basis for `M × M'`. For the specific case of `R × R`, see also `Basis.finTwoProd`.

Equations

- b.prod b' = { repr := b.repr.prodCongr b'.repr ≪≫ₗ (Finsupp.sumFinsuppLEquivProdFinsupp R).symm }

Instances For

source
@[simp]
theorem Module.Basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (x : M × M') (i : ι) :
((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i
source
@[simp]
theorem Module.Basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (x : M × M') (i : ι') :
((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i
source
theorem Module.Basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι) :
((b.prod b') (Sum.inl i)).1 = b i
source
theorem Module.Basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι') :
((b.prod b') (Sum.inr i)).1 = 0
source
theorem Module.Basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι) :
((b.prod b') (Sum.inl i)).2 = 0
source
theorem Module.Basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι') :
((b.prod b') (Sum.inr i)).2 = b' i
source
@[simp]
theorem Module.Basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι ⊕ ι') :
(b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i
source
instance Module.Free.prod (R : Type u_7) (M : Type u_8) (N : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Free R M] [Free R N] :
Free R (M × N)