Bases for the product of modules

noncomputable def Module.Basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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 }

@[simp]

theorem Module.Basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

@[simp]

theorem Module.Basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

theorem Module.Basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

theorem Module.Basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

theorem Module.Basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

theorem Module.Basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

@[simp]

theorem Module.Basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [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

instance Module.Free.prod (R : Type u_6) (M : Type u_7) (N : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Free R M] [Free R N] : Free R (M × N)