Complementary submodules under restriction, quotients and products

Three ways complementarity of a pair of submodules survives a construction.

Restriction to a subspace. Mathlib's Submodule.isCompl_comap_subtype_of_isCompl_of_le restricts a complementary pair to a subspace that contains one of the two. This file records the variant that applies when neither member of the pair lies in the subspace: a disjoint pair cuts a subspace U into a complementary pair as soon as the two intersections with U span U — for a general U a genuine hypothesis, not a consequence of spanning the ambient module.

Quotients. The images of two submodules A and B in M ⧸ p are complementary exactly when A ⊔ p and B ⊔ p meet in p and A, B and p together span M. This is the form in which opposedness of filtrations induced on a graded piece is checked in the ambient module.

Products. Complementarity is also preserved by products: a complementary pair in E and one in F give a complementary pair in E × F. This is what lets a direct-sum decomposition be built factor by factor, and it is used that way for the doubled totally real modules in TauCeti/LinearAlgebra/TotallyReal/Basic.lean.

Main results

• TauCeti.Submodule.isCompl_comap_subtype: a disjoint pair of submodules whose intersections with U span U restricts to a complementary pair of submodules of U.
• Submodule.isCompl_map_mkQ_iff: complementarity of images in a quotient, read in the ambient module.
• IsCompl.prod: a product of complementary pairs is complementary.

theorem TauCeti.Submodule.isCompl_comap_subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {U A B : Submodule R M} (hAB : Disjoint A B) (hU : U ≤ U ⊓ A ⊔ U ⊓ B) : IsCompl (Submodule.comap U.subtype A) (Submodule.comap U.subtype B)

A disjoint pair of submodules whose intersections with a subspace U span U cuts U into a complementary pair of submodules.

theorem Submodule.isCompl_map_mkQ_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {p A B : Submodule R M} : IsCompl (map p.mkQ A) (map p.mkQ B) ↔ (p ⊔ A) ⊓ (p ⊔ B) ≤ p ∧ p ⊔ (A ⊔ B) = ⊤

The images of two submodules in the quotient by p are complementary exactly when, after adding p, they meet in p, and together with p they span the whole module.

theorem IsCompl.prod {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] {L₁ L₂ : Submodule R E} {M₁ M₂ : Submodule R F} (hL : IsCompl L₁ L₂) (hM : IsCompl M₁ M₂) : IsCompl (L₁.prod M₁) (L₂.prod M₂)

Products of complementary submodules are complementary.