chore(algebra/direct_sum): linting (#4412)

src/algebra/direct_sum.lean

@@ -25,8 +25,11 @@ open_locale big_operators
 
 universes u v w u₁
 
-variables (ι : Type v) [decidable_eq ι] (β : ι → Type w) [Π i, add_comm_group (β i)]
+variables (ι : Type v) [dec_ι : decidable_eq ι] (β : ι → Type w) [Π i, add_comm_group (β i)]
 
+/-- `direct_sum β` is the direct sum of a family of additive commutative groups `β i`.
+
+Note: `open_locale direct_sum` will enable the notation `⨁ i, β i` for `direct_sum β`. -/
 def direct_sum : Type* := Π₀ i, β i
 
 localized "notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
@@ -41,9 +44,15 @@ dfinsupp.add_comm_group
 instance : inhabited (⨁ i, β i) := ⟨0⟩
 
 variables β
+
+include dec_ι
+
+/-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
+and has coefficient `x i` for `i` in `s`. -/
 def mk : Π s : finset ι, (Π i : (↑s : set ι), β i.1) → ⨁ i, β i :=
 dfinsupp.mk
 
+/-- `of i` is the natural inclusion map from `β i` to `⨁ i, β i`. -/
 def of : Π i : ι, β i → ⨁ i, β i :=
 dfinsupp.single
 variables {β}
@@ -99,6 +108,8 @@ variables {γ : Type u₁} [add_comm_group γ]
 variables (φ : Π i, β i → γ) [Π i, is_add_group_hom (φ i)]
 
 variables (φ)
+/-- `to_group φ` is the natural homomorphism from `⨁ i, β i` to `γ`
+induced by a family `φ` of homomorphisms `β i → γ`. -/
 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
@@ -162,6 +173,9 @@ direct_sum.induction_on f
   (λ x y ihx ihy, by rw [is_add_hom.map_add ψ, is_add_hom.map_add (to_group (λ i, ψ ∘ of β i)), ihx, ihy])
 
 variables (β)
+/-- `set_to_set β S T h` is the natural homomorphism `⨁ (i : S), β i → ⨁ (i : T), β i`,
+where `h : S ⊆ T`. -/
+-- TODO: generalize this to remove the assumption `S ⊆ T`.
 def set_to_set (S T : set ι) (H : S ⊆ T) :
   (⨁ (i : S), β i) → (⨁ (i : T), β i) :=
 to_group $ λ i, of (β ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
@@ -170,6 +184,10 @@ variables {β}
 instance (S T : set ι) (H : S ⊆ T) : is_add_group_hom (set_to_set β S T H) :=
 to_group.is_add_group_hom
 
+omit dec_ι
+
+/-- The natural equivalence between `⨁ _ : punit, M` and `M`. -/
+-- TODO: generalize this to a sum over any type `ι` that is `unique ι`.
 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,

src/algebra/lie/basic.lean

@@ -297,7 +297,7 @@ open dfinsupp
 open_locale direct_sum
 
 variables {R : Type u} [comm_ring R]
-variables {ι : Type v} [decidable_eq ι] {L : ι → Type w}
+variables {ι : Type v} {L : ι → Type w}
 variables [Π i, lie_ring (L i)] [Π i, lie_algebra R (L i)]
 
 /-- The direct sum of Lie rings carries a natural Lie ring structure. -/

src/linear_algebra/direct_sum_module.lean

@@ -27,7 +27,7 @@ All of this file assumes that
 universes u v w u₁
 
 variables (R : Type u) [semiring R]
-variables (ι : Type v) [decidable_eq ι] (M : ι → Type w)
+variables (ι : Type v) [dec_ι : decidable_eq ι] (M : ι → Type w)
 variables [Π i, add_comm_group (M i)] [Π i, semimodule R (M i)]
 include R
 
@@ -38,6 +38,8 @@ variables {R ι M}
 
 instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule
 
+include dec_ι
+
 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] (⨁ i, M i) :=
@@ -100,6 +102,10 @@ def lset_to_set (S T : set ι) (H : S ⊆ T) :
   (⨁ (i : S), M i) →ₗ (⨁ (i : T), M i) :=
 to_module R _ _ $ λ i, lof R T (M ∘ @subtype.val _ T) ⟨i.1, H i.2⟩
 
+omit dec_ι
+
+/-- The natural linear equivalence between `⨁ _ : punit, M` and `M`. -/
+-- TODO: generalize this to arbitrary index type `ι` with `unique ι`
 protected def lid (M : Type v) [add_comm_group M] [semimodule R M] :
   (⨁ (_ : punit), M) ≃ₗ M :=
 { .. direct_sum.id M,
@@ -113,12 +119,23 @@ def component (i : ι) : (⨁ i, M i) →ₗ[R] M i :=
   map_smul' := λ _ _, dfinsupp.smul_apply }
 
 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 : ⨁ i, M i) (i : ι) :
   f i = component R ι M i f := rfl
 
+@[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 : ⨁ i, M i} : f = g ↔
+  ∀ i, component R ι M i f = component R ι M i g :=
+⟨λ h _, by rw h, ext R⟩
+
+include dec_ι
+
+@[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]
+
 @[simp] lemma component.lof_self (i : ι) (b : M i) :
   component R ι M i ((lof R ι M i) b) = b :=
 lof_apply R i b
@@ -128,12 +145,4 @@ 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 : ⨁ 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 : ⨁ i, M i} : f = g ↔
-  ∀ i, component R ι M i f = component R ι M i g :=
-⟨λ h _, by rw h, ext R⟩
-
 end direct_sum