feat(linear_algebra): the direct sum of a submodule quotient is the q…

…uotient of the direct sum (#17069)

This defines the linear equivalence `submodule.quotient_pi` which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm.

Co-Authored-By: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/algebra/module/equiv.lean

@@ -264,6 +264,9 @@ rfl
 include σ₃₁
 @[simp] theorem trans_apply (c : M₁) :
   (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃) c = e₂₃ (e₁₂ c) := rfl
+
+theorem coe_trans :
+  (e₁₂.trans e₂₃ : M₁ →ₛₗ[σ₁₃] M₃) = (e₂₃ : M₂ →ₛₗ[σ₂₃] M₃).comp (e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) := rfl
 omit σ₃₁
 
 include σ'

src/analysis/inner_product_space/two_dim.lean

@@ -179,7 +179,11 @@ let to_dual : E ≃ₗ[ℝ] (E →ₗ[ℝ] ℝ) :=
 
 @[simp] lemma inner_right_angle_rotation_aux₁_left (x y : E) :
   ⟪o.right_angle_rotation_aux₁ x, y⟫ = ω x y :=
-by simp [right_angle_rotation_aux₁]
+by simp only [right_angle_rotation_aux₁, linear_equiv.trans_symm, linear_equiv.coe_trans,
+              linear_equiv.coe_coe, inner_product_space.to_dual_symm_apply, eq_self_iff_true,
+              linear_map.coe_to_continuous_linear_map', linear_isometry_equiv.coe_to_linear_equiv,
+              linear_map.comp_apply, linear_equiv.symm_symm,
+              linear_isometry_equiv.to_linear_equiv_symm]
 
 @[simp] lemma inner_right_angle_rotation_aux₁_right (x y : E) :
   ⟪x, o.right_angle_rotation_aux₁ y⟫ = - ω x y :=

src/linear_algebra/basic.lean

@@ -1982,7 +1982,18 @@ lemma comap_equiv_eq_map_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : submodule R
   K.comap (e : M →ₛₗ[τ₁₂] M₂) = K.map (e.symm : M₂ →ₛₗ[τ₂₁] M) :=
 (map_equiv_eq_comap_symm e.symm K).symm
 
+variables {p}
 include τ₂₁
+lemma map_symm_eq_iff (e : M ≃ₛₗ[τ₁₂] M₂) {K : submodule R₂ M₂} :
+  K.map e.symm = p ↔ p.map e = K :=
+begin
+  split; rintro rfl,
+  { calc map e (map e.symm K) = comap e.symm (map e.symm K) : map_equiv_eq_comap_symm _ _
+    ... = K : comap_map_eq_of_injective e.symm.injective _ },
+  { calc map e.symm (map e p) = comap e (map e p) : (comap_equiv_eq_map_symm _ _).symm
+    ... = p : comap_map_eq_of_injective e.injective _ },
+end
+
 lemma order_iso_map_comap_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : submodule R M) :
   order_iso_map_comap e p = comap e.symm p :=
 p.map_equiv_eq_comap_symm _

src/linear_algebra/pi.lean

@@ -120,6 +120,11 @@ families of functions on these modules. See note [bundled maps over different ri
       rw finset.univ_sum_single
     end }
 
+@[simp] lemma lsum_single {ι R : Type*} [fintype ι] [decidable_eq ι] [comm_ring R]
+  {M : ι → Type*} [∀ i, add_comm_group (M i)] [∀ i, module R (M i)] :
+  linear_map.lsum R M R linear_map.single = linear_map.id :=
+linear_map.ext (λ x, by simp [finset.univ_sum_single])
+
 variables {R φ}
 
 section ext
@@ -248,6 +253,17 @@ begin
     exact sum_mem_supr (λ i, mem_map_of_mem (hx i trivial)) }
 end
 
+lemma le_comap_single_pi [decidable_eq ι] (p : Π i, submodule R (φ i)) {i} :
+  p i ≤ submodule.comap (linear_map.single i : φ i →ₗ[R] _) (submodule.pi set.univ p) :=
+begin
+  intros x hx,
+  rw [submodule.mem_comap, submodule.mem_pi],
+  rintros j -,
+  by_cases h : j = i,
+  { rwa [h, linear_map.coe_single, pi.single_eq_same] },
+  { rw [linear_map.coe_single, pi.single_eq_of_ne h], exact (p j).zero_mem }
+end
+
 end submodule
 
 namespace linear_equiv

src/linear_algebra/quotient.lean

@@ -385,6 +385,43 @@ begin
   exact inf_le_right,
 end
 
+/-- If `P` is a submodule of `M` and `Q` a submodule of `N`,
+and `f : M ≃ₗ N` maps `P` to `Q`, then `M ⧸ P` is equivalent to `N ⧸ Q`. -/
+@[simps] def quotient.equiv {N : Type*} [add_comm_group N] [module R N]
+  (P : submodule R M) (Q : submodule R N)
+  (f : M ≃ₗ[R] N) (hf : P.map f = Q) : (M ⧸ P) ≃ₗ[R] N ⧸ Q :=
+{ to_fun := P.mapq Q (f : M →ₗ[R] N) (λ x hx, hf ▸ submodule.mem_map_of_mem hx),
+  inv_fun := Q.mapq P (f.symm : N →ₗ[R] M) (λ x hx, begin
+    rw [← hf, submodule.mem_map] at hx,
+    obtain ⟨y, hy, rfl⟩ := hx,
+    simpa
+  end),
+  left_inv := λ x, quotient.induction_on' x (by simp),
+  right_inv := λ x, quotient.induction_on' x (by simp),
+  .. P.mapq Q (f : M →ₗ[R] N) (λ x hx, hf ▸ submodule.mem_map_of_mem hx) }
+
+@[simp] lemma quotient.equiv_symm {R M N : Type*} [comm_ring R]
+  [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+  (P : submodule R M) (Q : submodule R N)
+  (f : M ≃ₗ[R] N) (hf : P.map f = Q) :
+  (quotient.equiv P Q f hf).symm =
+    quotient.equiv Q P f.symm ((submodule.map_symm_eq_iff f).mpr hf) :=
+rfl
+
+@[simp] lemma quotient.equiv_trans {N O : Type*} [add_comm_group N] [module R N]
+  [add_comm_group O] [module R O]
+  (P : submodule R M) (Q : submodule R N) (S : submodule R O)
+  (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] O)
+  (he : P.map e = Q) (hf : Q.map f = S) (hef : P.map (e.trans f) = S) :
+  quotient.equiv P S (e.trans f) hef = (quotient.equiv P Q e he).trans (quotient.equiv Q S f hf) :=
+begin
+  ext,
+  -- `simp` can deal with `hef` depending on `e` and `f`
+  simp only [quotient.equiv_apply, linear_equiv.trans_apply, linear_equiv.coe_trans],
+  -- `rw` can deal with `mapq_comp` needing extra hypotheses coming from the RHS
+  rw [mapq_comp, linear_map.comp_apply]
+end
+
 end submodule
 
 open submodule
@@ -452,6 +489,11 @@ lemma quot_equiv_of_eq_mk (h : p = p') (x : M) :
   submodule.quot_equiv_of_eq p p' h (submodule.quotient.mk x) = submodule.quotient.mk x :=
 rfl
 
+@[simp] lemma quotient.equiv_refl (P : submodule R M) (Q : submodule R M)
+  (hf : P.map (linear_equiv.refl R M : M →ₗ[R] M) = Q) :
+  quotient.equiv P Q (linear_equiv.refl R M) hf = quot_equiv_of_eq _ _ (by simpa using hf) :=
+rfl
+
 end submodule
 
 end ring

src/linear_algebra/quotient_pi.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2022 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Alex J. Best
+-/
+import linear_algebra.pi
+import linear_algebra.quotient
+
+/-!
+# Submodule quotients and direct sums
+
+This file contains some results on the quotient of a module by a direct sum of submodules,
+and the direct sum of quotients of modules by submodules.
+
+# Main definitions
+
+ * `submodule.pi_quotient_lift`: create a map out of the direct sum of quotients
+ * `submodule.quotient_pi_lift`: create a map out of the quotient of a direct sum
+ * `submodule.quotient_pi`: the quotient of a direct sum is the direct sum of quotients.
+
+-/
+
+namespace submodule
+
+open linear_map
+
+variables {ι R : Type*} [comm_ring R]
+variables {Ms : ι → Type*} [∀ i, add_comm_group (Ms i)] [∀ i, module R (Ms i)]
+variables {N : Type*} [add_comm_group N] [module R N]
+variables {Ns : ι → Type*} [∀ i, add_comm_group (Ns i)] [∀ i, module R (Ns i)]
+
+/-- Lift a family of maps to the direct sum of quotients. -/
+def pi_quotient_lift [fintype ι] [decidable_eq ι]
+  (p : ∀ i, submodule R (Ms i)) (q : submodule R N)
+  (f : Π i, Ms i →ₗ[R] N) (hf : ∀ i, p i ≤ q.comap (f i)) :
+  (Π i, (Ms i ⧸ p i)) →ₗ[R] (N ⧸ q) :=
+lsum R (λ i, (Ms i ⧸ (p i))) R (λ i, (p i).mapq q (f i) (hf i))
+
+@[simp] lemma pi_quotient_lift_mk [fintype ι] [decidable_eq ι]
+  (p : ∀ i, submodule R (Ms i)) (q : submodule R N)
+  (f : Π i, Ms i →ₗ[R] N) (hf : ∀ i, p i ≤ q.comap (f i)) (x : Π i, Ms i) :
+  pi_quotient_lift p q f hf (λ i, quotient.mk (x i)) =
+    quotient.mk (lsum _ _ R f x) :=
+by rw [pi_quotient_lift, lsum_apply, sum_apply, ← mkq_apply, lsum_apply, sum_apply, _root_.map_sum];
+   simp only [coe_proj, mapq_apply, mkq_apply, comp_apply]
+
+@[simp] lemma pi_quotient_lift_single [fintype ι] [decidable_eq ι]
+  (p : ∀ i, submodule R (Ms i)) (q : submodule R N)
+  (f : Π i, Ms i →ₗ[R] N) (hf : ∀ i, p i ≤ q.comap (f i)) (i) (x : Ms i ⧸ p i) :
+  pi_quotient_lift p q f hf (pi.single i x) =
+    mapq _ _ (f i) (hf i) x :=
+begin
+  simp_rw [pi_quotient_lift, lsum_apply, sum_apply,
+           comp_apply, proj_apply],
+  rw finset.sum_eq_single i,
+  { rw pi.single_eq_same },
+  { rintros j - hj, rw [pi.single_eq_of_ne hj, _root_.map_zero] },
+  { intros, have := finset.mem_univ i, contradiction },
+end
+
+/-- Lift a family of maps to a quotient of direct sums. -/
+def quotient_pi_lift
+  (p : ∀ i, submodule R (Ms i))
+  (f : Π i, Ms i →ₗ[R] Ns i) (hf : ∀ i, p i ≤ ker (f i)) :
+  ((Π i, Ms i) ⧸ pi set.univ p) →ₗ[R] Π i, Ns i :=
+(pi set.univ p).liftq (linear_map.pi (λ i, (f i).comp (proj i))) $
+λ x hx, mem_ker.mpr $
+by { ext i, simpa using hf i (mem_pi.mp hx i (set.mem_univ i)) }
+
+@[simp] lemma quotient_pi_lift_mk
+  (p : ∀ i, submodule R (Ms i))
+  (f : Π i, Ms i →ₗ[R] Ns i) (hf : ∀ i, p i ≤ ker (f i)) (x : Π i, Ms i) :
+  quotient_pi_lift p f hf (quotient.mk x) = λ i, f i (x i) :=
+rfl
+
+/-- The quotient of a direct sum is the direct sum of quotients. -/
+@[simps] def quotient_pi [fintype ι] [decidable_eq ι]
+  (p : ∀ i, submodule R (Ms i)) :
+  ((Π i, Ms i) ⧸ pi set.univ p) ≃ₗ[R] Π i, Ms i ⧸ p i :=
+{ to_fun := quotient_pi_lift p (λ i, (p i).mkq) (λ i, by simp),
+  inv_fun := pi_quotient_lift p (pi set.univ p)
+    single (λ i, le_comap_single_pi p),
+  left_inv := λ x, quotient.induction_on' x (λ x',
+    by simp_rw [quotient.mk'_eq_mk, quotient_pi_lift_mk, mkq_apply,
+                pi_quotient_lift_mk, lsum_single, id_apply]),
+  right_inv := begin
+    rw [function.right_inverse_iff_comp, ← coe_comp, ← @id_coe R],
+    refine congr_arg _ (pi_ext (λ i x, quotient.induction_on' x (λ x', funext $ λ j, _))),
+    rw [comp_apply, pi_quotient_lift_single, quotient.mk'_eq_mk, mapq_apply,
+        quotient_pi_lift_mk, id_apply],
+    by_cases hij : i = j; simp only [mkq_apply, coe_single],
+    { subst hij, simp only [pi.single_eq_same] },
+    { simp only [pi.single_eq_of_ne (ne.symm hij), quotient.mk_zero] },
+  end,
+  .. quotient_pi_lift p (λ i, (p i).mkq) (λ i, by simp) }
+
+end submodule