Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
int-y1 committed Mar 3, 2023
1 parent a963e6b commit 1a87c5b
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 19 deletions.
20 changes: 7 additions & 13 deletions Mathlib/Algebra/DirectSum/Module.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,16 +40,14 @@ variable {R : Type u} [Semiring R]

variable {ι : Type v} [dec_ι : DecidableEq ι]

include R

variable {M : ι → Type w} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]

instance : Module R (⨁ i, M i) :=
Dfinsupp.module

instance {S : Type _} [Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] :
SMulCommClass R S (⨁ i, M i) :=
Dfinsupp.sMulCommClass
Dfinsupp.smulCommClass

instance {S : Type _} [Semiring S] [SMul R S] [∀ i, Module S (M i)] [∀ i, IsScalarTower R S (M i)] :
IsScalarTower R S (⨁ i, M i) :=
Expand All @@ -62,8 +60,6 @@ theorem smul_apply (b : R) (v : ⨁ i, M i) (i : ι) : (b • v) i = b • v i :
Dfinsupp.smul_apply _ _ _
#align direct_sum.smul_apply DirectSum.smul_apply

include dec_ι

variable (R ι M)

/-- Create the direct sum given a family `M` of `R` modules indexed over `ι`. -/
Expand Down Expand Up @@ -107,11 +103,11 @@ variable {N : Type u₁} [AddCommMonoid N] [Module R N]

variable (φ : ∀ i, M i →ₗ[R] N)

variable (R ι N φ)
variable (R ι N)

/-- The linear map constructed using the universal property of the coproduct. -/
def toModule : (⨁ i, M i) →ₗ[R] N :=
Dfinsupp.lsum ℕ φ
FunLike.coe (Dfinsupp.lsum ℕ) φ
#align direct_sum.to_module DirectSum.toModule

/-- Coproducts in the categories of modules and additive monoids commute with the forgetful functor
Expand Down Expand Up @@ -153,25 +149,24 @@ theorem linearMap_ext ⦃ψ ψ' : (⨁ i, M i) →ₗ[R] N⦄
into a larger subset of the direct summands, as a linear map.
-/
def lsetToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, M i) →ₗ[R] ⨁ i : T, M i :=
toModule R _ _ fun i => lof R T (fun i : Subtype T => M i) ⟨i, H i.Prop
toModule R _ _ fun i => lof R T (fun i : Subtype T => M i) ⟨i, H i.prop
#align direct_sum.lset_to_set DirectSum.lsetToSet

omit dec_ι

variable (ι M)

/-- Given `fintype α`, `linear_equiv_fun_on_fintype R` is the natural `R`-linear equivalence
between `⨁ i, M i` and `Π i, M i`. -/
@[simps apply]
def linearEquivFunOnFintype [Fintype ι] : (⨁ i, M i) ≃ₗ[R] ∀ i, M i :=
{ Dfinsupp.equivFunOnFintype with
toFun := coeFn
toFun := (↑)
map_add' := fun f g => by
ext
simp only [add_apply, Pi.add_apply]
map_smul' := fun c f => by
ext
simp only [Dfinsupp.coe_smul, RingHom.id_apply] }
simp only [Dfinsupp.coe_smul, RingHom.id_apply]
rfl }
#align direct_sum.linear_equiv_fun_on_fintype DirectSum.linearEquivFunOnFintype

variable {ι M}
Expand Down Expand Up @@ -457,4 +452,3 @@ end Ring
end Submodule

end DirectSum

13 changes: 7 additions & 6 deletions Mathlib/Data/Dfinsupp/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -360,16 +360,17 @@ theorem coe_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction
rfl
#align dfinsupp.coe_smul Dfinsupp.coe_smul

instance {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
[∀ i, DistribMulAction δ (β i)] [∀ i, SMulCommClass γ δ (β i)] : SMulCommClass γ δ (Π₀ i, β i)
instance smulCommClass {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)]
[∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction δ (β i)] [∀ i, SMulCommClass γ δ (β i)] :
SMulCommClass γ δ (Π₀ i, β i)
where smul_comm r s m := ext fun i => by simp only [smul_apply, smul_comm r s (m i)]

instance {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
[∀ i, DistribMulAction δ (β i)] [SMul γ δ] [∀ i, IsScalarTower γ δ (β i)] :
IsScalarTower γ δ (Π₀ i, β i)
instance isScalarTower {δ : Type _} [Monoid γ] [Monoid δ] [∀ i, AddMonoid (β i)]
[∀ i, DistribMulAction γ (β i)] [∀ i, DistribMulAction δ (β i)] [SMul γ δ]
[∀ i, IsScalarTower γ δ (β i)] : IsScalarTower γ δ (Π₀ i, β i)
where smul_assoc r s m := ext fun i => by simp only [smul_apply, smul_assoc r s (m i)]

instance [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
instance isCentralScalar [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
[∀ i, DistribMulAction γᵐᵒᵖ (β i)] [∀ i, IsCentralScalar γ (β i)] :
IsCentralScalar γ (Π₀ i, β i)
where op_smul_eq_smul r m := ext fun i => by simp only [smul_apply, op_smul_eq_smul r (m i)]
Expand Down

0 comments on commit 1a87c5b

Please sign in to comment.