Skip to content

[Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin #35807

Closed
Raph-DG wants to merge 11 commits into
leanprover-community:masterfrom
Raph-DG:Raph-DG-locallyFinSuppInstances
Closed

[Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin #35807
Raph-DG wants to merge 11 commits into
leanprover-community:masterfrom
Raph-DG:Raph-DG-locallyFinSuppInstances

Conversation

@Raph-DG

@Raph-DG Raph-DG commented Feb 26, 2026

Copy link
Copy Markdown
Collaborator

In this PR, we generalised the various instances for locally fin supp functions. These changes were originally made on the PR #26304 about algebraic cycles, but it was decided that these changes are more appropriate in their own PR.

Open in Gitpod

@Raph-DG Raph-DG mentioned this pull request Feb 26, 2026
Closed
3 tasks
@github-actions

github-actions Bot commented Feb 26, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 3e143864e8

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Function.locallyFinsupp.locallyFiniteSupport
+ addSubmonoid
+ instance [AddCommMonoid Y] : AddCommMonoid (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : AddGroup (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : SMul ℤ (locallyFinsuppWithin U Y)
+ instance [AddGroup Y] : Sub (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : Add (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : AddMonoid (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : SMul ℕ (locallyFinsuppWithin U Y)
+ instance [AddMonoid Y] : Zero (locallyFinsuppWithin U Y)
+ memAddSubmonoid
+ mk_of_mem_addSubgroup
+ mk_of_mem_addSubmonoid
- instance [AddCommGroup Y] : Add (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : Neg (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : SMul ℕ (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : SMul ℤ (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : Sub (locallyFinsuppWithin U Y)
- instance [AddCommGroup Y] : Zero (locallyFinsuppWithin U Y)

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Feb 26, 2026
dagurtomas
dagurtomas reviewed Mar 5, 2026
View reviewed changes
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
@dagurtomas dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 5, 2026
Raph-DG and others added 4 commits March 5, 2026 19:12
@Raph-DG @dagurtomas
Update Mathlib/Topology/LocallyFinsupp.lean
8989ec2 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
@Raph-DG @dagurtomas
Update Mathlib/Topology/LocallyFinsupp.lean
21cfb9b 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
@Raph-DG @dagurtomas
Update Mathlib/Topology/LocallyFinsupp.lean
077cba8 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
@Raph-DG
Made name changes consistent and added in depricated lemma
57dfffc
@Raph-DG Raph-DG removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 5, 2026
dagurtomas
dagurtomas reviewed Mar 6, 2026
View reviewed changes
Comment thread Mathlib/Topology/LocallyFinsupp.lean Outdated
@dagurtomas

dagurtomas commented Mar 12, 2026

Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions

github-actions Bot commented Mar 12, 2026

Copy link
Copy Markdown

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

trigger_name: issue_comment
wf_run: workflow_run

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 12, 2026
j-loreaux
j-loreaux reviewed Mar 12, 2026
View reviewed changes

@j-loreaux j-loreaux left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

bors merge

@mathlib-triage mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 12, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Mar 12, 2026
@Raph-DG
chore(Topology): Generalised some of the instances for Function.local…
c1a1f0d 
…lyFinsuppWithin (#35807)

In this PR, we generalised the various instances for locally fin supp functions. These changes were originally made on the PR #26304 about algebraic cycles, but it was decided that these changes are more appropriate in their own PR.

Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
@mathlib-bors

mathlib-bors Bot commented Mar 12, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin [Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin Mar 12, 2026
@mathlib-bors mathlib-bors Bot closed this Mar 12, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jun 5, 2026
@Raph-DG
feat(AlgebraicGeometry): Pushforward of algebraic cycles (#26304)
dd6fae6 
In this PR we define a notion of the "pushfoward of functions with locally finite support". We give this PR the suggestive title "pushforward of algebraic cycles" because we will go on to model algebraic cycles on a scheme X as functions from X to the integers with locally finite support. 

- [x] depends on: #26225
- [x] depends on: #26259 
- [x] depends on: #35807

Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@Raph-DG @ReemMelamed
feat(AlgebraicGeometry): Pushforward of algebraic cycles (leanprover-…
6c9edae 
…community#26304)

In this PR we define a notion of the "pushfoward of functions with locally finite support". We give this PR the suggestive title "pushforward of algebraic cycles" because we will go on to model algebraic cycles on a scheme X as functions from X to the integers with locally finite support. 

- [x] depends on: leanprover-community#26225
- [x] depends on: leanprover-community#26259 
- [x] depends on: leanprover-community#35807

Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments
@dagurtomas dagurtomas dagurtomas left review comments

Assignees

@dagurtomas dagurtomas

Labels

ready-to-merge This PR has been sent to bors. 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.

3 participants

@Raph-DG @dagurtomas @j-loreaux