From fdbe954932c68567bc4d4eaae29cc8ce37b59872 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 21 Jul 2020 11:14:20 +0100 Subject: [PATCH 1/6] feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid --- src/data/dfinsupp.lean | 11 ++++++----- src/linear_algebra/direct_sum_module.lean | 2 +- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 64b3c32d50282..4d1f0f045d6bc 100644 --- a/src/data/dfinsupp.lean +++ b/src/data/dfinsupp.lean @@ -146,21 +146,22 @@ instance [Π i, add_comm_group (β i)] : add_comm_group (Π₀ i, β i) := /-- Dependent functions with finite support inherit a semiring action from an action on each coordinate. -/ -def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] : +def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] : has_scalar γ (Π₀ i, β i) := ⟨λc v, v.map_range (λ _, (•) c) (λ _, smul_zero _)⟩ local attribute [instance] to_has_scalar -@[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] +@[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] {i : ι} {b : γ} {v : Π₀ i, β i} : (b • v) i = b • (v i) := map_range_apply /-- Dependent functions with finite support inherit a semimodule structure from such a structure on each coordinate. -/ -def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] : - semimodule γ (Π₀ i, β i) := -semimodule.of_core { +def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] : + semimodule γ (Π₀ i, β i) := { + smul_zero := λ c, ext $ λ i, by simp only [smul_apply, smul_zero, zero_apply], + zero_smul := λ c, ext $ λ i, by simp only [smul_apply, zero_smul, zero_apply], smul_add := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, smul_add], add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul], one_smul := λ x, ext $ λ i, by simp only [smul_apply, one_smul], diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean index 4196caf26d630..d750ef0a0f20d 100644 --- a/src/linear_algebra/direct_sum_module.lean +++ b/src/linear_algebra/direct_sum_module.lean @@ -36,7 +36,7 @@ open_locale direct_sum variables {R ι M} -instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule +instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ (λ i, by apply_instance) _ variables R ι M /-- Create the direct sum given a family `M` of `R` semimodules indexed over `ι`. -/ From 1ff0b75ae75ad6d3191348dc297a9d18eab25ac9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 21 Jul 2020 13:57:06 +0100 Subject: [PATCH 2/6] fixup: Relax some more constraints to try and make the build succeed --- src/data/dfinsupp.lean | 4 ++-- src/linear_algebra/direct_sum_module.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 4d1f0f045d6bc..e025f4cc4fa5f 100644 --- a/src/data/dfinsupp.lean +++ b/src/data/dfinsupp.lean @@ -428,7 +428,7 @@ instance [Π i, add_group (β i)] {s : finset ι} : is_add_group_hom (@mk ι β section local attribute [instance] to_semimodule -variables (γ : Type w) [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] +variables (γ : Type w) [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] include γ @[simp] lemma mk_smul {s : finset ι} {c : γ} (x : Π i : (↑s : set ι), β i.1) : @@ -607,7 +607,7 @@ by ext i; simp local attribute [instance] dfinsupp.to_semimodule -lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] +lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support := support_map_range diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean index d750ef0a0f20d..f725762c7bd9b 100644 --- a/src/linear_algebra/direct_sum_module.lean +++ b/src/linear_algebra/direct_sum_module.lean @@ -36,7 +36,7 @@ open_locale direct_sum variables {R ι M} -instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ (λ i, by apply_instance) _ +instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ _ _ variables R ι M /-- Create the direct sum given a family `M` of `R` semimodules indexed over `ι`. -/ From cffe27a3cb83f39efc5a5702b4126c8559f1f686 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 21 Jul 2020 14:41:27 +0100 Subject: [PATCH 3/6] Add explicit arguments that the lean elaborator cannot work out --- src/algebra/direct_limit.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean index dfc997c81c6f8..69a3310f8dade 100644 --- a/src/algebra/direct_limit.lean +++ b/src/algebra/direct_limit.lean @@ -159,7 +159,7 @@ span_induction ((quotient.mk_eq_zero _).1 H) to_module_totalize_of_le hik hi, to_module_totalize_of_le hjk hj]⟩) (λ a x ⟨i, hi, hxi⟩, - ⟨i, λ k hk, hi k (dfinsupp.support_smul hk), + ⟨i, λ k hk, hi k (@dfinsupp.support_smul ι G _ _ _ _ _ _ _ _ _ hk), by simp [linear_map.map_smul, hxi]⟩) /-- A component that corresponds to zero in the direct limit is already zero in some From 5c7490767598cc3aee377009b20cddb320af265a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 21 Jul 2020 14:58:09 +0100 Subject: [PATCH 4/6] Add explicit arguments that the lean elaborator cannot work out --- src/algebra/lie_algebra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/lie_algebra.lean b/src/algebra/lie_algebra.lean index c5c2256518155..5c8bbdeda397b 100644 --- a/src/algebra/lie_algebra.lean +++ b/src/algebra/lie_algebra.lean @@ -334,7 +334,7 @@ instance : lie_ring (direct_sum ι L) := { /-- The direct sum of Lie algebras carries a natural Lie algebra structure. -/ instance : lie_algebra R (direct_sum ι L) := -{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, smul_apply, bracket_apply, lie_smul], }, +{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, @smul_apply ι L _ _ _ _ _ _ _, bracket_apply, lie_smul],}, ..(infer_instance : module R _) } end direct_sum From 31274849eb1d479927bafd9052a376ea4840fe97 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 26 Oct 2020 14:13:36 +0000 Subject: [PATCH 5/6] Apply suggestions from code review Co-authored-by: Anne Baanen --- src/algebra/lie/basic.lean | 2 +- src/data/dfinsupp.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/algebra/lie/basic.lean b/src/algebra/lie/basic.lean index ff01a6ab8f97d..c2dfd7fc790e2 100644 --- a/src/algebra/lie/basic.lean +++ b/src/algebra/lie/basic.lean @@ -314,7 +314,7 @@ instance : lie_ring (⨁ i, L i) := /-- The direct sum of Lie algebras carries a natural Lie algebra structure. -/ instance : lie_algebra R (⨁ i, L i) := -{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, @smul_apply ι L _ _ _ _ _ _ _, bracket_apply, lie_smul],}, +{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, @smul_apply ι L _ _ _ _ _ _ _, bracket_apply, lie_smul] }, ..(infer_instance : module R _) } end direct_sum diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 6f31c4162ed62..cac0d33609a06 100644 --- a/src/data/dfinsupp.lean +++ b/src/data/dfinsupp.lean @@ -159,8 +159,8 @@ map_range_apply /-- Dependent functions with finite support inherit a semimodule structure from such a structure on each coordinate. -/ def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] : - semimodule γ (Π₀ i, β i) := { - smul_zero := λ c, ext $ λ i, by simp only [smul_apply, smul_zero, zero_apply], + semimodule γ (Π₀ i, β i) := +{ smul_zero := λ c, ext $ λ i, by simp only [smul_apply, smul_zero, zero_apply], zero_smul := λ c, ext $ λ i, by simp only [smul_apply, zero_smul, zero_apply], smul_add := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, smul_add], add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul], From bfe4595975d832d42f1076d7bd712a86521aa6a1 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 28 Oct 2020 12:47:17 -0400 Subject: [PATCH 6/6] implicitness fixes --- src/algebra/direct_limit.lean | 2 +- src/algebra/direct_sum.lean | 7 +++++++ src/algebra/lie/basic.lean | 10 ++++++---- src/data/dfinsupp.lean | 19 +++++++++---------- src/linear_algebra/direct_sum_module.lean | 13 ++++++++++--- 5 files changed, 33 insertions(+), 18 deletions(-) diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean index 0d40f32f2e3cb..806b3702c7c54 100644 --- a/src/algebra/direct_limit.lean +++ b/src/algebra/direct_limit.lean @@ -175,7 +175,7 @@ span_induction ((quotient.mk_eq_zero _).1 H) to_module_totalize_of_le hik hi, to_module_totalize_of_le hjk hj]⟩) (λ a x ⟨i, hi, hxi⟩, - ⟨i, λ k hk, hi k (@dfinsupp.support_smul ι G _ _ _ _ _ _ _ _ _ hk), + ⟨i, λ k hk, hi k (direct_sum.support_smul _ _ hk), by simp [linear_map.map_smul, hxi]⟩) /-- A component that corresponds to zero in the direct limit is already zero in some diff --git a/src/algebra/direct_sum.lean b/src/algebra/direct_sum.lean index 017e50a83ebd2..0c0ff65a01271 100644 --- a/src/algebra/direct_sum.lean +++ b/src/algebra/direct_sum.lean @@ -39,6 +39,13 @@ namespace direct_sum variables {ι} +@[simp] lemma zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 := rfl + +variables {β} +@[simp] lemma add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i := +dfinsupp.add_apply _ _ _ + +variables (β) include dec_ι /-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s` diff --git a/src/algebra/lie/basic.lean b/src/algebra/lie/basic.lean index c2dfd7fc790e2..7fbc7bc2f01de 100644 --- a/src/algebra/lie/basic.lean +++ b/src/algebra/lie/basic.lean @@ -306,7 +306,8 @@ instance : lie_ring (⨁ i, L i) := add_lie := λ x y z, by { ext, simp only [zip_with_apply, add_apply, add_lie], }, lie_add := λ x y z, by { ext, simp only [zip_with_apply, add_apply, lie_add], }, lie_self := λ x, by { ext, simp only [zip_with_apply, add_apply, lie_self, zero_apply], }, - jacobi := λ x y z, by { ext, simp only [zip_with_apply, add_apply, lie_ring.jacobi, zero_apply], }, + jacobi := λ x y z, by { ext, simp only [ + zip_with_apply, add_apply, lie_ring.jacobi, zero_apply], }, ..(infer_instance : add_comm_group _) } @[simp] lemma bracket_apply {x y : (⨁ i, L i)} {i : ι} : @@ -314,7 +315,8 @@ instance : lie_ring (⨁ i, L i) := /-- The direct sum of Lie algebras carries a natural Lie algebra structure. -/ instance : lie_algebra R (⨁ i, L i) := -{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, @smul_apply ι L _ _ _ _ _ _ _, bracket_apply, lie_smul] }, +{ lie_smul := λ c x y, by { ext, simp only [ + zip_with_apply, direct_sum.smul_apply, bracket_apply, lie_smul] }, ..(infer_instance : module R _) } end direct_sum @@ -341,8 +343,8 @@ def of_associative_algebra_hom {R : Type u} {A : Type v} {B : Type w} by simp only [lie_ring.of_associative_ring_bracket, alg_hom.map_sub, alg_hom.map_mul], ..f.to_linear_map, } -@[simp] lemma of_associative_algebra_hom_id {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] : - of_associative_algebra_hom (alg_hom.id R A) = 1 := rfl +@[simp] lemma of_associative_algebra_hom_id {R : Type u} {A : Type v} + [comm_ring R] [ring A] [algebra R A] : of_associative_algebra_hom (alg_hom.id R A) = 1 := rfl @[simp] lemma of_associative_algebra_hom_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [comm_ring R] [ring A] [ring B] [ring C] [algebra R A] [algebra R B] [algebra R C] diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 49c949a6a7770..5ff6a96ccaaeb 100644 --- a/src/data/dfinsupp.lean +++ b/src/data/dfinsupp.lean @@ -62,10 +62,9 @@ instance : has_coe_to_fun (Π₀ i, β i) := instance : has_zero (Π₀ i, β i) := ⟨⟦⟨λ i, 0, ∅, λ i, or.inr rfl⟩⟧⟩ instance : inhabited (Π₀ i, β i) := ⟨0⟩ -@[simp] lemma zero_apply {i : ι} : (0 : Π₀ i, β i) i = 0 := rfl +@[simp] lemma zero_apply (i : ι) : (0 : Π₀ i, β i) i = 0 := rfl -@[ext] -lemma ext {f g : Π₀ i, β i} (H : ∀ i, f i = g i) : f = g := +@[ext] lemma ext {f g : Π₀ i, β i} (H : ∀ i, f i = g i) : f = g := quotient.induction_on₂ f g (λ _ _ H, quotient.sound H) H /-- The composition of `f : β₁ → β₂` and `g : Π₀ i, β₁ i` is @@ -107,7 +106,7 @@ section algebra instance [Π i, add_monoid (β i)] : has_add (Π₀ i, β i) := ⟨zip_with (λ _, (+)) (λ _, add_zero 0)⟩ -@[simp] lemma add_apply [Π i, add_monoid (β i)] {g₁ g₂ : Π₀ i, β i} {i : ι} : +@[simp] lemma add_apply [Π i, add_monoid (β i)] (g₁ g₂ : Π₀ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i := zip_with_apply @@ -119,8 +118,8 @@ instance [Π i, add_monoid (β i)] : add_monoid (Π₀ i, β i) := zero_add := λ f, ext $ λ i, by simp only [add_apply, zero_apply, zero_add], add_zero := λ f, ext $ λ i, by simp only [add_apply, zero_apply, add_zero] } -instance [Π i, add_monoid (β i)] {i : ι} : is_add_monoid_hom (λ g : Π₀ i : ι, β i, g i) := -{ map_add := λ _ _, add_apply, map_zero := zero_apply } +instance [Π i, add_monoid (β i)] (i : ι) : is_add_monoid_hom (λ g : Π₀ i : ι, β i, g i) := +{ map_add := λ _ _, add_apply _ _ _, map_zero := zero_apply _ } instance [Π i, add_group (β i)] : has_neg (Π₀ i, β i) := ⟨λ f, f.map_range (λ _, has_neg.neg) (λ _, neg_zero)⟩ @@ -153,7 +152,7 @@ def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π local attribute [instance] to_has_scalar @[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] - [Π i, semimodule γ (β i)] {i : ι} {b : γ} {v : Π₀ i, β i} : + [Π i, semimodule γ (β i)] (b : γ) (v : Π₀ i, β i) (i : ι) : (b • v) i = b • (v i) := map_range_apply @@ -609,9 +608,9 @@ by ext i; simp local attribute [instance] dfinsupp.to_semimodule -lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] - [Π (i : ι) (x : β i), decidable (x ≠ 0)] - {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support := +lemma support_smul {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] + [Π ( i : ι) (x : β i), decidable (x ≠ 0)] + (b : γ) (v : Π₀ i, β i) : (b • v).support ⊆ v.support := support_map_range instance [Π i, has_zero (β i)] [Π i, decidable_eq (β i)] : decidable_eq (Π₀ i, β i) := diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean index b3bfa6920b069..e3e394a3f202b 100644 --- a/src/linear_algebra/direct_sum_module.lean +++ b/src/linear_algebra/direct_sum_module.lean @@ -38,6 +38,9 @@ variables {R ι M} instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ _ _ +@[simp] lemma smul_apply (b : R) (v : ⨁ i, M i) (i : ι) : + (b • v) i = b • (v i) := dfinsupp.smul_apply _ _ _ + include dec_ι variables R ι M @@ -61,10 +64,14 @@ theorem mk_smul (s : finset ι) (c : R) (x) : mk M s (c • x) = c • mk M s x theorem of_smul (i : ι) (c : R) (x) : of M i (c • x) = c • of M i x := (lof R ι M i).map_smul c x +variables {R} +lemma support_smul [Π (i : ι) (x : M i), decidable (x ≠ 0)] + (c : R) (v : ⨁ i, M i) : (c • v).support ⊆ v.support := dfinsupp.support_smul _ _ + variables {N : Type u₁} [add_comm_group N] [semimodule R N] variables (φ : Π i, M i →ₗ[R] N) -variables (ι N φ) +variables (R ι N φ) /-- The linear map constructed using the universal property of the coproduct. -/ def to_module : (⨁ i, M i) →ₗ[R] N := { to_fun := to_group (λ i, (φ i).to_add_monoid_hom), @@ -119,8 +126,8 @@ variables (ι M) /-- The projection map onto one component, as a linear map. -/ def component (i : ι) : (⨁ i, M i) →ₗ[R] M i := { to_fun := λ f, f i, - map_add' := λ _ _, dfinsupp.add_apply, - map_smul' := λ _ _, dfinsupp.smul_apply } + map_add' := λ _ _, dfinsupp.add_apply _ _ _, + map_smul' := λ _ _, dfinsupp.smul_apply _ _ _ } variables {ι M}