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

refactor: deprecate ContinuousMonoidHomClass #17558

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

refactor: deprecate ContinuousMonoidHomClass #17558

wants to merge 2 commits into from
+42 −46

Conversation

urkud
Copy link
Member

@urkud urkud commented Oct 8, 2024 •
edited
Loading

Use [ContinuousMapClass ..] [MonoidHomClass ..] instead. Also deprecate mk' since it's defeq mk.

Open in Gitpod

@urkud
refactor: deprecate ContinuousMonoidHomClass
22af102 
Use `[ContinuousMapClass ..] [MonoidHomClass ..]` instead.
@urkud urkud added t-topology Topological spaces, uniform spaces, metric spaces, filters t-algebra Algebra (groups, rings, fields, etc) labels Oct 8, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Oct 8, 2024 •
edited
Loading

PR summary 29a5790d8c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instFunLike
++ instContinuousMapClass
++ instMonoidHomClass
- funLike
- instance (priority := 100) ContinuousMonoidHomClass.toContinuousMapClass
- instance : ContinuousMonoidHomClass (PontryaginDual A) A Circle
- toContinuousMap
--+ ContinuousMonoidHomClass

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@urkud urkud requested a review from YaelDillies October 8, 2024 22:10
@urkud
Copy link
Member Author

urkud commented Oct 8, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 22af102.
The entire run failed.
Found no significant differences.

YaelDillies
YaelDillies approved these changes Oct 9, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Now that FunLike is not extended, this makes a lot of sense.

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Oct 9, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

sgouezel
sgouezel reviewed Oct 9, 2024
View reviewed changes
Copy link
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

bors d+
Thanks!

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
@@ -30,49 +30,43 @@ variable (F A B C D E : Type*) [Monoid A] [Monoid B] [Monoid C] [Monoid D] [Comm
/-- The type of continuous additive monoid homomorphisms from `A` to `B`.
When possible, instead of parametrizing results over `(f : ContinuousAddMonoidHom A B)`,
you should parametrize over `(F : Type*) [ContinuousAddMonoidHomClass F A B] (f : F)`.
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [AddMonoidHomClass F A B] (f : F)`.
When you extend this structure, make sure to extend `ContinuousAddMonoidHomClass`. -/
Copy link
Contributor

Choose a reason for hiding this comment

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

Can you adapt the docstring to the new setting?

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
@[to_additive]
theorem toContinuousMap_injective : Injective (toContinuousMap : _ → C(A, B)) := fun f g h =>
ext <| by convert DFunLike.ext_iff.1 h

-- Porting note: Removed simps because given definition is not a constructor application
/-- Construct a `ContinuousMonoidHom` from a `Continuous` `MonoidHom`. -/
@[to_additive "Construct a `ContinuousAddMonoidHom` from a `Continuous` `AddMonoidHom`."]
@[to_additive (attr := deprecated (since := "2024-10-08"))
"Construct a `ContinuousAddMonoidHom` from a `Continuous` `AddMonoidHom`."]
def mk' (f : A →* B) (hf : Continuous f) : ContinuousMonoidHom A B :=
Copy link
Contributor

Choose a reason for hiding this comment

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

If it's defeq to something already existing, could you rather write it as a deprecated alias, to make sure that people who were using it get the suggestion to use mk instead?

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 9, 2024

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

jcommelin
jcommelin reviewed Oct 9, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 9, 2024
@jcommelin
Copy link
Member

bors r-

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 9, 2024

Canceled.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@sgouezel sgouezel sgouezel left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees
No one assigned
Labels
delegated maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@urkud @leanprover-bot @jcommelin @sgouezel @YaelDillies @leanprover-community-mathlib4-bot