From 5c5703c2fc697da61be3816250ca2350011c1558 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 24 Mar 2023 17:48:27 +0000 Subject: [PATCH] feat: Missing opposite instances (#2940) Match https://github.com/leanprover-community/mathlib/pull/18602 Co-authored-by: Eric Wieser --- Mathlib/Algebra/Field/Opposite.lean | 34 +++++++++++++-- Mathlib/Algebra/Group/Opposite.lean | 66 ++++++++++++++++++++++++----- Mathlib/Algebra/Ring/Defs.lean | 2 +- Mathlib/Algebra/Ring/Opposite.lean | 12 +++--- Mathlib/Data/Int/Cast/Defs.lean | 6 ++- Mathlib/Data/Int/Cast/Lemmas.lean | 18 +------- Mathlib/Data/Nat/Cast/Basic.lean | 18 +------- Mathlib/Data/Rat/Cast.lean | 20 +-------- 8 files changed, 102 insertions(+), 74 deletions(-) diff --git a/Mathlib/Algebra/Field/Opposite.lean b/Mathlib/Algebra/Field/Opposite.lean index 9a407690dc134..4f1e1f7a7b785 100644 --- a/Mathlib/Algebra/Field/Opposite.lean +++ b/Mathlib/Algebra/Field/Opposite.lean @@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau ! This file was ported from Lean 3 source module algebra.field.opposite -! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9 +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ import Mathlib.Algebra.Field.Defs import Mathlib.Algebra.Ring.Opposite +import Mathlib.Data.Int.Cast.Lemmas /-! # Field structure on the multiplicative/additive opposite @@ -19,11 +20,34 @@ namespace MulOpposite variable (α : Type _) +@[to_additive] +instance ratCast [RatCast α] : RatCast αᵐᵒᵖ := + ⟨fun n => op n⟩ + +variable {α} + +@[to_additive (attr := simp, norm_cast)] +theorem op_ratCast [RatCast α] (q : ℚ) : op (q : α) = q := + rfl +#align mul_opposite.op_rat_cast MulOpposite.op_ratCast +#align add_opposite.op_rat_cast AddOpposite.op_ratCast + +@[to_additive (attr := simp, norm_cast)] +theorem unop_ratCast [RatCast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q := + rfl +#align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast +#align add_opposite.unop_rat_cast AddOpposite.unop_ratCast + +variable (α) + instance divisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ := { MulOpposite.groupWithZero α, MulOpposite.semiring α with } instance divisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ := - { MulOpposite.groupWithZero α, MulOpposite.ring α with } + { MulOpposite.divisionSemiring α, MulOpposite.ring α, MulOpposite.ratCast α with + ratCast_mk := fun a b hb h => unop_injective $ by + rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast, + Int.commute_cast, div_eq_mul_inv] } instance semifield [Semifield α] : Semifield αᵐᵒᵖ := { MulOpposite.divisionSemiring α, MulOpposite.commSemiring α with } @@ -39,7 +63,11 @@ instance divisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ : { AddOpposite.groupWithZero α, AddOpposite.semiring α with } instance divisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ := - { AddOpposite.groupWithZero α, AddOpposite.ring α with } + { -- porting note: added `ratCast` override + AddOpposite.groupWithZero α, AddOpposite.ring α, AddOpposite.ratCast α with + ratCast_mk := fun a b hb h => unop_injective $ by + rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast, + div_eq_mul_inv] } instance semifield [Semifield α] : Semifield αᵃᵒᵖ := { AddOpposite.divisionSemiring, AddOpposite.commSemiring α with } diff --git a/Mathlib/Algebra/Group/Opposite.lean b/Mathlib/Algebra/Group/Opposite.lean index 1dc4c7c734b1a..72e82ec41551c 100644 --- a/Mathlib/Algebra/Group/Opposite.lean +++ b/Mathlib/Algebra/Group/Opposite.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau ! This file was ported from Lean 3 source module algebra.group.opposite -! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94 +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -29,6 +29,13 @@ namespace MulOpposite ### Additive structures on `αᵐᵒᵖ` -/ +@[to_additive] +instance natCast [NatCast α] : NatCast αᵐᵒᵖ := + ⟨fun n => op n⟩ + +@[to_additive] +instance intCast [IntCast α] : IntCast αᵐᵒᵖ := + ⟨fun n => op n⟩ instance addSemigroup [AddSemigroup α] : AddSemigroup αᵐᵒᵖ := unop_injective.addSemigroup _ fun _ _ => rfl @@ -48,14 +55,16 @@ instance addZeroClass [AddZeroClass α] : AddZeroClass αᵐᵒᵖ := instance addMonoid [AddMonoid α] : AddMonoid αᵐᵒᵖ := unop_injective.addMonoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl +instance addCommMonoid [AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ := + unop_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl + instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne αᵐᵒᵖ := - { MulOpposite.addMonoid α, MulOpposite.one α with - natCast := fun n => op n, - natCast_zero := show op ((0 : ℕ) : α) = 0 by simp, - natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ((n : ℕ) : α) + 1 by simp } + { MulOpposite.addMonoid α, MulOpposite.one α, MulOpposite.natCast _ with + natCast_zero := show op ((0 : ℕ) : α) = 0 by rw [Nat.cast_zero, op_zero] + natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ↑(n : ℕ) + 1 by simp } -instance addCommMonoid [AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ := - unop_injective.addCommMonoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl +instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵐᵒᵖ := + { MulOpposite.addMonoidWithOne α, MulOpposite.addCommMonoid α with } instance subNegMonoid [SubNegMonoid α] : SubNegMonoid αᵐᵒᵖ := unop_injective.subNegMonoid _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) @@ -65,6 +74,10 @@ instance addGroup [AddGroup α] : AddGroup αᵐᵒᵖ := unop_injective.addGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl +instance addCommGroup [AddCommGroup α] : AddCommGroup αᵐᵒᵖ := + unop_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) + (fun _ _ => rfl) fun _ _ => rfl + instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ := { MulOpposite.addMonoidWithOne α, MulOpposite.addGroup α with intCast := fun n => op n, @@ -72,9 +85,8 @@ instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ := intCast_negSucc := fun n => show op _ = op (-unop (op ((n + 1 : ℕ) : α))) by simp } -instance addCommGroup [AddCommGroup α] : AddCommGroup αᵐᵒᵖ := - unop_injective.addCommGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) - (fun _ _ => rfl) fun _ _ => rfl +instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵐᵒᵖ := + { MulOpposite.addGroupWithOne α, MulOpposite.addCommGroup α with } /-! ### Multiplicative structures on `αᵐᵒᵖ` @@ -166,6 +178,29 @@ instance commGroup [CommGroup α] : CommGroup αᵐᵒᵖ := { MulOpposite.group α, MulOpposite.commMonoid α with } variable {α} +@[to_additive (attr := simp, norm_cast)] +theorem op_natCast [NatCast α] (n : ℕ) : op (n : α) = n := + rfl +#align mul_opposite.op_nat_cast MulOpposite.op_natCast +#align add_opposite.op_nat_cast AddOpposite.op_natCast + +@[to_additive (attr := simp, norm_cast)] +theorem op_intCast [IntCast α] (n : ℤ) : op (n : α) = n := + rfl +#align mul_opposite.op_int_cast MulOpposite.op_intCast +#align add_opposite.op_int_cast AddOpposite.op_intCast + +@[to_additive (attr := simp, norm_cast)] +theorem unop_natCast [NatCast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n := + rfl +#align mul_opposite.unop_nat_cast MulOpposite.unop_natCast +#align add_opposite.unop_nat_cast AddOpposite.unop_natCast + +@[to_additive (attr := simp, norm_cast)] +theorem unop_intCast [IntCast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n := + rfl +#align mul_opposite.unop_int_cast MulOpposite.unop_intCast +#align add_opposite.unop_int_cast AddOpposite.unop_intCast @[to_additive (attr := simp)] theorem unop_div [DivInvMonoid α] (x y : αᵐᵒᵖ) : unop (x / y) = (unop y)⁻¹ * unop x := @@ -300,6 +335,17 @@ instance commGroup [CommGroup α] : CommGroup αᵃᵒᵖ := unop_injective.commGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl +-- NOTE: `addMonoidWithOne α → addMonoidWithOne αᵃᵒᵖ` does not hold +instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵃᵒᵖ := + { AddOpposite.addCommMonoid α, AddOpposite.one, AddOpposite.natCast α with + natCast_zero := show op ((0 : ℕ) : α) = 0 by rw [Nat.cast_zero, op_zero] + natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ↑(n : ℕ) + 1 by simp [add_comm] } + +instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵃᵒᵖ := + { AddOpposite.addCommMonoidWithOne α, AddOpposite.addCommGroup α, AddOpposite.intCast α with + intCast_ofNat := λ _ ↦ congr_arg op $ Int.cast_ofNat _ + intCast_negSucc := λ _ ↦ congr_arg op $ Int.cast_negSucc _ } + variable {α} /-- The function `AddOpposite.op` is a multiplicative equivalence. -/ diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean index 9bdc5e7f8b433..acc6789d56ed3 100644 --- a/Mathlib/Algebra/Ring/Defs.lean +++ b/Mathlib/Algebra/Ring/Defs.lean @@ -333,7 +333,7 @@ class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSem /-- A unital but not-necessarily-associative ring. -/ class NonAssocRing (α : Type _) extends NonUnitalNonAssocRing α, NonAssocSemiring α, - AddGroupWithOne α + AddCommGroupWithOne α #align non_assoc_ring NonAssocRing class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R diff --git a/Mathlib/Algebra/Ring/Opposite.lean b/Mathlib/Algebra/Ring/Opposite.lean index 9c72920a623eb..4023d5f1f8a33 100644 --- a/Mathlib/Algebra/Ring/Opposite.lean +++ b/Mathlib/Algebra/Ring/Opposite.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau ! This file was ported from Lean 3 source module algebra.ring.opposite -! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -130,8 +130,8 @@ instance nonUnitalSemiring [NonUnitalSemiring α] : NonUnitalSemiring αᵃᵒ { AddOpposite.semigroupWithZero α, AddOpposite.nonUnitalNonAssocSemiring α with } instance nonAssocSemiring [NonAssocSemiring α] : NonAssocSemiring αᵃᵒᵖ := - { AddOpposite.mulZeroOneClass α, - AddOpposite.nonUnitalNonAssocSemiring α with } + { AddOpposite.mulZeroOneClass α, AddOpposite.nonUnitalNonAssocSemiring α, + AddOpposite.addCommMonoidWithOne _ with } instance semiring [Semiring α] : Semiring αᵃᵒᵖ := { AddOpposite.nonUnitalSemiring α, AddOpposite.nonAssocSemiring α, @@ -149,11 +149,13 @@ instance nonUnitalNonAssocRing [NonUnitalNonAssocRing α] : NonUnitalNonAssocRin instance nonUnitalRing [NonUnitalRing α] : NonUnitalRing αᵃᵒᵖ := { AddOpposite.addCommGroup α, AddOpposite.semigroupWithZero α, AddOpposite.distrib α with } +-- porting note: added missing `addCommGroupWithOne` inheritance instance nonAssocRing [NonAssocRing α] : NonAssocRing αᵃᵒᵖ := - { AddOpposite.addCommGroup α, AddOpposite.mulZeroOneClass α, AddOpposite.distrib α with } + { AddOpposite.addCommGroupWithOne α, AddOpposite.mulZeroOneClass α, AddOpposite.distrib α with } +-- porting note: added missing `addCommGroupWithOne` inheritance instance ring [Ring α] : Ring αᵃᵒᵖ := - { AddOpposite.addCommGroup α, AddOpposite.monoid α, AddOpposite.semiring α with } + { AddOpposite.addCommGroupWithOne α, AddOpposite.monoid α, AddOpposite.semiring α with } instance nonUnitalCommRing [NonUnitalCommRing α] : NonUnitalCommRing αᵃᵒᵖ := { AddOpposite.nonUnitalRing α, AddOpposite.nonUnitalCommSemiring α with } diff --git a/Mathlib/Data/Int/Cast/Defs.lean b/Mathlib/Data/Int/Cast/Defs.lean index 123ea72b079c7..238079af880a2 100644 --- a/Mathlib/Data/Int/Cast/Defs.lean +++ b/Mathlib/Data/Int/Cast/Defs.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Gabriel Ebner ! This file was ported from Lean 3 source module data.int.cast.defs -! leanprover-community/mathlib commit 99e8971dc62f1f7ecf693d75e75fbbabd55849de +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -60,9 +60,11 @@ class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGro #align add_group_with_one.int_cast_neg_succ_of_nat AddGroupWithOne.intCast_negSucc /-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/ -class AddCommGroupWithOne (R : Type u) extends AddCommGroup R, AddGroupWithOne R +class AddCommGroupWithOne (R : Type u) + extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R #align add_comm_group_with_one AddCommGroupWithOne #align add_comm_group_with_one.to_add_comm_group AddCommGroupWithOne.toAddCommGroup #align add_comm_group_with_one.to_add_group_with_one AddCommGroupWithOne.toAddGroupWithOne +#align add_comm_group_with_one.to_add_comm_monoid_with_one AddCommGroupWithOne.toAddCommMonoidWithOne open Nat diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean index 524ba3a4ddd02..f781a915ddabe 100644 --- a/Mathlib/Data/Int/Cast/Lemmas.lean +++ b/Mathlib/Data/Int/Cast/Lemmas.lean @@ -5,7 +5,7 @@ Authors: Mario Carneiro Ported by: Scott Morrison ! This file was ported from Lean 3 source module data.int.cast.lemmas -! leanprover-community/mathlib commit 7a89b1aed52bcacbcc4a8ad515e72c5c07268940 +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -368,22 +368,6 @@ theorem Sum.elim_intCast_intCast {α β γ : Type _} [IntCast γ] (n : ℤ) : @Sum.elim_lam_const_lam_const α β γ n #align sum.elim_int_cast_int_cast Sum.elim_intCast_intCast -namespace MulOpposite - -variable [AddGroupWithOne α] - -@[simp, norm_cast] -theorem op_intCast (z : ℤ) : op (z : α) = z := - rfl -#align mul_opposite.op_int_cast MulOpposite.op_intCast - -@[simp, norm_cast] -theorem unop_intCast (n : ℤ) : unop (n : αᵐᵒᵖ) = n := - rfl -#align mul_opposite.unop_int_cast MulOpposite.unop_intCast - -end MulOpposite - /-! ### Order dual -/ diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean index 6a06845ba56ac..4a51a9c115bb5 100644 --- a/Mathlib/Data/Nat/Cast/Basic.lean +++ b/Mathlib/Data/Nat/Cast/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro ! This file was ported from Lean 3 source module data.nat.cast.basic -! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -297,22 +297,6 @@ instance Nat.uniqueRingHom {R : Type _} [NonAssocSemiring R] : Unique (ℕ →+* default := Nat.castRingHom R uniq := RingHom.eq_natCast' -namespace MulOpposite - -variable [AddMonoidWithOne α] - -@[simp, norm_cast] -theorem op_natCast (n : ℕ) : op (n : α) = n := - rfl -#align mul_opposite.op_nat_cast MulOpposite.op_natCast - -@[simp, norm_cast] -theorem unop_natCast (n : ℕ) : unop (n : αᵐᵒᵖ) = n := - rfl -#align mul_opposite.unop_nat_cast MulOpposite.unop_natCast - -end MulOpposite - namespace Pi variable {π : α → Type _} [∀ a, NatCast (π a)] diff --git a/Mathlib/Data/Rat/Cast.lean b/Mathlib/Data/Rat/Cast.lean index 1379c8c442931..17b8ea4a2609a 100644 --- a/Mathlib/Data/Rat/Cast.lean +++ b/Mathlib/Data/Rat/Cast.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro ! This file was ported from Lean 3 source module data.rat.cast -! leanprover-community/mathlib commit 422e70f7ce183d2900c586a8cda8381e788a0c62 +! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -499,24 +499,6 @@ instance Rat.subsingleton_ringHom {R : Type _} [Semiring R] : Subsingleton (ℚ ⟨RingHom.ext_rat⟩ #align rat.subsingleton_ring_hom Rat.subsingleton_ringHom -namespace MulOpposite - -variable [DivisionRing α] - -@[simp, norm_cast] -theorem op_ratCast (r : ℚ) : op (r : α) = (↑r : αᵐᵒᵖ) := by - rw [cast_def, div_eq_mul_inv, op_mul, op_inv, op_natCast, op_intCast, - (Commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv] -#align mul_opposite.op_rat_cast MulOpposite.op_ratCast - -@[simp, norm_cast] -theorem unop_ratCast (r : ℚ) : unop (r : αᵐᵒᵖ) = r := by - rw [cast_def, div_eq_mul_inv, unop_mul, unop_inv, unop_natCast, unop_intCast, - (Commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv] -#align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast - -end MulOpposite - section SMul namespace Rat