Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - refactor: drop some *HomClasses #10544

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - refactor: drop some *HomClasses #10544

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2dce925
refactor: drop some `*HomClass`es
urkud Feb 14, 2024
2d5f46c
Docs
urkud Feb 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 44 additions & 78 deletions Mathlib/Algebra/Order/Hom/Monoid.lean
View file
Open in desktop
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) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a bit weird to put this in the OrderMonoidHomClass namespace given that such a class doesn't exist anymore, but I don't have a better suggestion.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How about

Suggested change
def OrderMonoidHomClass.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) :
def FunLike.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) :

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let me do it for all bundled homs at once.

α →*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
Open in desktop
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
Loading