feat(algebra/direct_sum): Add ⨁ notation (#3473)

This uses the unicode character "n-ary circled plus operator", which seems to be the usual symbol for this operation




Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: eric-wieser

src/algebra/direct_sum.lean

@@ -3,10 +3,24 @@ 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
 
+/-!
+# Direct sum
+
+This file defines the direct sum of abelian groups, indexed by a discrete type.
+
+## Notation
+
+`⨁ i, β i` is the n-ary direct sum `direct_sum`.
+This notation is in the `direct_sum` locale, accessible after `open_locale direct_sum`.
+
+## References
+
+* https://en.wikipedia.org/wiki/Direct_sum
+-/
+
 open_locale big_operators
 
 universes u v w u₁
@@ -15,20 +29,22 @@ variables (ι : Type v) [decidable_eq ι] (β : ι → Type w) [Π i, add_comm_g
 
 def direct_sum : Type* := Π₀ i, β i
 
+localized "notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
+
 namespace direct_sum
 
 variables {ι β}
 
-instance : add_comm_group (direct_sum ι β) :=
+instance : add_comm_group (⨁ i, β i) :=
 dfinsupp.add_comm_group
 
-instance : inhabited (direct_sum ι β) := ⟨0⟩
+instance : inhabited (⨁ i, β i) := ⟨0⟩
 
 variables β
-def mk : Π s : finset ι, (Π i : (↑s : set ι), β i.1) → direct_sum ι β :=
+def mk : Π s : finset ι, (Π i : (↑s : set ι), β i.1) → ⨁ i, β i :=
 dfinsupp.mk
 
-def of : Π i : ι, β i → direct_sum ι β :=
+def of : Π i : ι, β i → ⨁ i, β i :=
 dfinsupp.single
 variables {β}
 
@@ -69,8 +85,8 @@ theorem of_injective (i : ι) : function.injective (of β i) :=
 λ x y H, congr_fun (mk_injective _ H) ⟨i, by simp⟩
 
 @[elab_as_eliminator]
-protected theorem induction_on {C : direct_sum ι β → Prop}
-  (x : direct_sum ι β) (H_zero : C 0)
+protected theorem induction_on {C : (⨁ i, β i) → Prop}
+  (x : ⨁ i, β i) (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
@@ -83,7 +99,7 @@ variables {γ : Type u₁} [add_comm_group γ]
 variables (φ : Π i, β i → γ) [Π i, is_add_group_hom (φ i)]
 
 variables (φ)
-def to_group (f : direct_sum ι β) : γ :=
+def to_group (f : ⨁ i, β i) : γ :=
 quotient.lift_on f (λ x, ∑ i in x.2.to_finset, φ 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 _ _,
@@ -135,9 +151,9 @@ is_add_group_hom.map_sub _ x y
 (add_zero _).trans $ congr_arg (φ i) $ show (if H : i ∈ ({i} : finset _) then x else 0) = x,
 from dif_pos $ finset.mem_singleton_self i
 
-variables (ψ : direct_sum ι β → γ) [is_add_group_hom ψ]
+variables (ψ : (⨁ i, β i) → γ) [is_add_group_hom ψ]
 
-theorem to_group.unique (f : direct_sum ι β) :
+theorem to_group.unique (f : ⨁ i, β i) :
   ψ f = @to_group _ _ _ _ _ _ (λ i, ψ ∘ of β i) (λ i, is_add_group_hom.comp (of β i) ψ) f :=
 by haveI : ∀ i, is_add_group_hom (ψ ∘ of β i) := (λ _, is_add_group_hom.comp _ _); exact
 direct_sum.induction_on f
@@ -147,14 +163,14 @@ direct_sum.induction_on f
 
 variables (β)
 def set_to_set (S T : set ι) (H : S ⊆ T) :
-  direct_sum S (β ∘ subtype.val) → direct_sum T (β ∘ subtype.val) :=
+  (⨁ (i : S), β i) → (⨁ (i : T), β i) :=
 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 :=
+protected def id (M : Type v) [add_comm_group M] : (⨁ (_ : punit), M) ≃ M :=
 { to_fun := direct_sum.to_group (λ _, id),
   inv_fun := of (λ _, M) punit.star,
   left_inv := λ x, direct_sum.induction_on x
@@ -163,7 +179,7 @@ protected def id (M : Type v) [add_comm_group M] : direct_sum punit (λ _, M) 
     (λ 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 ι β) :=
+instance : has_coe_to_fun (⨁ i, β i) :=
 dfinsupp.has_coe_to_fun
 
 end direct_sum

src/linear_algebra/direct_sum/tensor_product.lean

@@ -11,6 +11,7 @@ section ring
 namespace tensor_product
 
 open_locale tensor_product
+open_locale direct_sum
 open linear_map
 
 variables (R : Type*) [comm_ring R]
@@ -20,10 +21,10 @@ 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.
+/-- 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) :=
+  (⨁ i₁, M₁ i₁) ⊗[R] (⨁ i₂, M₂ i₂) ≃ₗ[R] (⨁ (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₂,

src/linear_algebra/direct_sum_module.lean

@@ -32,18 +32,19 @@ variables [Π i, add_comm_group (M i)] [Π i, semimodule R (M i)]
 include R
 
 namespace direct_sum
+open_locale direct_sum
 
 variables {R ι M}
 
-instance : semimodule R (direct_sum ι M) := dfinsupp.to_semimodule
+instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule
 
 variables R ι M
 /-- Create the direct sum given a family `M` of `R` semimodules indexed over `ι`. -/
-def lmk : Π s : finset ι, (Π i : (↑s : set ι), M i.val) →ₗ[R] direct_sum ι M :=
+def lmk : Π s : finset ι, (Π i : (↑s : set ι), M i.val) →ₗ[R] (⨁ i, M i) :=
 dfinsupp.lmk M R
 
 /-- Inclusion of each component into the direct sum. -/
-def lof : Π i : ι, M i →ₗ[R] direct_sum ι M :=
+def lof : Π i : ι, M i →ₗ[R] (⨁ i, M i) :=
 dfinsupp.lsingle M R
 variables {ι M}
 
@@ -63,7 +64,7 @@ variables (φ : Π i, M i →ₗ[R] N)
 
 variables (ι N φ)
 /-- The linear map constructed using the universal property of the coproduct. -/
-def to_module : direct_sum ι M →ₗ[R] N :=
+def to_module : (⨁ i, M i) →ₗ[R] N :=
 { to_fun := to_group (λ i, φ i),
   map_add' := to_group_add _,
   map_smul' := λ c x, direct_sum.induction_on x
@@ -78,16 +79,16 @@ restricted to each component. -/
 @[simp] lemma to_module_lof (i) (x : M i) : to_module R ι N φ (lof R ι M i x) = φ i x :=
 to_group_of (λ i, φ i) i x
 
-variables (ψ : direct_sum ι M →ₗ[R] N)
+variables (ψ : (⨁ i, M i) →ₗ[R] N)
 
 /-- Every linear map from a direct sum agrees with the one obtained by applying
 the universal property to each of its components. -/
-theorem to_module.unique (f : direct_sum ι M) : ψ f = to_module R ι N (λ i, ψ.comp $ lof R ι M i) f :=
+theorem to_module.unique (f : ⨁ i, M i) : ψ f = to_module R ι N (λ i, ψ.comp $ lof R ι M i) f :=
 to_group.unique ψ f
 
-variables {ψ} {ψ' : direct_sum ι M →ₗ[R] N}
+variables {ψ} {ψ' : (⨁ i, M i) →ₗ[R] N}
 
-theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) (f : direct_sum ι M) :
+theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) (f : ⨁ i, M i) :
   ψ f = ψ' f :=
 by rw [to_module.unique R ψ, to_module.unique R ψ', funext H]
 
@@ -96,17 +97,17 @@ The inclusion of a subset of the direct summands
 into a larger subset of the direct summands, as a linear map.
 -/
 def lset_to_set (S T : set ι) (H : S ⊆ T) :
-  direct_sum S (M ∘ subtype.val) →ₗ direct_sum T (M ∘ subtype.val) :=
+  (⨁ (i : S), M i) →ₗ (⨁ (i : T), M i) :=
 to_module R _ _ $ λ i, lof R T (M ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
 
 protected def lid (M : Type v) [add_comm_group M] [semimodule R M] :
-  direct_sum punit (λ _, M) ≃ₗ M :=
+  (⨁ (_ : punit), M) ≃ₗ M :=
 { .. direct_sum.id M,
   .. to_module R punit M (λ i, linear_map.id) }
 
 variables (ι M)
 /-- The projection map onto one component, as a linear map. -/
-def component (i : ι) : direct_sum ι M →ₗ[R] M i :=
+def component (i : ι) : (⨁ i, M i) →ₗ[R] M i :=
 { to_fun := λ f, f i,
   map_add' := λ _ _, dfinsupp.add_apply,
   map_smul' := λ _ _, dfinsupp.smul_apply }
@@ -115,7 +116,7 @@ variables {ι M}
 @[simp] lemma lof_apply (i : ι) (b : M i) : ((lof R ι M i) b) i = b :=
 by rw [lof, dfinsupp.lsingle_apply, dfinsupp.single_apply, dif_pos rfl]
 
-lemma apply_eq_component (f : direct_sum ι M) (i : ι) :
+lemma apply_eq_component (f : ⨁ i, M i) (i : ι) :
   f i = component R ι M i f := rfl
 
 @[simp] lemma component.lof_self (i : ι) (b : M i) :
@@ -127,11 +128,11 @@ lemma component.of (i j : ι) (b : M j) :
   if h : j = i then eq.rec_on h b else 0 :=
 dfinsupp.single_apply
 
-@[ext] lemma ext {f g : direct_sum ι M}
+@[ext] lemma ext {f g : ⨁ i, M i}
   (h : ∀ i, component R ι M i f = component R ι M i g) : f = g :=
 dfinsupp.ext h
 
-lemma ext_iff {f g : direct_sum ι M} : f = g ↔
+lemma ext_iff {f g : ⨁ i, M i} : f = g ↔
   ∀ i, component R ι M i f = component R ι M i g :=
 ⟨λ h _, by rw h, ext R⟩