Products of submodules

Products of submodules preserve indexed suprema and independence of families of submodules, and the two coordinate copies Submodule.fst and Submodule.snd of the factors of a product module are cut out by the vanishing of the other coordinate and are complementary.

Main declarations

• TauCeti.iSup_prod_submodule: products commute with indexed suprema.
• TauCeti.iSupIndep.prod: products of independent families are independent.
• Submodule.mem_fst_iff, Submodule.mem_snd_iff: membership in the coordinate copies of the factors.
• Submodule.isCompl_fst_snd: the coordinate copies of the two factors are complementary.

@[simp]

theorem Submodule.mem_fst_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {x : M × N} : x ∈ fst R M N ↔ x.2 = 0

A vector of a product module lies in the copy of the first factor exactly when its second coordinate vanishes.

@[simp]

theorem Submodule.mem_snd_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {x : M × N} : x ∈ snd R M N ↔ x.1 = 0

A vector of a product module lies in the copy of the second factor exactly when its first coordinate vanishes.

theorem Submodule.isCompl_fst_snd (R : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : IsCompl (fst R M N) (snd R M N)

The copies of the two factors of a product module are complementary submodules.

@[simp]

theorem TauCeti.iSup_prod_submodule {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Sort u_4} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (P : ι → Submodule R M) (Q : ι → Submodule R N) : ⨆ (i : ι), (P i).prod (Q i) = (⨆ (i : ι), P i).prod (⨆ (i : ι), Q i)

Taking products of submodules commutes with indexed suprema, including the empty one.

theorem TauCeti.iSupIndep.prod {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Sort u_4} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {P : ι → Submodule R M} {Q : ι → Submodule R N} (hP : iSupIndep P) (hQ : iSupIndep Q) : iSupIndep fun (i : ι) => (P i).prod (Q i)

Componentwise products of independent families of submodules are independent.

Use TauCeti.iSupIndep.prod hP hQ, or hP.prod hQ after open TauCeti.