feat(algebra/direct_sum/module): link direct_sum.submodule_is_internal to is_compl (#12671)

This is then used to show the even and odd components of a clifford algebra are complementary.

Author: eric-wieser

src/algebra/direct_sum/module.lean

@@ -274,6 +274,14 @@ lemma submodule_is_internal.collected_basis_mem
   h.collected_basis v a ∈ A a.1 :=
 by simp
 
+/-- When indexed by only two distinct elements, `direct_sum.submodule_is_internal` implies
+the two submodules are complementary. Over a `ring R`, this is true as an iff, as
+`direct_sum.submodule_is_internal_iff_is_compl`. --/
+lemma submodule_is_internal.is_compl {A : ι → submodule R M} {i j : ι} (hij : i ≠ j)
+  (h : (set.univ : set ι) = {i, j}) (hi : submodule_is_internal A) : is_compl (A i) (A j) :=
+⟨hi.independent.disjoint hij, eq.le $ hi.supr_eq_top.symm.trans $
+  by rw [←Sup_pair, supr, ←set.image_univ, h, set.image_insert_eq, set.image_singleton]⟩
+
 end semiring
 
 section ring
@@ -301,6 +309,19 @@ lemma submodule_is_internal_iff_independent_and_supr_eq_top (A : ι → submodul
 ⟨λ i, ⟨i.independent, i.supr_eq_top⟩,
  and.rec submodule_is_internal_of_independent_of_supr_eq_top⟩
 
+/-- If a collection of submodules has just two indices, `i` and `j`, then
+`direct_sum.submodule_is_internal` is equivalent to `is_compl`. -/
+lemma submodule_is_internal_iff_is_compl (A : ι → submodule R M) {i j : ι} (hij : i ≠ j)
+  (h : (set.univ : set ι) = {i, j}) :
+  submodule_is_internal A ↔ is_compl (A i) (A j) :=
+begin
+  have : ∀ k, k = i ∨ k = j := λ k, by simpa using set.ext_iff.mp h k,
+  rw [submodule_is_internal_iff_independent_and_supr_eq_top,
+    supr, ←set.image_univ, h, set.image_insert_eq, set.image_singleton, Sup_pair,
+    complete_lattice.independent_pair hij this],
+  exact ⟨λ ⟨hd, ht⟩, ⟨hd, ht.ge⟩, λ ⟨hd, ht⟩, ⟨hd, eq_top_iff.mpr ht⟩⟩,
+end
+
 /-! Now copy the lemmas for subgroup and submonoids. -/
 
 lemma add_submonoid_is_internal.independent {M : Type*} [add_comm_monoid M]

src/linear_algebra/clifford_algebra/grading.lean

@@ -125,6 +125,12 @@ begin
     ... = (⨆ (i : ℕ), (ι Q).range ^ i) : supr_congr (λ i, i.2) (λ i, ⟨⟨_, i, rfl⟩, rfl⟩) (λ _, rfl),
 end
 
+lemma even_odd_is_compl : is_compl (even_odd Q 0) (even_odd Q 1) :=
+(graded_algebra.is_internal (even_odd Q)).is_compl zero_ne_one $ begin
+  have : (finset.univ : finset (zmod 2)) = {0, 1} := rfl,
+  simpa using congr_arg (coe : finset (zmod 2) → set (zmod 2)) this,
+end
+
 /-- To show a property is true on the even or odd part, it suffices to show it is true on the
 scalars or vectors (respectively), closed under addition, and under left-multiplication by a pair
 of vectors. -/