From 3c7394fe69e8fa2ac1df988b72a5fab81cd0559c Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 22 Dec 2020 03:10:42 +0000 Subject: [PATCH] fix(group_theory/*, algebra/group): [to_additive, simp] doesn't work (#5468) As explained in `algebra/group/to_additive`, `@[to_additive, simp]` doesn't work (it doesn't attach a `simp` attribute to the additive lemma), but conversely `@[simps, to_additive]` is also wrong. Along the way I also noticed that some `right_inv` (as in an inverse function) lemmas were being changed to `right_neg` by to_additive :D --- src/algebra/category/Group/basic.lean | 3 ++- src/algebra/group/hom.lean | 4 ++-- src/algebra/group/semiconj.lean | 2 +- src/algebra/ordered_monoid.lean | 17 +++++++++++++---- src/group_theory/monoid_localization.lean | 18 ++++++++++-------- src/group_theory/submonoid/operations.lean | 2 +- src/topology/algebra/monoid.lean | 8 +++++--- 7 files changed, 34 insertions(+), 20 deletions(-) diff --git a/src/algebra/category/Group/basic.lean b/src/algebra/category/Group/basic.lean index 3597a585d0c44..98801bb6033f1 100644 --- a/src/algebra/category/Group/basic.lean +++ b/src/algebra/category/Group/basic.lean @@ -60,10 +60,11 @@ instance one.unique : unique (1 : Group) := @[simp, to_additive] lemma one_apply (G H : Group) (g : G) : (1 : G ⟶ H) g = 1 := rfl -@[to_additive, ext] +@[ext, to_additive] lemma ext (G H : Group) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by { ext1, apply w } +-- should to_additive do this automatically? attribute [ext] AddGroup.ext @[to_additive has_forget_to_AddMon] diff --git a/src/algebra/group/hom.lean b/src/algebra/group/hom.lean index 3e6ae28816f4f..90994ebea1bdd 100644 --- a/src/algebra/group/hom.lean +++ b/src/algebra/group/hom.lean @@ -668,8 +668,8 @@ def eval [monoid M] [comm_monoid N] : M →* (M →* N) →* N := (monoid_hom.id lemma eval_apply [monoid M] [comm_monoid N] (x : M) (f : M →* N) : eval x f = f x := rfl /-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/ -@[simps, to_additive "Composition of additive monoid morphisms -(`add_monoid_hom.comp`) as an additive monoid morphism."] +@[to_additive "Composition of additive monoid morphisms +(`add_monoid_hom.comp`) as an additive monoid morphism.", simps] def comp_hom [monoid M] [comm_monoid N] [comm_monoid P] : (N →* P) →* (M →* N) →* (M →* P) := { to_fun := λ g, { to_fun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g }, diff --git a/src/algebra/group/semiconj.lean b/src/algebra/group/semiconj.lean index d3d2213fe6138..da73a2a73d141 100644 --- a/src/algebra/group/semiconj.lean +++ b/src/algebra/group/semiconj.lean @@ -45,7 +45,7 @@ variables {S : Type u} [semigroup S] {a b x y z x' y' : S} /-- If `a` semiconjugates `x` to `y` and `x'` to `y'`, then it semiconjugates `x * x'` to `y * y'`. -/ -@[to_additive, simp] lemma mul_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') : +@[simp, to_additive] lemma mul_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') : semiconj_by a (x * x') (y * y') := by unfold semiconj_by; assoc_rw [h.eq, h'.eq] diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean index fa93beb8126f5..20097a1b5af8c 100644 --- a/src/algebra/ordered_monoid.lean +++ b/src/algebra/ordered_monoid.lean @@ -208,14 +208,19 @@ namespace units instance [monoid α] [preorder α] : preorder (units α) := preorder.lift (coe : units α → α) -@[simp, to_additive, norm_cast] +@[simp, norm_cast, to_additive] theorem coe_le_coe [monoid α] [preorder α] {a b : units α} : (a : α) ≤ b ↔ a ≤ b := iff.rfl -@[simp, to_additive, norm_cast] +-- should `to_additive` do this? +attribute [norm_cast] add_units.coe_le_coe + +@[simp, norm_cast, to_additive] theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} : (a : α) < b ↔ a < b := iff.rfl +attribute [norm_cast] add_units.coe_lt_coe + @[to_additive] instance [monoid α] [partial_order α] : partial_order (units α) := partial_order.lift coe units.ext @@ -224,16 +229,20 @@ partial_order.lift coe units.ext instance [monoid α] [linear_order α] : linear_order (units α) := linear_order.lift coe units.ext -@[simp, to_additive, norm_cast] +@[simp, norm_cast, to_additive] theorem max_coe [monoid α] [linear_order α] {a b : units α} : (↑(max a b) : α) = max a b := by by_cases b ≤ a; simp [max, h] -@[simp, to_additive, norm_cast] +attribute [norm_cast] add_units.max_coe + +@[simp, norm_cast, to_additive] theorem min_coe [monoid α] [linear_order α] {a b : units α} : (↑(min a b) : α) = min a b := by by_cases a ≤ b; simp [min, h] +attribute [norm_cast] add_units.min_coe + end units namespace with_zero diff --git a/src/group_theory/monoid_localization.lean b/src/group_theory/monoid_localization.lean index 75741add724b5..62272387ffb01 100644 --- a/src/group_theory/monoid_localization.lean +++ b/src/group_theory/monoid_localization.lean @@ -850,11 +850,11 @@ noncomputable def mul_equiv_of_localizations ⟨f.lift k.map_units, k.lift f.map_units, f.lift_left_inverse, k.lift_left_inverse, monoid_hom.map_mul _⟩ -@[to_additive, simp] lemma mul_equiv_of_localizations_apply +@[simp, to_additive] lemma mul_equiv_of_localizations_apply {k : localization_map S P} {x} : f.mul_equiv_of_localizations k x = f.lift k.map_units x := rfl -@[to_additive, simp] lemma mul_equiv_of_localizations_symm_apply +@[simp, to_additive] lemma mul_equiv_of_localizations_symm_apply {k : localization_map S P} {x} : (f.mul_equiv_of_localizations k).symm x = k.lift f.map_units x := rfl @@ -872,7 +872,7 @@ def of_mul_equiv_of_localizations (k : N ≃* P) : localization_map S P := let ⟨x, hx⟩ := f.surj z in ⟨x, show v * k _ = k _, by rw [←hx, k.map_mul, ←hz]; refl⟩) (λ x y, k.apply_eq_iff_eq.trans f.eq_iff_exists) -@[to_additive, simp] lemma of_mul_equiv_of_localizations_apply {k : N ≃* P} (x) : +@[simp, to_additive] lemma of_mul_equiv_of_localizations_apply {k : N ≃* P} (x) : (f.of_mul_equiv_of_localizations k).to_map x = k (f.to_map x) := rfl @[to_additive] lemma of_mul_equiv_of_localizations_eq {k : N ≃* P} : @@ -890,11 +890,13 @@ k.apply_symm_apply (f.to_map x) (f.of_mul_equiv_of_localizations k).to_map x = y ↔ f.to_map x = k.symm y := k.to_equiv.eq_symm_apply.symm -@[to_additive] lemma mul_equiv_of_localizations_right_inv (k : localization_map S P) : +@[to_additive add_equiv_of_localizations_right_inv] +lemma mul_equiv_of_localizations_right_inv (k : localization_map S P) : f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k) = k := to_map_injective $ f.lift_comp k.map_units -@[to_additive, simp] lemma mul_equiv_of_localizations_right_inv_apply +@[to_additive add_equiv_of_localizations_right_inv_apply, simp] +lemma mul_equiv_of_localizations_right_inv_apply {k : localization_map S P} {x} : (f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k)).to_map x = k.to_map x := ext_iff.1 (f.mul_equiv_of_localizations_right_inv k) x @@ -903,7 +905,7 @@ ext_iff.1 (f.mul_equiv_of_localizations_right_inv k) x f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k) = k := mul_equiv.ext $ monoid_hom.ext_iff.1 $ f.lift_of_comp k.to_monoid_hom -@[to_additive, simp] lemma mul_equiv_of_localizations_left_inv_apply {k : N ≃* P} (x) : +@[simp, to_additive] lemma mul_equiv_of_localizations_left_inv_apply {k : N ≃* P} (x) : f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k) x = k x := by rw mul_equiv_of_localizations_left_inv @@ -937,7 +939,7 @@ let H' : S.comap k.to_monoid_hom = T := exact k.to_equiv.injective hc⟩, λ ⟨c, hc⟩, ⟨⟨k c, H ▸ set.mem_image_of_mem k c.2⟩, by erw ←k.map_mul; rw [hc, k.map_mul]; refl⟩⟩) -@[to_additive, simp] lemma of_mul_equiv_of_dom_apply +@[simp, to_additive] lemma of_mul_equiv_of_dom_apply {k : P ≃* M} (H : T.map k.to_monoid_hom = S) (x) : (f.of_mul_equiv_of_dom H).to_map x = f.to_map (k x) := rfl @@ -993,7 +995,7 @@ f.map_eq (λ y : S, H ▸ set.mem_image_of_mem j y.2) _ f.mul_equiv_of_mul_equiv k H (f.mk' x y) = k.mk' (j x) ⟨j y, H ▸ set.mem_image_of_mem j y.2⟩ := f.map_mk' (λ y : S, H ▸ set.mem_image_of_mem j y.2) _ _ -@[to_additive, simp] lemma of_mul_equiv_of_mul_equiv_apply +@[simp, to_additive] lemma of_mul_equiv_of_mul_equiv_apply {k : localization_map T Q} {j : M ≃* P} (H : S.map j.to_monoid_hom = T) (x) : (f.of_mul_equiv_of_localizations (f.mul_equiv_of_mul_equiv k H)).to_map x = k.to_map (j x) := ext_iff.1 (f.mul_equiv_of_localizations_right_inv (k.of_mul_equiv_of_dom H)) x diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean index b3ce61276f299..f906f0297a552 100644 --- a/src/group_theory/submonoid/operations.lean +++ b/src/group_theory/submonoid/operations.lean @@ -129,7 +129,7 @@ lemma comap_comap (S : submonoid P) (g : N →* P) (f : M →* N) : (S.comap g).comap f = S.comap (g.comp f) := rfl -@[to_additive, simp] +@[simp, to_additive] lemma comap_id (S : submonoid P) : S.comap (monoid_hom.id _) = S := ext (by simp) diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean index a78708b8bcaa4..653702484e344 100644 --- a/src/topology/algebra/monoid.lean +++ b/src/topology/algebra/monoid.lean @@ -42,12 +42,13 @@ variables [topological_space M] [has_mul M] [has_continuous_mul M] lemma continuous_mul : continuous (λp:M×M, p.1 * p.2) := has_continuous_mul.continuous_mul -@[to_additive, continuity] +@[continuity, to_additive] lemma continuous.mul [topological_space α] {f : α → M} {g : α → M} (hf : continuous f) (hg : continuous g) : continuous (λx, f x * g x) := continuous_mul.comp (hf.prod_mk hg : _) +-- should `to_additive` be doing this? attribute [continuity] continuous.add @[to_additive] @@ -101,7 +102,7 @@ instance [topological_space N] [has_mul N] [has_continuous_mul N] : has_continuo ⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prod_mk ((continuous_snd.comp continuous_fst).mul (continuous_snd.comp continuous_snd))⟩ -@[to_additive, priority 100] +@[priority 100, to_additive] instance has_continuous_mul_of_discrete_topology [topological_space N] [has_mul N] [discrete_topology N] : has_continuous_mul N := ⟨continuous_of_discrete_topology⟩ @@ -247,11 +248,12 @@ by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l } attribute [continuity] continuous_multiset_sum -@[to_additive, continuity] +@[continuity, to_additive] lemma continuous_finset_prod [topological_space α] {f : β → α → M} (s : finset β) : (∀c∈s, continuous (f c)) → continuous (λa, ∏ c in s, f c a) := continuous_multiset_prod _ +-- should `to_additive` be doing this? attribute [continuity] continuous_finset_sum end