feat(algebra/module/submodule_lattice, linear_algebra/projection): tw…

…o lemmas about `is_compl` (#10709)

src/algebra/module/submodule_lattice.lean

@@ -226,6 +226,19 @@ lemma mem_Sup_of_mem {S : set (submodule R M)} {s : submodule R M}
   (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ Sup S :=
 show s ≤ Sup S, from le_Sup hs
 
+theorem disjoint_def {p p' : submodule R M} :
+  disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0:M) :=
+show (∀ x, x ∈ p ∧ x ∈ p' → x ∈ ({0} : set M)) ↔ _, by simp
+
+theorem disjoint_def' {p p' : submodule R M} :
+  disjoint p p' ↔ ∀ (x ∈ p) (y ∈ p'), x = y → x = (0:M) :=
+disjoint_def.trans ⟨λ h x hx y hy hxy, h x hx $ hxy.symm ▸ hy,
+  λ h x hx hx', h _ hx x hx' rfl⟩
+
+lemma eq_zero_of_coe_mem_of_disjoint (hpq : disjoint p q) {a : p} (ha : (a : M) ∈ q) :
+  a = 0 :=
+by exact_mod_cast disjoint_def.mp hpq a (coe_mem a) ha
+
 end submodule
 
 section nat_submodule

src/linear_algebra/basic.lean

@@ -531,15 +531,6 @@ by haveI := module.subsingleton R M; apply_instance
 
 instance [nontrivial M] : nontrivial (submodule R M) := (nontrivial_iff R).mpr ‹_›
 
-theorem disjoint_def {p p' : submodule R M} :
-  disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0:M) :=
-show (∀ x, x ∈ p ∧ x ∈ p' → x ∈ ({0} : set M)) ↔ _, by simp
-
-theorem disjoint_def' {p p' : submodule R M} :
-  disjoint p p' ↔ ∀ (x ∈ p) (y ∈ p'), x = y → x = (0:M) :=
-disjoint_def.trans ⟨λ h x hx y hy hxy, h x hx $ hxy.symm ▸ hy,
-  λ h x hx hx', h _ hx x hx' rfl⟩
-
 theorem mem_right_iff_eq_zero_of_disjoint {p p' : submodule R M} (h : disjoint p p') {x : p} :
   (x:M) ∈ p' ↔ x = 0 :=
 ⟨λ hx, coe_eq_zero.1 $ disjoint_def.1 h x x.2 hx, λ h, h.symm ▸ p'.zero_mem⟩

src/linear_algebra/prod.lean

@@ -444,6 +444,15 @@ lemma fst_inf_snd : submodule.fst R M M₂ ⊓ submodule.snd R M M₂ = ⊥ := b
 end submodule
 
 namespace linear_equiv
+
+/-- Product of modules is commutative up to linear isomorphism. -/
+@[simps apply]
+def prod_comm (R M N : Type*) [semiring R] [add_comm_monoid M] [add_comm_monoid N]
+  [module R M] [module R N] : (M × N) ≃ₗ[R] (N × M) :=
+{ to_fun := prod.swap,
+  map_smul' := λ r ⟨m, n⟩, rfl,
+  ..add_equiv.prod_comm }
+
 section
 
 variables [semiring R]

src/linear_algebra/projection.lean

@@ -128,6 +128,12 @@ begin
     mem_left_iff_eq_zero_of_disjoint h.disjoint]
 end
 
+@[simp]
+lemma prod_comm_trans_prod_equiv_of_is_compl (h : is_compl p q) :
+  linear_equiv.prod_comm R q p ≪≫ₗ prod_equiv_of_is_compl p q h =
+    prod_equiv_of_is_compl q p h.symm :=
+linear_equiv.ext $ λ _, add_comm _ _
+
 /-- Projection to a submodule along its complement. -/
 def linear_proj_of_is_compl (h : is_compl p q) :
   E →ₗ[R] p :=
@@ -178,6 +184,14 @@ lemma exists_unique_add_of_is_compl (hc : is_compl p q) (x : E) :
 let ⟨u, hu₁, hu₂⟩ := exists_unique_add_of_is_compl_prod hc x in
   ⟨u.1, u.2, hu₁, λ r s hrs, prod.eq_iff_fst_eq_snd_eq.1 (hu₂ ⟨r, s⟩ hrs)⟩
 
+lemma linear_proj_add_linear_proj_of_is_compl_eq_self (hpq : is_compl p q) (x : E) :
+  (p.linear_proj_of_is_compl q hpq x + q.linear_proj_of_is_compl p hpq.symm x : E) = x :=
+begin
+  dunfold linear_proj_of_is_compl,
+  rw ←prod_comm_trans_prod_equiv_of_is_compl _ _ hpq,
+  exact (prod_equiv_of_is_compl _ _ hpq).apply_symm_apply x,
+end
+
 end submodule
 
 namespace linear_map