refactor(linear_algebra/*): postpone importing material on direct sums (

#3484)

This is just a refactor, to avoid needing to develop material on direct sums before we can even define an algebra.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/algebra/direct_limit.lean

@@ -15,6 +15,7 @@ the free commutative ring (for the ring case) instead of a quotient of the disjo
 so as to make the operations (addition etc.) "computable".
 -/
 import ring_theory.free_comm_ring
+import linear_algebra.direct_sum_module
 
 universes u v w u₁
 

src/algebra/lie_algebra.lean

@@ -6,6 +6,7 @@ Authors: Oliver Nash
 import ring_theory.algebra
 import linear_algebra.linear_action
 import linear_algebra.bilinear_form
+import linear_algebra.direct_sum.finsupp
 import tactic.noncomm_ring
 
 /-!

src/linear_algebra/direct_sum/finsupp.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Johannes Hölzl
+-/
+import linear_algebra.finsupp
+import linear_algebra.direct_sum.tensor_product
+
+/-!
+# Results on direct sums and finitely supported functions.
+
+1. The linear equivalence between finitely supported functions `ι →₀ M` and
+the direct sum of copies of `M` indexed by `ι`.
+
+2. The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).
+-/
+
+universes u v w
+
+noncomputable theory
+open_locale classical
+
+open set linear_map submodule
+variables {R : Type u} {M : Type v} {N : Type w} [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+
+section finsupp_lequiv_direct_sum
+
+variables (R M) (ι : Type*) [decidable_eq ι]
+
+/-- The finitely supported functions ι →₀ M are in linear equivalence with the direct sum of
+copies of M indexed by ι. -/
+def finsupp_lequiv_direct_sum : (ι →₀ M) ≃ₗ[R] direct_sum ι (λ i, M) :=
+linear_equiv.of_linear
+  (finsupp.lsum $ direct_sum.lof R ι (λ _, M))
+  (direct_sum.to_module _ _ _ finsupp.lsingle)
+  (linear_map.ext $ direct_sum.to_module.ext _ $ λ i,
+    linear_map.ext $ λ x, by simp [finsupp.sum_single_index])
+  (linear_map.ext $ λ f, finsupp.ext $ λ i, by simp [finsupp.lsum_apply])
+
+@[simp] theorem finsupp_lequiv_direct_sum_single (i : ι) (m : M) :
+  finsupp_lequiv_direct_sum R M ι (finsupp.single i m) = direct_sum.lof R ι _ i m :=
+finsupp.sum_single_index $ direct_sum.of_zero i
+
+@[simp] theorem finsupp_lequiv_direct_sum_symm_lof (i : ι) (m : M) :
+  (finsupp_lequiv_direct_sum R M ι).symm (direct_sum.lof R ι _ i m) = finsupp.single i m :=
+direct_sum.to_module_lof _ _ _
+
+end finsupp_lequiv_direct_sum
+
+section tensor_product
+
+open_locale tensor_product
+
+/-- The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N). -/
+def finsupp_tensor_finsupp (R M N ι κ : Sort*) [comm_ring R]
+  [add_comm_group M] [module R M] [add_comm_group N] [module R N] :
+  (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] (ι × κ) →₀ (M ⊗[R] N) :=
+linear_equiv.trans
+  (tensor_product.congr (finsupp_lequiv_direct_sum R M ι) (finsupp_lequiv_direct_sum R N κ)) $
+linear_equiv.trans
+  (tensor_product.direct_sum R ι κ (λ _, M) (λ _, N))
+  (finsupp_lequiv_direct_sum R (M ⊗[R] N) (ι × κ)).symm
+
+@[simp] theorem finsupp_tensor_finsupp_single (R M N ι κ : Sort*) [comm_ring R]
+  [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+  (i : ι) (m : M) (k : κ) (n : N) :
+  finsupp_tensor_finsupp R M N ι κ (finsupp.single i m ⊗ₜ finsupp.single k n) =
+  finsupp.single (i, k) (m ⊗ₜ n) :=
+by simp [finsupp_tensor_finsupp]
+
+@[simp] theorem finsupp_tensor_finsupp_symm_single (R M N ι κ : Sort*) [comm_ring R]
+  [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+  (i : ι × κ) (m : M) (n : N) :
+  (finsupp_tensor_finsupp R M N ι κ).symm (finsupp.single i (m ⊗ₜ n)) =
+  (finsupp.single i.1 m ⊗ₜ finsupp.single i.2 n) :=
+prod.cases_on i $ λ i k, (linear_equiv.symm_apply_eq _).2
+  (finsupp_tensor_finsupp_single _ _ _ _ _ _ _ _ _).symm
+
+end tensor_product

src/linear_algebra/direct_sum/tensor_product.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Mario Carneiro
+-/
+import linear_algebra.tensor_product
+import linear_algebra.direct_sum_module
+
+section ring
+
+namespace tensor_product
+
+open_locale tensor_product
+open linear_map
+
+variables (R : Type*) [comm_ring R]
+variables (ι₁ : Type*) (ι₂ : Type*)
+variables [decidable_eq ι₁] [decidable_eq ι₂]
+variables (M₁ : ι₁ → Type*) (M₂ : ι₂ → Type*)
+variables [Π i₁, add_comm_group (M₁ i₁)] [Π i₂, add_comm_group (M₂ i₂)]
+variables [Π i₁, module R (M₁ i₁)] [Π i₂, module R (M₂ i₂)]
+
+/-- The linear equivalence `(⊕ i₁, M₁ i₁) ⊗ (⊕ i₂, M₂ i₂) ≃ (⊕ i₁, ⊕ i₂, M₁ i₁ ⊗ M₂ i₂)`, i.e.
+"tensor product distributes over direct sum". -/
+def direct_sum :
+  direct_sum ι₁ M₁ ⊗[R] direct_sum ι₂ M₂ ≃ₗ[R] direct_sum (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) :=
+begin
+  refine linear_equiv.of_linear
+    (lift $ direct_sum.to_module R _ _ $ λ i₁, flip $ direct_sum.to_module R _ _ $ λ i₂,
+      flip $ curry $ direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))
+    (direct_sum.to_module R _ _ $ λ i, map (direct_sum.lof R _ _ _) (direct_sum.lof R _ _ _))
+    (linear_map.ext $ direct_sum.to_module.ext _ $ λ i, mk_compr₂_inj $
+      linear_map.ext $ λ x₁, linear_map.ext $ λ x₂, _)
+    (mk_compr₂_inj $ linear_map.ext $ direct_sum.to_module.ext _ $ λ i₁, linear_map.ext $ λ x₁,
+      linear_map.ext $ direct_sum.to_module.ext _ $ λ i₂, linear_map.ext $ λ x₂, _),
+  repeat { rw compr₂_apply <|> rw comp_apply <|> rw id_apply <|> rw mk_apply <|>
+    rw direct_sum.to_module_lof <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
+    rw curry_apply },
+  cases i; refl
+end
+
+@[simp] theorem direct_sum_lof_tmul_lof (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
+  direct_sum R ι₁ ι₂ M₁ M₂ (direct_sum.lof R ι₁ M₁ i₁ m₁ ⊗ₜ direct_sum.lof R ι₂ M₂ i₂ m₂) =
+  direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂) :=
+by simp [direct_sum]
+
+end tensor_product
+
+end ring

src/linear_algebra/finsupp.lean

@@ -478,58 +478,3 @@ begin
   have hi : i ∈ s, { rw finset.mem_image, exact ⟨⟨x, hx⟩, finset.mem_univ _, rfl⟩ },
   exact hN i hi (hg _),
 end
-
-section finsupp_lequiv_direct_sum
-
-variables (R M) (ι : Type*) [decidable_eq ι]
-
-/-- The finitely supported functions ι →₀ M are in linear equivalence with the direct sum of
-copies of M indexed by ι. -/
-def finsupp_lequiv_direct_sum : (ι →₀ M) ≃ₗ[R] direct_sum ι (λ i, M) :=
-linear_equiv.of_linear
-  (finsupp.lsum $ direct_sum.lof R ι (λ _, M))
-  (direct_sum.to_module _ _ _ finsupp.lsingle)
-  (linear_map.ext $ direct_sum.to_module.ext _ $ λ i,
-    linear_map.ext $ λ x, by simp [finsupp.sum_single_index])
-  (linear_map.ext $ λ f, finsupp.ext $ λ i, by simp [finsupp.lsum_apply])
-
-@[simp] theorem finsupp_lequiv_direct_sum_single (i : ι) (m : M) :
-  finsupp_lequiv_direct_sum R M ι (finsupp.single i m) = direct_sum.lof R ι _ i m :=
-finsupp.sum_single_index $ direct_sum.of_zero i
-
-@[simp] theorem finsupp_lequiv_direct_sum_symm_lof (i : ι) (m : M) :
-  (finsupp_lequiv_direct_sum R M ι).symm (direct_sum.lof R ι _ i m) = finsupp.single i m :=
-direct_sum.to_module_lof _ _ _
-
-end finsupp_lequiv_direct_sum
-
-section tensor_product
-
-open_locale tensor_product
-
-/-- The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N). -/
-def finsupp_tensor_finsupp (R M N ι κ : Sort*) [comm_ring R]
-  [add_comm_group M] [module R M] [add_comm_group N] [module R N] :
-  (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] (ι × κ) →₀ (M ⊗[R] N) :=
-linear_equiv.trans
-  (tensor_product.congr (finsupp_lequiv_direct_sum R M ι) (finsupp_lequiv_direct_sum R N κ)) $
-linear_equiv.trans
-  (tensor_product.direct_sum R ι κ (λ _, M) (λ _, N))
-  (finsupp_lequiv_direct_sum R (M ⊗[R] N) (ι × κ)).symm
-
-@[simp] theorem finsupp_tensor_finsupp_single (R M N ι κ : Sort*) [comm_ring R]
-  [add_comm_group M] [module R M] [add_comm_group N] [module R N]
-  (i : ι) (m : M) (k : κ) (n : N) :
-  finsupp_tensor_finsupp R M N ι κ (finsupp.single i m ⊗ₜ finsupp.single k n) =
-  finsupp.single (i, k) (m ⊗ₜ n) :=
-by simp [finsupp_tensor_finsupp]
-
-@[simp] theorem finsupp_tensor_finsupp_symm_single (R M N ι κ : Sort*) [comm_ring R]
-  [add_comm_group M] [module R M] [add_comm_group N] [module R N]
-  (i : ι × κ) (m : M) (n : N) :
-  (finsupp_tensor_finsupp R M N ι κ).symm (finsupp.single i (m ⊗ₜ n)) =
-  (finsupp.single i.1 m ⊗ₜ finsupp.single i.2 n) :=
-prod.cases_on i $ λ i k, (linear_equiv.symm_apply_eq _).2
-  (finsupp_tensor_finsupp_single _ _ _ _ _ _ _ _ _).symm
-
-end tensor_product

src/linear_algebra/finsupp_vector_space.lean

@@ -7,6 +7,8 @@ Linear structures on function with finite support `ι →₀ β`.
 -/
 import data.mv_polynomial
 import linear_algebra.dimension
+import linear_algebra.direct_sum.finsupp
+
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 

src/linear_algebra/tensor_product.lean

@@ -5,8 +5,7 @@ Authors: Kenny Lau, Mario Carneiro
 -/
 
 import group_theory.congruence
-import group_theory.free_abelian_group
-import linear_algebra.direct_sum_module
+import linear_algebra.basic
 
 /-!
 # Tensor product of semimodules over commutative semirings.
@@ -607,36 +606,6 @@ instance : add_comm_group (M ⊗[R] N) :=
 lemma neg_tmul (m : M) (n : N) : (-m) ⊗ₜ n = -(m ⊗ₜ[R] n) := (mk R M N).map_neg₂ _ _
 lemma tmul_neg (m : M) (n : N) : m ⊗ₜ (-n) = -(m ⊗ₜ[R] n) := (mk R M N _).map_neg _
 
-variables (R) (ι₁ : Type*) (ι₂ : Type*)
-variables [decidable_eq ι₁] [decidable_eq ι₂]
-variables (M₁ : ι₁ → Type*) (M₂ : ι₂ → Type*)
-variables [Π i₁, add_comm_group (M₁ i₁)] [Π i₂, add_comm_group (M₂ i₂)]
-variables [Π i₁, module R (M₁ i₁)] [Π i₂, module R (M₂ i₂)]
-
-/-- The linear equivalence `(⊕ i₁, M₁ i₁) ⊗ (⊕ i₂, M₂ i₂) ≃ (⊕ i₁, ⊕ i₂, M₁ i₁ ⊗ M₂ i₂)`, i.e.
-"tensor product distributes over direct sum". -/
-def direct_sum : direct_sum ι₁ M₁ ⊗[R] direct_sum ι₂ M₂
-  ≃ₗ[R] direct_sum (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) :=
-begin
-  refine linear_equiv.of_linear
-    (lift $ direct_sum.to_module R _ _ $ λ i₁, flip $ direct_sum.to_module R _ _ $ λ i₂,
-      flip $ curry $ direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))
-    (direct_sum.to_module R _ _ $ λ i, map (direct_sum.lof R _ _ _) (direct_sum.lof R _ _ _))
-    (linear_map.ext $ direct_sum.to_module.ext _ $ λ i, mk_compr₂_inj $
-      linear_map.ext $ λ x₁, linear_map.ext $ λ x₂, _)
-    (mk_compr₂_inj $ linear_map.ext $ direct_sum.to_module.ext _ $ λ i₁, linear_map.ext $ λ x₁,
-      linear_map.ext $ direct_sum.to_module.ext _ $ λ i₂, linear_map.ext $ λ x₂, _);
-  repeat { rw compr₂_apply <|> rw comp_apply <|> rw id_apply <|> rw mk_apply <|>
-    rw direct_sum.to_module_lof <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
-    rw curry_apply },
-  cases i; refl
-end
-
-@[simp] theorem direct_sum_lof_tmul_lof (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
-  direct_sum R ι₁ ι₂ M₁ M₂ (direct_sum.lof R ι₁ M₁ i₁ m₁ ⊗ₜ direct_sum.lof R ι₂ M₂ i₂ m₂) =
-  direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂) :=
-by simp [direct_sum]
-
 end tensor_product
 
 end ring