refactor(linear_algebra/direct_sum_module): move to algebra/direct_sum

src/algebra/direct_sum.lean

@@ -0,0 +1,164 @@
+/-
+Copyright (c) 2019 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+
+Direct sum of abelian groups, indexed by a discrete type.
+-/
+
+import data.dfinsupp
+
+universes u v w u₁
+
+variables (ι : Type v) [decidable_eq ι] (β : ι → Type w) [Π i, add_comm_group (β i)]
+
+def direct_sum : Type* := Π₀ i, β i
+
+namespace direct_sum
+
+variables {ι β}
+
+instance : add_comm_group (direct_sum ι β) :=
+dfinsupp.add_comm_group
+
+variables β
+def mk : Π s : finset ι, (Π i : (↑s : set ι), β i.1) → direct_sum ι β :=
+dfinsupp.mk
+
+def of : Π i : ι, β i → direct_sum ι β :=
+dfinsupp.single
+variables {β}
+
+instance mk.is_add_group_hom (s : finset ι) : is_add_group_hom (mk β s) :=
+⟨λ _ _, dfinsupp.mk_add⟩
+
+@[simp] lemma mk_zero (s : finset ι) : mk β s 0 = 0 :=
+is_add_group_hom.zero _
+
+@[simp] lemma mk_add (s : finset ι) (x y) : mk β s (x + y) = mk β s x + mk β s y :=
+is_add_group_hom.add _ x y
+
+@[simp] lemma mk_neg (s : finset ι) (x) : mk β s (-x) = -mk β s x :=
+is_add_group_hom.neg _ x
+
+@[simp] lemma mk_sub (s : finset ι) (x y) : mk β s (x - y) = mk β s x - mk β s y :=
+is_add_group_hom.sub _ x y
+
+instance of.is_add_group_hom (i : ι) : is_add_group_hom (of β i) :=
+⟨λ _ _, dfinsupp.single_add⟩
+
+@[simp] lemma of_zero (i : ι) : of β i 0 = 0 :=
+is_add_group_hom.zero _
+
+@[simp] lemma of_add (i : ι) (x y) : of β i (x + y) = of β i x + of β i y :=
+is_add_group_hom.add _ x y
+
+@[simp] lemma of_neg (i : ι) (x) : of β i (-x) = -of β i x :=
+is_add_group_hom.neg _ x
+
+@[simp] lemma of_sub (i : ι) (x y) : of β i (x - y) = of β i x - of β i y :=
+is_add_group_hom.sub _ x y
+
+theorem mk_inj (s : finset ι) : function.injective (mk β s) :=
+dfinsupp.mk_inj s
+
+theorem of_inj (i : ι) : function.injective (of β i) :=
+λ x y H, congr_fun (mk_inj _ H) ⟨i, by simp [finset.to_set]⟩
+
+@[elab_as_eliminator]
+protected theorem induction_on {C : direct_sum ι β → Prop}
+  (x : direct_sum ι β) (H_zero : C 0)
+  (H_basic : ∀ (i : ι) (x : β i), C (of β i x))
+  (H_plus : ∀ x y, C x → C y → C (x + y)) : C x :=
+begin
+  apply dfinsupp.induction x H_zero,
+  intros i b f h1 h2 ih,
+  solve_by_elim
+end
+
+variables {γ : Type u₁} [add_comm_group γ]
+variables (φ : Π i, β i → γ) [Π i, is_add_group_hom (φ i)]
+
+variables (φ)
+def to_group (f : direct_sum ι β) : γ :=
+quotient.lift_on f (λ x, x.2.to_finset.sum $ λ i, φ i (x.1 i)) $ λ x y H,
+begin
+  have H1 : x.2.to_finset ∩ y.2.to_finset ⊆ x.2.to_finset, from finset.inter_subset_left _ _,
+  have H2 : x.2.to_finset ∩ y.2.to_finset ⊆ y.2.to_finset, from finset.inter_subset_right _ _,
+  refine (finset.sum_subset H1 _).symm.trans ((finset.sum_congr rfl _).trans (finset.sum_subset H2 _)),
+  { intros i H1 H2, rw finset.mem_inter at H2, rw H i,
+    simp only [multiset.mem_to_finset] at H1 H2,
+    rw [(y.3 i).resolve_left (mt (and.intro H1) H2), is_add_group_hom.zero (φ i)] },
+  { intros i H1, rw H i },
+  { intros i H1 H2, rw finset.mem_inter at H2, rw ← H i,
+    simp only [multiset.mem_to_finset] at H1 H2,
+    rw [(x.3 i).resolve_left (mt (λ H3, and.intro H3 H1) H2), is_add_group_hom.zero (φ i)] }
+end
+variables {φ}
+
+instance to_group.is_add_group_hom : is_add_group_hom (to_group φ) :=
+begin
+  constructor, intros f g,
+  refine quotient.induction_on f (λ x, _),
+  refine quotient.induction_on g (λ y, _),
+  change finset.sum _ _ = finset.sum _ _ + finset.sum _ _,
+  simp only, conv { to_lhs, congr, skip, funext, rw is_add_group_hom.add (φ i) },
+  simp only [finset.sum_add_distrib],
+  congr' 1,
+  { refine (finset.sum_subset _ _).symm,
+    { intro i, simp only [multiset.mem_to_finset, multiset.mem_add], exact or.inl },
+    { intros i H1 H2, simp only [multiset.mem_to_finset, multiset.mem_add] at H2,
+      rw [(x.3 i).resolve_left H2, is_add_group_hom.zero (φ i)] } },
+  { refine (finset.sum_subset _ _).symm,
+    { intro i, simp only [multiset.mem_to_finset, multiset.mem_add], exact or.inr },
+    { intros i H1 H2, simp only [multiset.mem_to_finset, multiset.mem_add] at H2,
+      rw [(y.3 i).resolve_left H2, is_add_group_hom.zero (φ i)] } }
+end
+
+variables (φ)
+@[simp] lemma to_group_zero : to_group φ 0 = 0 :=
+is_add_group_hom.zero _
+
+@[simp] lemma to_group_add (x y) : to_group φ (x + y) = to_group φ x + to_group φ y :=
+is_add_group_hom.add _ x y
+
+@[simp] lemma to_group_neg (x) : to_group φ (-x) = -to_group φ x :=
+is_add_group_hom.neg _ x
+
+@[simp] lemma to_group_sub (x y) : to_group φ (x - y) = to_group φ x - to_group φ y :=
+is_add_group_hom.sub _ x y
+
+@[simp] lemma to_group_of (i) (x : β i) : to_group φ (of β i x) = φ i x :=
+(add_zero _).trans $ congr_arg (φ i) $ show (if H : i ∈ finset.singleton i then x else 0) = x,
+from dif_pos $ finset.mem_singleton_self i
+
+variables (ψ : direct_sum ι β → γ) [is_add_group_hom ψ]
+
+theorem to_group.unique (f : direct_sum ι β) : ψ f = to_group (λ i, ψ ∘ of β i) f :=
+direct_sum.induction_on f
+  (by rw [is_add_group_hom.zero ψ, is_add_group_hom.zero (to_group (λ i, ψ ∘ of β i))])
+  (λ i x, by rw [to_group_of])
+  (λ x y ihx ihy, by rw [is_add_group_hom.add ψ, is_add_group_hom.add (to_group (λ i, ψ ∘ of β i)), ihx, ihy])
+
+variables (β)
+def set_to_set (S T : set ι) (H : S ⊆ T) :
+  direct_sum S (β ∘ subtype.val) → direct_sum T (β ∘ subtype.val) :=
+to_group $ λ i, of (β ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
+variables {β}
+
+instance (S T : set ι) (H : S ⊆ T) : is_add_group_hom (set_to_set β S T H) :=
+to_group.is_add_group_hom
+
+protected def id (M : Type v) [add_comm_group M] : direct_sum punit (λ _, M) ≃ M :=
+{ to_fun := direct_sum.to_group (λ _, id),
+  inv_fun := of (λ _, M) punit.star,
+  left_inv := λ x, direct_sum.induction_on x
+    (by rw [to_group_zero, of_zero])
+    (λ ⟨⟩ x, by rw [to_group_of]; refl)
+    (λ x y ihx ihy, by rw [to_group_add, of_add, ihx, ihy]),
+  right_inv := λ x, to_group_of _ _ _ }
+
+instance : has_coe_to_fun (direct_sum ι β) :=
+dfinsupp.has_coe_to_fun
+
+end direct_sum

src/linear_algebra/direct_sum_module.lean

@@ -6,9 +6,8 @@ Authors: Kenny Lau
 Direct sum of modules over commutative rings, indexed by a discrete type.
 -/
 
+import algebra.direct_sum
 import linear_algebra.basic
-import algebra.pi_instances
-import data.dfinsupp
 
 universes u v w u₁
 
@@ -17,131 +16,60 @@ variables (ι : Type v) [decidable_eq ι] (β : ι → Type w)
 variables [Π i, add_comm_group (β i)] [Π i, module R (β i)]
 include R
 
-def direct_sum : Type* := Π₀ i, β i
-
 namespace direct_sum
 
 variables {R ι β}
---local attribute [instance] dfinsupp.to_has_scalar'
-instance direct_sum.add_comm_group : add_comm_group (direct_sum R ι β) :=
-dfinsupp.add_comm_group
-
-instance direct_sum.module : module R (direct_sum R ι β) :=
-dfinsupp.to_module
-
-variable β
-def mk (s : finset ι) : (Π i : (↑s : set ι), β i.1) →ₗ direct_sum R ι β :=
-dfinsupp.lmk β s
-
-def of (i : ι) : β i →ₗ direct_sum R ι β :=
-dfinsupp.lsingle β i
-variable {β}
-
-theorem mk_inj (s : finset ι) : function.injective ⇑(mk β s) :=
-dfinsupp.mk_inj s
-
-theorem of_inj (i : ι) : function.injective ⇑(of β i) :=
-λ x y H, congr_fun (mk_inj _ H) ⟨i, by simp [finset.to_set]⟩
-
-@[elab_as_eliminator]
-protected theorem induction_on {C : direct_sum R ι β → Prop}
-  (x : direct_sum R ι β) (H_zero : C 0)
-  (H_basic : ∀ (i : ι) (x : β i), C ((of β i : β i →ₗ direct_sum R ι β) x))
-  (H_plus : ∀ x y, C x → C y → C (x + y)) : C x :=
-begin
-  apply dfinsupp.induction x H_zero,
-  intros i b f h1 h2 ih,
-  solve_by_elim
-end
+
+instance : module R (direct_sum ι β) := dfinsupp.to_module
+
+variables ι β
+def lmk : Π s : finset ι, (Π i : (↑s : set ι), β i.1) →ₗ direct_sum ι β :=
+dfinsupp.lmk β
+
+def lof : Π i : ι, β i →ₗ direct_sum ι β :=
+dfinsupp.lsingle β
+variables {ι β}
+
+theorem mk_smul (s : finset ι) (c x) : mk β s (c • x) = c • mk β s x :=
+(lmk ι β s).map_smul c x
+
+theorem of_smul (i : ι) (c x) : of β i (c • x) = c • of β i x :=
+(lof ι β i).map_smul c x
 
 variables {γ : Type u₁} [add_comm_group γ] [module R γ]
 variables (φ : Π i, β i →ₗ γ)
 
-def to_module_aux (f : direct_sum R ι β) : γ :=
-quotient.lift_on f (λ x, x.2.to_finset.sum $ λ i, φ i (x.1 i)) $ λ x y H,
-begin
-  have H1 : x.2.to_finset ∩ y.2.to_finset ⊆ x.2.to_finset, from finset.inter_subset_left _ _,
-  have H2 : x.2.to_finset ∩ y.2.to_finset ⊆ y.2.to_finset, from finset.inter_subset_right _ _,
-  refine (finset.sum_subset H1 _).symm.trans ((finset.sum_congr rfl _).trans (finset.sum_subset H2 _)),
-  { intros i H1 H2, rw finset.mem_inter at H2, rw H i,
-    simp only [multiset.mem_to_finset] at H1 H2,
-    rw [(y.3 i).resolve_left (mt (and.intro H1) H2), (φ i).map_zero] },
-  { intros i H1, rw H i },
-  { intros i H1 H2, rw finset.mem_inter at H2, rw ← H i,
-    simp only [multiset.mem_to_finset] at H1 H2,
-    rw [(x.3 i).resolve_left (mt (λ H3, and.intro H3 H1) H2), (φ i).map_zero] }
-end
-
-variables {φ}
-
-theorem to_module_aux.add (f g) :
-  to_module_aux φ (f + g) = to_module_aux φ f + to_module_aux φ g :=
-begin
-  refine quotient.induction_on f (λ x, _),
-  refine quotient.induction_on g (λ y, _),
-  change finset.sum _ _ = finset.sum _ _ + finset.sum _ _,
-  simp only [(φ _).map_add, finset.sum_add_distrib],
-  congr' 1,
-  { refine (finset.sum_subset _ _).symm,
-    { intro i, simp only [multiset.mem_to_finset, multiset.mem_add], exact or.inl },
-    { intros i H1 H2, simp only [multiset.mem_to_finset, multiset.mem_add] at H2,
-      rw [(x.3 i).resolve_left H2, (φ i).map_zero] } },
-  { refine (finset.sum_subset _ _).symm,
-    { intro i, simp only [multiset.mem_to_finset, multiset.mem_add], exact or.inr },
-    { intros i H1 H2, simp only [multiset.mem_to_finset, multiset.mem_add] at H2,
-      rw [(y.3 i).resolve_left H2, (φ i).map_zero] } }
-end
-
-theorem to_module_aux.smul (c f) :
-  to_module_aux φ (c • f) = c • to_module_aux φ f :=
-begin
-  refine quotient.induction_on f (λ x, _),
-  refine eq.trans (finset.sum_congr rfl _) finset.smul_sum.symm,
-  { intros i h1, dsimp at *, simp [h1, (φ i).map_smul] }
-end
-
-variable (φ)
-def to_module : direct_sum R ι β →ₗ γ :=
-⟨to_module_aux φ, to_module_aux.add, to_module_aux.smul⟩
-variable {φ}
-
-lemma to_module_apply (x) :
-  (to_module φ : direct_sum R ι (λ (i : ι), β i) →ₗ γ) x = to_module_aux φ x := rfl
-
-@[simp] lemma to_module.of (i) (x : β i) :
-  (to_module φ : direct_sum R ι (λ (i : ι), β i) →ₗ γ) ((of β i : β i →ₗ direct_sum R ι β) x) = φ i x :=
-by dsimp [to_module_apply, to_module_aux, of, dfinsupp.single, dfinsupp.mk, to_module_aux]; simp
-
-variables {ψ : direct_sum R ι β →ₗ γ}
-variables (H1 : ∀ (i : ι) (x : β i),
-  ψ ((of β i : β i →ₗ direct_sum R ι β) x)
-  = (to_module φ : direct_sum R ι (λ (i : ι), β i) →ₗ γ) ((of β i : β i →ₗ direct_sum R ι β) x))
-
-theorem to_module.unique (f : direct_sum R ι β) :
-  ψ f = (to_module φ : direct_sum R ι (λ (i : ι), β i) →ₗ γ) f :=
-direct_sum.induction_on f
-  (ψ.map_zero.trans (to_module _).map_zero.symm) H1 $ λ f g ihf ihg,
-by rw [ψ.map_add, (to_module _).map_add, ihf, ihg]
-
-variables {ψ' : direct_sum R ι β →ₗ γ}
-variables (H2 : ∀ i, ψ.comp (of β i) = ψ'.comp (of β i))
-
-theorem to_module.ext (f : direct_sum R ι β) : ψ f = ψ' f :=
-direct_sum.induction_on f (ψ.map_zero.trans ψ'.map_zero.symm)
-  (λ i, linear_map.ext_iff.1 (H2 i)) $ λ f g ihf ihg,
-by rw [ψ.map_add, ψ'.map_add, ihf, ihg]
-
-def set_to_set (S T : set ι) (H : S ⊆ T) :
-  direct_sum R S (β ∘ subtype.val) →ₗ direct_sum R T (β ∘ subtype.val) :=
-to_module $ λ i, of (β ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
-
-protected def id (M : Type v) [add_comm_group M] [module R M] :
-  direct_sum R punit (λ _, M) ≃ₗ M :=
-linear_equiv.of_linear (to_module $ λ _, linear_map.id) (of (λ _, M) punit.star)
-  (linear_map.ext $ λ x, to_module.of _ _)
-  (linear_map.ext $ to_module.ext $ λ ⟨⟩, linear_map.ext $ λ m, by dsimp; rw to_module.of; refl)
-
-instance : has_coe_to_fun (direct_sum R ι β) :=
-dfinsupp.has_coe_to_fun
-
-end direct_sum
+variables (ι γ φ)
+def to_module : direct_sum ι β →ₗ γ :=
+{ to_fun := to_group (λ i, φ i),
+  add := to_group_add _,
+  smul := λ c x, direct_sum.induction_on x
+    (by rw [smul_zero, to_group_zero, smul_zero])
+    (λ i x, by rw [← of_smul, to_group_of, to_group_of, (φ i).map_smul c x])
+    (λ x y ihx ihy, by rw [smul_add, to_group_add, ihx, ihy, to_group_add, smul_add]) }
+variables {ι γ φ}
+
+@[simp] lemma to_module_lof (i) (x : β i) : to_module ι γ φ (lof ι β i x) = φ i x :=
+to_group_of (λ i, φ i) i x
+
+variables (ψ : direct_sum ι β →ₗ γ)
+
+theorem to_module.unique (f : direct_sum ι β) : ψ f = to_module ι γ (λ i, ψ.comp $ lof ι β i) f :=
+to_group.unique ψ f
+
+variables {ψ} {ψ' : direct_sum ι β →ₗ γ}
+
+theorem to_module.ext (H : ∀ i, ψ.comp (lof ι β i) = ψ'.comp (lof ι β i)) (f : direct_sum ι β) :
+  ψ f = ψ' f :=
+by rw [to_module.unique ψ, to_module.unique ψ', funext H]
+
+def lset_to_set (S T : set ι) (H : S ⊆ T) :
+  direct_sum S (β ∘ subtype.val) →ₗ direct_sum T (β ∘ subtype.val) :=
+to_module _ _ $ λ i, lof T (β ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
+
+protected def lid (M : Type v) [add_comm_group M] [module R M] :
+  direct_sum punit (λ _, M) ≃ₗ M :=
+{ .. direct_sum.id M,
+  .. to_module punit M (λ i, linear_map.id) }
+
+end direct_sum

src/linear_algebra/tensor_product.lean

@@ -395,19 +395,19 @@ variables (β₁ : ι₁ → Type*) (β₂ : ι₂ → Type*)
 variables [Π i₁, add_comm_group (β₁ i₁)] [Π i₂, add_comm_group (β₂ i₂)]
 variables [Π i₁, module R (β₁ i₁)] [Π i₂, module R (β₂ i₂)]
 
-def direct_sum : direct_sum R ι₁ β₁ ⊗ direct_sum R ι₂ β₂
-  ≃ₗ direct_sum R (ι₁ × ι₂) (λ i, β₁ i.1 ⊗ β₂ i.2) :=
+def direct_sum : direct_sum ι₁ β₁ ⊗ direct_sum ι₂ β₂
+  ≃ₗ direct_sum (ι₁ × ι₂) (λ i, β₁ i.1 ⊗ β₂ i.2) :=
 begin
   refine linear_equiv.of_linear
-    (lift $ direct_sum.to_module $ λ i₁, flip $ direct_sum.to_module $ λ i₂,
-      flip $ curry $ direct_sum.of (λ i : ι₁ × ι₂, β₁ i.1 ⊗ β₂ i.2) (i₁, i₂))
-    (direct_sum.to_module $ λ i, map (direct_sum.of _ _) (direct_sum.of _ _))
+    (lift $ direct_sum.to_module _ _ $ λ i₁, flip $ direct_sum.to_module _ _ $ λ i₂,
+      flip $ curry $ direct_sum.lof (ι₁ × ι₂) (λ i, β₁ i.1 ⊗ β₂ i.2) (i₁, i₂))
+    (direct_sum.to_module _ _ $ λ i, map (direct_sum.lof _ _ _) (direct_sum.lof _ _ _))
     (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.of <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
+    rw direct_sum.to_module_lof <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
     rw curry_apply },
   cases i; refl
 end