Small TODO in Algebra/DirectSum/Basic.lean

Stream: new members

[Walter Moreira]

There is this small TODO in the file Algebra/DirectSum/Basic.lean:

-- TODO: generalize this to remove the assumption `S ⊆ T`.
/-- `setToSet β S T h` is the natural homomorphism `⨁ (i : S), β i → ⨁ (i : T), β i`,
where `h : S ⊆ T`. -/
def setToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, β i) →+ ⨁ i : T, β i :=
  toAddMonoid fun i => of (fun i : Subtype T => β i) ⟨↑i, H i.2⟩

The following definition generalizes setToSet and it coincides with the original when S ⊆ T (under the hypothesis of DecidablePred (· ∈ T)). Is it PR worthy?

There is an analogous one for a linear map in Algebra/DirectSum/Module.lean that can be extended in the same way.

import Mathlib
open DirectSum
variable {ι : Type*} (β : ι → Type*) [∀ i, AddCommMonoid (β i)] [DecidableEq ι]

/-- New definition: -/
def setToSetNew (S T : Set ι) [DecidablePred (· ∈ T)] : (⨁ i : S, β i) →+ ⨁ i : T, β i :=
  toAddMonoid fun i => if h : ((i : ι) ∈ T) then of (fun i : T => β i) ⟨↑i, h⟩ else 0

theorem setToSet_eq_setToSetNew_of_subset (S T : Set ι) [DecidablePred (· ∈ T)] (H : S ⊆ T) :
    setToSet β S T H = setToSetNew β S T := by
  rw [setToSet, setToSetNew, toAddMonoid_inj]
  ext x
  simp only [H x.property]
  rfl