Skip to content

Commit

Permalink
refactor: drop some *HomClasses (#10544)
Browse files Browse the repository at this point in the history 
Drop classes that mix `OrderHomClass` with algebraic hom classes.
  • Loading branch information
@urkud @riccardobrasca
urkud authored and riccardobrasca committed Feb 18, 2024
1 parent 7eac0dc commit ed9cb5f
Show file tree
Hide file tree
Showing 2 changed files with 80 additions and 156 deletions.
122 changes: 44 additions & 78 deletions Mathlib/Algebra/Order/Hom/Monoid.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,6 @@ This file defines morphisms between (additive) ordered monoids.
* `OrderMonoidHom`: Ordered monoid homomorphisms.
* `OrderMonoidWithZeroHom`: Ordered monoid with zero homomorphisms.
## Typeclasses
* `OrderAddMonoidHomClass`
* `OrderMonoidHomClass`
* `OrderMonoidWithZeroHomClass`
## Notation
* `→+o`: Bundled ordered additive monoid homs. Also use for additive groups homs.
Expand All @@ -48,6 +42,15 @@ Implicit `{}` brackets are often used instead of type class `[]` brackets. This
instances can be inferred because they are implicit arguments to the type `OrderMonoidHom`. When
they can be inferred from the type it is faster to use this method than to use type class inference.
### Removed typeclasses
This file used to define typeclasses for order-preserving (additive) monoid homomorphisms:
`OrderAddMonoidHomClass`, `OrderMonoidHomClass`, and `OrderMonoidWithZeroHomClass`.
In #10544 we migrated from these typeclasses
to assumptions like `[FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N ]`,
making some definitions and lemmas irrelevant.
## Tags
ordered monoid, ordered group, monoid with zero
Expand Down Expand Up @@ -78,19 +81,6 @@ structure OrderAddMonoidHom (α β : Type*) [Preorder α] [Preorder β] [AddZero
/-- Infix notation for `OrderAddMonoidHom`. -/
infixr:25 " →+o " => OrderAddMonoidHom

section

/-- `OrderAddMonoidHomClass F α β` states that `F` is a type of ordered monoid homomorphisms.
You should also extend this typeclass when you extend `OrderAddMonoidHom`. -/
class OrderAddMonoidHomClass (F α β : Type*) [Preorder α] [Preorder β]
[AddZeroClass α] [AddZeroClass β] [FunLike F α β] extends AddMonoidHomClass F α β : Prop where
/-- An `OrderAddMonoidHom` is a monotone function. -/
monotone (f : F) : Monotone f
#align order_add_monoid_hom_class OrderAddMonoidHomClass

end

-- Instances and lemmas are defined below through `@[to_additive]`.
end AddMonoid

Expand All @@ -114,43 +104,22 @@ structure OrderMonoidHom (α β : Type*) [Preorder α] [Preorder β] [MulOneClas
/-- Infix notation for `OrderMonoidHom`. -/
infixr:25 " →*o " => OrderMonoidHom

section

/-- `OrderMonoidHomClass F α β` states that `F` is a type of ordered monoid homomorphisms.
You should also extend this typeclass when you extend `OrderMonoidHom`. -/
@[to_additive]
class OrderMonoidHomClass (F α β : Type*) [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β]
[FunLike F α β] extends MonoidHomClass F α β : Prop where
/-- An `OrderMonoidHom` is a monotone function. -/
monotone (f : F) : Monotone f
#align order_monoid_hom_class OrderMonoidHomClass

end

variable [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [FunLike F α β]

/-- Turn an element of a type `F` satisfying `OrderMonoidHomClass F α β` into an actual
`OrderMonoidHom`. This is declared as the default coercion from `F` to `α →*o β`. -/
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `MonoidHomClass F α β`
into an actual `OrderMonoidHom`. This is declared as the default coercion from `F` to `α →*o β`. -/
@[to_additive (attr := coe)
"Turn an element of a type `F` satisfying `OrderAddMonoidHomClass F α β` into an actual
`OrderAddMonoidHom`. This is declared as the default coercion from `F` to `α →+o β`."]
def OrderMonoidHomClass.toOrderMonoidHom [OrderMonoidHomClass F α β] (f : F) : α →*o β :=
{ (f : α →* β) with monotone' := monotone f }

-- See note [lower instance priority]
@[to_additive]
instance (priority := 100) OrderMonoidHomClass.toOrderHomClass [OrderMonoidHomClass F α β] :
OrderHomClass F α β :=
{ ‹OrderMonoidHomClass F α β› with map_rel := OrderMonoidHomClass.monotone }
#align order_monoid_hom_class.to_order_hom_class OrderMonoidHomClass.toOrderHomClass
#align order_add_monoid_hom_class.to_order_hom_class OrderAddMonoidHomClass.toOrderHomClass
def OrderMonoidHomClass.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) :
α →*o β :=
{ (f : α →* β) with monotone' := OrderHomClass.monotone f }

/-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
`OrderMonoidHomClass.toOrderMonoidHom`. -/
@[to_additive "Any type satisfying `OrderAddMonoidHomClass` can be cast into `OrderAddMonoidHom` via
`OrderAddMonoidHomClass.toOrderAddMonoidHom`"]
instance [OrderMonoidHomClass F α β] : CoeTC F (α →*o β) :=
instance [OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β) :=
⟨OrderMonoidHomClass.toOrderMonoidHom⟩

end Monoid
Expand Down Expand Up @@ -179,47 +148,31 @@ infixr:25 " →*₀o " => OrderMonoidWithZeroHom

section

/-- `OrderMonoidWithZeroHomClass F α β` states that `F` is a type of
ordered monoid with zero homomorphisms.
You should also extend this typeclass when you extend `OrderMonoidWithZeroHom`. -/
class OrderMonoidWithZeroHomClass (F α β : Type*) [Preorder α] [Preorder β]
[MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β]
extends MonoidWithZeroHomClass F α β : Prop where
/-- An `OrderMonoidWithZeroHom` is a monotone function. -/
monotone (f : F) : Monotone f
#align order_monoid_with_zero_hom_class OrderMonoidWithZeroHomClass

variable [FunLike F α β]

/-- Turn an element of a type `F` satisfying `OrderMonoidWithZeroHomClass F α β` into an actual
`OrderMonoidWithZeroHom`. This is declared as the default coercion from `F` to `α →+*₀o β`. -/
/-- Turn an element of a type `F`
satisfying `OrderHomClass F α β` and `MonoidWithZeroHomClass F α β`
into an actual `OrderMonoidWithZeroHom`.
This is declared as the default coercion from `F` to `α →+*₀o β`. -/
@[coe]
def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom [OrderMonoidWithZeroHomClass F α β]
(f : F) : α →*₀o β :=
{ (f : α →*₀ β) with monotone' := monotone f }
def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom [OrderHomClass F α β]
[MonoidWithZeroHomClass F α β] (f : F) : α →*₀o β :=
{ (f : α →*₀ β) with monotone' := OrderHomClass.monotone f }

end

variable [FunLike F α β]

-- See note [lower instance priority]
instance (priority := 100) OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
{_ : Preorder α} {_ : Preorder β} {_ : MulZeroOneClass α} {_ : MulZeroOneClass β}
[OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β :=
{ ‹OrderMonoidWithZeroHomClass F α β› with }
#align order_monoid_with_zero_hom_class.to_order_monoid_hom_class OrderMonoidWithZeroHomClass.toOrderMonoidHomClass

instance [OrderMonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) :=
instance [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) :=
⟨OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom⟩

end MonoidWithZero

section OrderedAddCommMonoid
section OrderedZero

variable [FunLike F α β]
variable [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [OrderAddMonoidHomClass F α β] (f : F)
{a : α}
variable [Preorder α] [Zero α] [Preorder β] [Zero β] [OrderHomClass F α β]
[ZeroHomClass F α β] (f : F) {a : α}

/-- See also `NonnegHomClass.apply_nonneg`. -/
theorem map_nonneg (ha : 0 ≤ a) : 0 ≤ f a := by
Expand All @@ -232,7 +185,7 @@ theorem map_nonpos (ha : a ≤ 0) : f a ≤ 0 := by
exact OrderHomClass.mono _ ha
#align map_nonpos map_nonpos

end OrderedAddCommMonoid
end OrderedZero

section OrderedAddCommGroup

Expand Down Expand Up @@ -299,10 +252,13 @@ instance : FunLike (α →*o β) α β where
congr

@[to_additive]
instance : OrderMonoidHomClass (α →*o β) α β where
instance : OrderHomClass (α →*o β) α β where
map_rel f _ _ h := f.monotone' h

@[to_additive]
instance : MonoidHomClass (α →*o β) α β where
map_mul f := f.map_mul'
map_one f := f.map_one'
monotone f := f.monotone'

-- Other lemmas should be accessed through the `FunLike` API
@[to_additive (attr := ext)]
Expand Down Expand Up @@ -586,11 +542,13 @@ instance : FunLike (α →*₀o β) α β where
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
congr

instance : OrderMonoidWithZeroHomClass (α →*₀o β) α β where
instance : MonoidWithZeroHomClass (α →*₀o β) α β where
map_mul f := f.map_mul'
map_one f := f.map_one'
map_zero f := f.map_zero'
monotone f := f.monotone'

instance : OrderHomClass (α →*₀o β) α β where
map_rel f _ _ h := f.monotone' h

-- Other lemmas should be accessed through the `FunLike` API
@[ext]
Expand Down Expand Up @@ -766,3 +724,11 @@ theorem toOrderMonoidHom_eq_coe (f : α →*₀o β) : f.toOrderMonoidHom = f :=
end LinearOrderedCommMonoidWithZero

end OrderMonoidWithZeroHom

/- See module docstring for details. -/
#noalign order_add_monoid_hom_class
#noalign order_monoid_hom_class
#noalign order_monoid_hom_class.to_order_hom_class
#noalign order_add_monoid_hom_class.to_order_hom_class
#noalign order_monoid_with_zero_hom_class
#noalign order_monoid_with_zero_hom_class.to_order_monoid_hom_class
114 changes: 36 additions & 78 deletions Mathlib/Algebra/Order/Hom/Ring.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,13 @@ Homomorphisms between ordered (semi)rings that respect the ordering.
* `→+*o`: Ordered ring homomorphisms.
* `≃+*o`: Ordered ring isomorphisms.
## Implementation notes
This file used to define typeclasses for order-preserving ring homomorphisms and isomorphisms.
In #10544, we migrated from assumptions like `[FunLike F R S] [OrderRingHomClass F R S]`
to assumptions like `[FunLike F R S] [OrderHomClass F R S] [RingHomClass F R S]`,
making some typeclasses and instances irrelevant.
## Tags
ordered ring homomorphism, order homomorphism
Expand Down Expand Up @@ -75,80 +82,30 @@ structure OrderRingIso (α β : Type*) [Mul α] [Mul β] [Add α] [Add β] [LE
@[inherit_doc]
infixl:25 " ≃+*o " => OrderRingIso

/-- `OrderRingHomClass F α β` states that `F` is a type of ordered semiring homomorphisms.
You should extend this typeclass when you extend `OrderRingHom`. -/
class OrderRingHomClass (F : Type*) (α β : outParam <| Type*) [NonAssocSemiring α] [Preorder α]
[NonAssocSemiring β] [Preorder β] [FunLike F α β] extends RingHomClass F α β : Prop where
/-- The proposition that the function preserves the order. -/
monotone (f : F) : Monotone f
#align order_ring_hom_class OrderRingHomClass

/-- `OrderRingIsoClass F α β` states that `F` is a type of ordered semiring isomorphisms.
You should extend this class when you extend `OrderRingIso`. -/
class OrderRingIsoClass (F : Type*) (α β : outParam (Type*)) [Mul α] [Add α] [LE α] [Mul β]
[Add β] [LE β] [EquivLike F α β] extends RingEquivClass F α β : Prop where
/-- The proposition that the function preserves the order bijectively. -/
map_le_map_iff (f : F) {a b : α} : f a ≤ f b ↔ a ≤ b
#align order_ring_iso_class OrderRingIsoClass
-- See module docstring for details
#noalign order_ring_hom_class
#noalign order_ring_iso_class
#noalign order_ring_hom_class.to_order_add_monoid_hom_class
#noalign order_ring_hom_class.to_order_monoid_with_zero_hom_class
#noalign order_ring_iso_class.to_order_iso_class
#noalign order_ring_iso_class.to_order_ring_hom_class

section Hom

variable [FunLike F α β]

-- See note [lower priority instance]
instance (priority := 100) OrderRingHomClass.toOrderAddMonoidHomClass [NonAssocSemiring α]
[Preorder α] [NonAssocSemiring β] [Preorder β] [OrderRingHomClass F α β] :
OrderAddMonoidHomClass F α β :=
{ ‹OrderRingHomClass F α β› with }
#align order_ring_hom_class.to_order_add_monoid_hom_class OrderRingHomClass.toOrderAddMonoidHomClass

-- See note [lower priority instance]
instance (priority := 100) OrderRingHomClass.toOrderMonoidWithZeroHomClass [NonAssocSemiring α]
[Preorder α] [NonAssocSemiring β] [Preorder β] [OrderRingHomClass F α β] :
OrderMonoidWithZeroHomClass F α β :=
{ ‹OrderRingHomClass F α β› with }
#align order_ring_hom_class.to_order_monoid_with_zero_hom_class OrderRingHomClass.toOrderMonoidWithZeroHomClass

end Hom

section Equiv

variable [EquivLike F α β]

-- See note [lower instance priority]
instance (priority := 100) OrderRingIsoClass.toOrderIsoClass [Mul α] [Add α] [LE α]
[Mul β] [Add β] [LE β] [OrderRingIsoClass F α β] : OrderIsoClass F α β :=
{ ‹OrderRingIsoClass F α β› with }
#align order_ring_iso_class.to_order_iso_class OrderRingIsoClass.toOrderIsoClass

-- See note [lower instance priority]
instance (priority := 100) OrderRingIsoClass.toOrderRingHomClass [NonAssocSemiring α]
[Preorder α] [NonAssocSemiring β] [Preorder β] [OrderRingIsoClass F α β] :
OrderRingHomClass F α β :=
{ monotone := fun f _ _ => (map_le_map_iff f).2
-- porting note: used to be the following which times out
--‹OrderRingIsoClass F α β› with monotone := fun f => OrderHomClass.mono f
}
#align order_ring_iso_class.to_order_ring_hom_class OrderRingIsoClass.toOrderRingHomClass

end Equiv

section Hom

variable [FunLike F α β]

-- porting note: OrderRingHomClass.toOrderRingHom is new
/-- Turn an element of a type `F` satisfying `OrderRingHomClass F α β` into an actual
`OrderRingHom`. This is declared as the default coercion from `F` to `α →+*o β`. -/
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `RingHomClass F α β`
into an actual `OrderRingHom`.
This is declared as the default coercion from `F` to `α →+*o β`. -/
@[coe]
def OrderRingHomClass.toOrderRingHom [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β]
[Preorder β] [OrderRingHomClass F α β] (f : F) : α →+*o β :=
{ (f : α →+* β) with monotone' := monotone f}
[Preorder β] [OrderHomClass F α β] [RingHomClass F α β] (f : F) : α →+*o β :=
{ (f : α →+* β) with monotone' := OrderHomClass.monotone f}

/-- Any type satisfying `OrderRingHomClass` can be cast into `OrderRingHom` via
`OrderRingHomClass.toOrderRingHom`. -/
instance [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β]
[OrderRingHomClass F α β] : CoeTC F (α →+*o β) :=
[OrderHomClass F α β] [RingHomClass F α β] : CoeTC F (α →+*o β) :=
⟨OrderRingHomClass.toOrderRingHom⟩

end Hom
Expand All @@ -157,18 +114,18 @@ section Equiv

variable [EquivLike F α β]

-- porting note: OrderRingIsoClass.toOrderRingIso is new
/-- Turn an element of a type `F` satisfying `OrderRingIsoClass F α β` into an actual
`OrderRingIso`. This is declared as the default coercion from `F` to `α ≃+*o β`. -/
/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `RingEquivClass F α β`
into an actual `OrderRingIso`.
This is declared as the default coercion from `F` to `α ≃+*o β`. -/
@[coe]
def OrderRingIsoClass.toOrderRingIso [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β]
[OrderRingIsoClass F α β] (f : F) : α ≃+*o β :=
[OrderIsoClass F α β] [RingEquivClass F α β] (f : F) : α ≃+*o β :=
{ (f : α ≃+* β) with map_le_map_iff' := map_le_map_iff f}

/-- Any type satisfying `OrderRingIsoClass` can be cast into `OrderRingIso` via
`OrderRingIsoClass.toOrderRingIso`. -/
instance [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderRingIsoClass F α β] :
CoeTC F (α ≃+*o β) :=
instance [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β]
[RingEquivClass F α β] : CoeTC F (α ≃+*o β) :=
⟨OrderRingIsoClass.toOrderRingIso⟩

end Equiv
Expand All @@ -194,21 +151,21 @@ def toOrderMonoidWithZeroHom (f : α →+*o β) : α →*₀o β :=
{ f with }
#align order_ring_hom.to_order_monoid_with_zero_hom OrderRingHom.toOrderMonoidWithZeroHom

instance : FunLike (α →+*o β) α β
where
instance : FunLike (α →+*o β) α β where
coe f := f.toFun
coe_injective' f g h := by
obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr
-- porting note: needed to add the following line
exact DFunLike.coe_injective' h

instance : OrderRingHomClass (α →+*o β) α β
where
instance : OrderHomClass (α →+*o β) α β where
map_rel f _ _ h := f.monotone' h

instance : RingHomClass (α →+*o β) α β where
map_mul f := f.map_mul'
map_one f := f.map_one'
map_add f := f.map_add'
map_zero f := f.map_zero'
monotone f := f.monotone'

theorem toFun_eq_coe (f : α →+*o β) : f.toFun = f :=
rfl
Expand Down Expand Up @@ -398,12 +355,13 @@ instance : EquivLike (α ≃+*o β) α β
left_inv f := f.left_inv
right_inv f := f.right_inv

instance : OrderRingIsoClass (α ≃+*o β) α β
where
map_add f := f.map_add'
map_mul f := f.map_mul'
instance : OrderIsoClass (α ≃+*o β) α β where
map_le_map_iff f _ _ := f.map_le_map_iff'

instance : RingEquivClass (α ≃+*o β) α β where
map_mul f := f.map_mul'
map_add f := f.map_add'

theorem toFun_eq_coe (f : α ≃+*o β) : f.toFun = f :=
rfl
#align order_ring_iso.to_fun_eq_coe OrderRingIso.toFun_eq_coe
Expand Down

0 comments on commit ed9cb5f

Please sign in to comment.