From 55005042fd651a7e222ee198ccd31bdc61270bbc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 3 Oct 2020 21:36:44 +0100 Subject: [PATCH 1/5] feat(algebra/monoid_algebra): Add an equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` Note that this needs a new `exact` tactic for conv mode. --- src/algebra/monoid_algebra.lean | 107 +++++++++++++++++++++++++- src/tactic/converter/interactive.lean | 13 ++++ 2 files changed, 119 insertions(+), 1 deletion(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 8a99722544933..2ab8dbf7947fa 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -187,6 +187,38 @@ subset.trans support_sum $ bind_mono $ assume a₁ _, section +/-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/ +lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [monoid α] [monoid α₂] + {x y : monoid_algebra β α} (f : mul_hom α α₂) : + (map_domain f (x * y : monoid_algebra β α) : monoid_algebra β α₂) = + (map_domain f x * map_domain f y : monoid_algebra β α₂) := +begin + simp only [mul_def, map_domain_sum, map_domain_single], + -- I can't work out any way to avoid `conv` here + conv_rhs { + for (finsupp.sum _ _) [2] { + rw finsupp.sum_map_domain_index _ _, + skip, + exact λ a, by { simp, }, + exact λ a b c, by { simp [mul_add], } + }, + for (finsupp.sum _ _) [1] { + rw finsupp.sum_map_domain_index _ _, + skip, + exact λ a, by { simp, }, + exact λ a b c, by { simp [add_mul], }, + }, + }, + simp_rw f.map_mul, +end + +/-- `map_domain_mul` for unbundled morphisms -/ +lemma map_domain_mul' {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [monoid α] [monoid α₂]{x y : monoid_algebra β α} + (f : α → α₂) (hf : ∀ x y, f (x * y) = f x * f y) : + (map_domain f (x * y : monoid_algebra β α) : monoid_algebra β α₂) = + (map_domain f x * map_domain f y : monoid_algebra β α₂) := +map_domain_mul ⟨f, hf⟩ + variables (k G) /-- Embedding of a monoid into its monoid algebra. -/ @@ -535,7 +567,7 @@ instance [comm_semiring k] [add_comm_monoid G] : comm_semiring (add_monoid_algeb simp only [add_comm] end, .. add_monoid_algebra.semiring } - + /-! #### Derived instances -/ section derived_instances @@ -585,6 +617,40 @@ lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} : (sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans (sum_single_index (by rw [mul_zero, single_zero])) +/-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/ +lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} + [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α} + (f : add_hom α α₂) : + (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = + (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := +begin + simp only [mul_def, map_domain_sum, map_domain_single], + -- I can't work out any way to avoid `conv` here + conv_rhs { + for (finsupp.sum _ _) [2] { + rw finsupp.sum_map_domain_index _ _, + skip, + exact λ a, by { simp, }, + exact λ a b c, by { simp [mul_add], } + }, + for (finsupp.sum _ _) [1] { + rw finsupp.sum_map_domain_index _ _, + skip, + exact λ a, by { simp, }, + exact λ a b c, by { simp [add_mul], }, + }, + }, + simp_rw f.map_add, +end + +/-- `map_domain_mul` for unbundled morphisms -/ +lemma map_domain_mul' {α : Type*} {β : Type*} {α₂ : Type*} + [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α} + (f : α → α₂) (hf : ∀ x y, f (x + y) = f x + f y) : + (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = + (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := +map_domain_mul ⟨f, hf⟩ + section variables (k G) @@ -632,6 +698,45 @@ f.single_mul_apply_aux r _ _ _ $ λ a, by rw [zero_add] end misc_theorems +end add_monoid_algebra + +/-! +#### Conversions between `add_monoid_algebra` and `monoid_algebra` + +While we were not able to define `add_monoid_algebra k G = monoid_algebra k (multiplicative G)` due +to definitional inconveniences, we can still show the types are isomorphic. +-/ + +/-- The equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` -/ +protected def add_monoid_algebra.to_multiplicative [semiring k] [add_monoid G] : + add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) := +{ map_mul' := λ x y, by { + simp only [finsupp.dom_congr], + apply add_monoid_algebra.map_domain_mul', + intros p q, + -- At this point the pretty-printing of the goal is nonsense, containing `p + q` despite + -- the fact there is no obvious `has_add (multiplicative G)`. + simp only [←to_add_mul], + refl, }, + ..finsupp.dom_congr multiplicative.to_add } + +/-- The equivalence between `monoid_algebra` and `add_monoid_algebra` in terms of `additive` -/ +protected def monoid_algebra.to_additive [semiring k] [monoid G] : + monoid_algebra k G ≃+* add_monoid_algebra k (additive G) := +{ map_mul' := λ x y, by { + simp only [finsupp.dom_congr], + apply monoid_algebra.map_domain_mul', + intros p q, + -- At this point the pretty-printing of the goal is nonsense, containing `p + q` despite + -- the fact there is no obvious `has_mul (additive G)`. + simp only [of_mul_mul], + refl, }, + ..finsupp.dom_congr additive.of_mul } + +namespace add_monoid_algebra + +variables {k G} + /-! #### Algebra structure -/ section algebra diff --git a/src/tactic/converter/interactive.lean b/src/tactic/converter/interactive.lean index ab8c4d54cc7f5..5b6b04f0e4b49 100644 --- a/src/tactic/converter/interactive.lean +++ b/src/tactic/converter/interactive.lean @@ -112,6 +112,19 @@ We use this tactic for writing tests. meta def guard_target (p : parse texpr) : conv unit := do `(%%t = _) ← target, tactic.interactive.guard_expr_eq t p +/-- +When using `rw` in `conv` mode on conditional equality lemmas, sometimes `⊢` goals can be +introduced which are impossible to close with `conv` tactics. Note that goals like `⊢ a = 0` will +be displayed by conv mode as `| a`, making the problem difficult to diagnose at times. + +The `exact` conv tactic allows these to be closed, and is sufficient to allow re-entering tactic +mode with `exact by { ... }`. + +Discussion of how to fix `rw` in the longer term can be found in +https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212181256 +-/ +meta def exact := tactic.interactive.exact + end interactive end conv From 1ad73f06f5942a1ac04e36c59eec404881c12fd3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 14 Oct 2020 10:10:12 +0100 Subject: [PATCH 2/5] chore(*): Corrections thanks to Kevin Buzzard --- src/algebra/monoid_algebra.lean | 65 ++++++++++++--------------- src/tactic/converter/interactive.lean | 13 ------ 2 files changed, 29 insertions(+), 49 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 2ab8dbf7947fa..d3f66b9fa0779 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -193,23 +193,19 @@ lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [mo (map_domain f (x * y : monoid_algebra β α) : monoid_algebra β α₂) = (map_domain f x * map_domain f y : monoid_algebra β α₂) := begin - simp only [mul_def, map_domain_sum, map_domain_single], - -- I can't work out any way to avoid `conv` here - conv_rhs { - for (finsupp.sum _ _) [2] { - rw finsupp.sum_map_domain_index _ _, - skip, - exact λ a, by { simp, }, - exact λ a b c, by { simp [mul_add], } - }, - for (finsupp.sum _ _) [1] { - rw finsupp.sum_map_domain_index _ _, - skip, - exact λ a, by { simp, }, - exact λ a b c, by { simp [add_mul], }, - }, - }, - simp_rw f.map_mul, + simp_rw [mul_def, map_domain_sum, map_domain_single, f.map_mul], + transitivity, swap, + { rw finsupp.sum_map_domain_index, + { simp }, + { simp [add_mul] } }, + congr, + ext1, + ext1, + transitivity, swap, + { rw finsupp.sum_map_domain_index, + { simp }, + { simp [mul_add] } }, + refl, end /-- `map_domain_mul` for unbundled morphisms -/ @@ -624,23 +620,19 @@ lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := begin - simp only [mul_def, map_domain_sum, map_domain_single], - -- I can't work out any way to avoid `conv` here - conv_rhs { - for (finsupp.sum _ _) [2] { - rw finsupp.sum_map_domain_index _ _, - skip, - exact λ a, by { simp, }, - exact λ a b c, by { simp [mul_add], } - }, - for (finsupp.sum _ _) [1] { - rw finsupp.sum_map_domain_index _ _, - skip, - exact λ a, by { simp, }, - exact λ a b c, by { simp [add_mul], }, - }, - }, - simp_rw f.map_add, + simp_rw [mul_def, map_domain_sum, map_domain_single, f.map_add], + transitivity, swap, + { rw finsupp.sum_map_domain_index, + { simp }, + { simp [add_mul] } }, + congr, + ext1, + ext1, + transitivity, swap, + { rw finsupp.sum_map_domain_index, + { simp }, + { simp [mul_add] } }, + refl, end /-- `map_domain_mul` for unbundled morphisms -/ @@ -718,7 +710,8 @@ protected def add_monoid_algebra.to_multiplicative [semiring k] [add_monoid G] : -- the fact there is no obvious `has_add (multiplicative G)`. simp only [←to_add_mul], refl, }, - ..finsupp.dom_congr multiplicative.to_add } + ..finsupp.dom_congr multiplicative.of_add } + /-- The equivalence between `monoid_algebra` and `add_monoid_algebra` in terms of `additive` -/ protected def monoid_algebra.to_additive [semiring k] [monoid G] : @@ -727,7 +720,7 @@ protected def monoid_algebra.to_additive [semiring k] [monoid G] : simp only [finsupp.dom_congr], apply monoid_algebra.map_domain_mul', intros p q, - -- At this point the pretty-printing of the goal is nonsense, containing `p + q` despite + -- At this point the pretty-printing of the goal is nonsense, containing `p * q` despite -- the fact there is no obvious `has_mul (additive G)`. simp only [of_mul_mul], refl, }, diff --git a/src/tactic/converter/interactive.lean b/src/tactic/converter/interactive.lean index 5b6b04f0e4b49..ab8c4d54cc7f5 100644 --- a/src/tactic/converter/interactive.lean +++ b/src/tactic/converter/interactive.lean @@ -112,19 +112,6 @@ We use this tactic for writing tests. meta def guard_target (p : parse texpr) : conv unit := do `(%%t = _) ← target, tactic.interactive.guard_expr_eq t p -/-- -When using `rw` in `conv` mode on conditional equality lemmas, sometimes `⊢` goals can be -introduced which are impossible to close with `conv` tactics. Note that goals like `⊢ a = 0` will -be displayed by conv mode as `| a`, making the problem difficult to diagnose at times. - -The `exact` conv tactic allows these to be closed, and is sufficient to allow re-entering tactic -mode with `exact by { ... }`. - -Discussion of how to fix `rw` in the longer term can be found in -https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212181256 --/ -meta def exact := tactic.interactive.exact - end interactive end conv From ee17c59cb1c2eb49732c3eaeabad56178af94d85 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 20 Oct 2020 15:42:21 +0100 Subject: [PATCH 3/5] Apply suggestions from code review Co-authored-by: Kevin Buzzard --- src/algebra/monoid_algebra.lean | 32 ++++++++++++-------------------- 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index bce0d537dd637..d2a1e69e126ff 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -204,18 +204,14 @@ lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [mo (map_domain f x * map_domain f y : monoid_algebra β α₂) := begin simp_rw [mul_def, map_domain_sum, map_domain_single, f.map_mul], - transitivity, swap, - { rw finsupp.sum_map_domain_index, - { simp }, - { simp [add_mul] } }, - congr, - ext1, - ext1, - transitivity, swap, - { rw finsupp.sum_map_domain_index, + rw finsupp.sum_map_domain_index, + { congr, + ext a b, + rw finsupp.sum_map_domain_index, { simp }, { simp [mul_add] } }, - refl, + { simp }, + { simp [add_mul] } end /-- `map_domain_mul` for unbundled morphisms -/ @@ -656,18 +652,14 @@ lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := begin simp_rw [mul_def, map_domain_sum, map_domain_single, f.map_add], - transitivity, swap, - { rw finsupp.sum_map_domain_index, - { simp }, - { simp [add_mul] } }, - congr, - ext1, - ext1, - transitivity, swap, - { rw finsupp.sum_map_domain_index, + rw finsupp.sum_map_domain_index, + { congr, + ext a b, + rw finsupp.sum_map_domain_index, { simp }, { simp [mul_add] } }, - refl, + { simp }, + { simp [add_mul] } end /-- `map_domain_mul` for unbundled morphisms -/ From 10d9b11f3d26a5a5e5b668882c0184c1816ee1cc Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 23 Oct 2020 06:35:44 +0000 Subject: [PATCH 4/5] golf --- src/algebra/monoid_algebra.lean | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index d2a1e69e126ff..ec9f001374780 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -646,8 +646,8 @@ lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} : /-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/ lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} - [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α} - (f : add_hom α α₂) : + [semiring β] [add_monoid α] [add_monoid α₂] + (f : add_hom α α₂) (x y : add_monoid_algebra β α) : (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := begin @@ -664,11 +664,12 @@ end /-- `map_domain_mul` for unbundled morphisms -/ lemma map_domain_mul' {α : Type*} {β : Type*} {α₂ : Type*} - [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α} - (f : α → α₂) (hf : ∀ x y, f (x + y) = f x + f y) : + [semiring β] [add_monoid α] [add_monoid α₂] + (f : α → α₂) (hf : ∀ x y, f (x + y) = f x + f y) + (x y : add_monoid_algebra β α) : (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := -map_domain_mul ⟨f, hf⟩ +map_domain_mul ⟨f, hf⟩ x y section @@ -729,17 +730,10 @@ to definitional inconveniences, we can still show the types are isomorphic. /-- The equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` -/ protected def add_monoid_algebra.to_multiplicative [semiring k] [add_monoid G] : add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) := -{ map_mul' := λ x y, by { - simp only [finsupp.dom_congr], - apply add_monoid_algebra.map_domain_mul', - intros p q, - -- At this point the pretty-printing of the goal is nonsense, containing `p + q` despite - -- the fact there is no obvious `has_add (multiplicative G)`. - simp only [←to_add_mul], - refl, }, +{ to_fun := (finsupp.dom_congr multiplicative.of_add), + map_mul' := λ x y, by convert add_monoid_algebra.map_domain_mul (add_hom.id G) x y, ..finsupp.dom_congr multiplicative.of_add } - /-- The equivalence between `monoid_algebra` and `add_monoid_algebra` in terms of `additive` -/ protected def monoid_algebra.to_additive [semiring k] [monoid G] : monoid_algebra k G ≃+* add_monoid_algebra k (additive G) := From e026b21b5ba5a91aea544a94238404d61dd9fe1e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 23 Oct 2020 13:40:26 +0100 Subject: [PATCH 5/5] chore(*): Simplify using the golfing trick --- src/algebra/monoid_algebra.lean | 30 +++--------------------------- 1 file changed, 3 insertions(+), 27 deletions(-) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index ec9f001374780..760f313d03875 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -214,13 +214,6 @@ begin { simp [add_mul] } end -/-- `map_domain_mul` for unbundled morphisms -/ -lemma map_domain_mul' {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [monoid α] [monoid α₂]{x y : monoid_algebra β α} - (f : α → α₂) (hf : ∀ x y, f (x * y) = f x * f y) : - (map_domain f (x * y : monoid_algebra β α) : monoid_algebra β α₂) = - (map_domain f x * map_domain f y : monoid_algebra β α₂) := -map_domain_mul ⟨f, hf⟩ - variables (k G) /-- Embedding of a monoid into its monoid algebra. -/ @@ -647,7 +640,7 @@ lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} : /-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/ lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [add_monoid α] [add_monoid α₂] - (f : add_hom α α₂) (x y : add_monoid_algebra β α) : + {x y : add_monoid_algebra β α} (f : add_hom α α₂) : (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := begin @@ -662,15 +655,6 @@ begin { simp [add_mul] } end -/-- `map_domain_mul` for unbundled morphisms -/ -lemma map_domain_mul' {α : Type*} {β : Type*} {α₂ : Type*} - [semiring β] [add_monoid α] [add_monoid α₂] - (f : α → α₂) (hf : ∀ x y, f (x + y) = f x + f y) - (x y : add_monoid_algebra β α) : - (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) = - (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := -map_domain_mul ⟨f, hf⟩ x y - section variables (k G) @@ -730,21 +714,13 @@ to definitional inconveniences, we can still show the types are isomorphic. /-- The equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` -/ protected def add_monoid_algebra.to_multiplicative [semiring k] [add_monoid G] : add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) := -{ to_fun := (finsupp.dom_congr multiplicative.of_add), - map_mul' := λ x y, by convert add_monoid_algebra.map_domain_mul (add_hom.id G) x y, +{ map_mul' := λ x y, by convert add_monoid_algebra.map_domain_mul (add_hom.id G), ..finsupp.dom_congr multiplicative.of_add } /-- The equivalence between `monoid_algebra` and `add_monoid_algebra` in terms of `additive` -/ protected def monoid_algebra.to_additive [semiring k] [monoid G] : monoid_algebra k G ≃+* add_monoid_algebra k (additive G) := -{ map_mul' := λ x y, by { - simp only [finsupp.dom_congr], - apply monoid_algebra.map_domain_mul', - intros p q, - -- At this point the pretty-printing of the goal is nonsense, containing `p * q` despite - -- the fact there is no obvious `has_mul (additive G)`. - simp only [of_mul_mul], - refl, }, +{ map_mul' := λ x y, by convert monoid_algebra.map_domain_mul (mul_hom.id G), ..finsupp.dom_congr additive.of_mul } namespace add_monoid_algebra