Quotients by products of submodules

The quotient by a product submodule is the product of the two quotients:

(M × N) ⧸ p.prod q ≃ₗ (M ⧸ p) × (N ⧸ q).

Mathlib has the additive-group form of this statement, QuotientAddGroup.prodAddEquiv; quotientProdEquiv below records the analogous scalar-compatible equivalence, which is the form module-theoretic consumers need. There is no submodule form upstream.

Main declarations

• Submodule.quotientProdEquiv: (M × N) ⧸ p.prod q ≃ₗ (M ⧸ p) × (N ⧸ q).
• Submodule.finrank_quotient_prod: the ranks of the quotients add.

Implementation notes

quotientProdEquiv is assembled from Submodule.liftQ and LinearMap.coprod, so its computation rules are stated in the Submodule.Quotient.mk API rather than through AddEquiv wrappers.

def Submodule.quotientProdEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (p : Submodule R M) (q : Submodule R N) : ((M × N) ⧸ p.prod q) ≃ₗ[R] (M ⧸ p) × N ⧸ q

The quotient by a product of submodules is the product of the quotients.

This is the module analogue of QuotientAddGroup.prodAddEquiv. Its action and inverse action on quotient representatives are recorded by quotientProdEquiv_apply_mk and quotientProdEquiv_symm_apply_mk.

Equations

• p.quotientProdEquiv q = LinearEquiv.ofLinearMap (Submodule.quotientProdMap✝ p q) (Submodule.quotientProdInvMap✝ p q) ⋯ ⋯

@[simp]

theorem Submodule.quotientProdEquiv_apply_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (p : Submodule R M) (q : Submodule R N) (x : M × N) : (p.quotientProdEquiv q) (Quotient.mk x) = (Quotient.mk x.1, Quotient.mk x.2)

@[simp]

theorem Submodule.quotientProdEquiv_symm_apply_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (p : Submodule R M) (q : Submodule R N) (x : M) (y : N) : (p.quotientProdEquiv q).symm (Quotient.mk x, Quotient.mk y) = Quotient.mk (x, y)

@[simp]

theorem Submodule.finrank_quotient_prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [StrongRankCondition R] (p : Submodule R M) (q : Submodule R N) [Module.Free R (M ⧸ p)] [Module.Free R (N ⧸ q)] [Module.Finite R (M ⧸ p)] [Module.Finite R (N ⧸ q)] : Module.finrank R ((M × N) ⧸ p.prod q) = Module.finrank R (M ⧸ p) + Module.finrank R (N ⧸ q)

The quotient by a product of submodules has rank the sum of the two quotients' ranks.