feat: add `DFinsupp.mapDomain` to match `Finsupp.mapDomain` by eric-wieser · Pull Request #38977 · leanprover-community/mathlib4

eric-wieser · 2026-05-06T00:07:14Z

The API for DFinsupp.mapDomain is copied from Finsupp.mapDomain.

One motivation here is to make it easier to swap out either Basis or AddMonoidAlgebra to use DFinsupp and thus become computable.

depends on: [Merged by Bors] - feat(Data/Multiset): add the Multiset version of List.find? #40326

github-actions · 2026-05-06T00:08:32Z

PR summary a60ac7cccf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.DFinsupp.Basic` (new file)	781

Declarations diff (regex)

+ _root_.Function.Injective.subsingleton_fiber
+ embDomain
+ embDomain_apply_self
+ embDomain_eq_mapDomain
+ embDomain_notin_range
+ equivCongrLeft_symm_eq_mapDomain
+ mapDomain
+ mapDomain.addMonoidHom
+ mapDomain.addMonoidHom_apply
+ mapDomain.addMonoidHom_comp
+ mapDomain.addMonoidHom_comp_mapRange
+ mapDomain.addMonoidHom_id
+ mapDomainEmbedding
+ mapDomain_add
+ mapDomain_apply
+ mapDomain_apply'
+ mapDomain_comp
+ mapDomain_congr
+ mapDomain_dcongr
+ mapDomain_eq_sum
+ mapDomain_equiv_apply
+ mapDomain_finsetSum
+ mapDomain_fun_id
+ mapDomain_id
+ mapDomain_injOn
+ mapDomain_injective
+ mapDomain_mapRange
+ mapDomain_notin_range
+ mapDomain_rightInverse
+ mapDomain_single
+ mapDomain_sub
+ mapDomain_sum
+ mapDomain_support
+ mapDomain_support_of_injOn
+ mapDomain_support_of_injective
+ mapDomain_surjective
+ mapDomain_zero
+ mapRange_fun_comp
+ mapRange_fun_id
+ prod_congr
+ prod_embDomain
+ prod_mapDomain_index
+ prod_mapDomain_index_inj
+ sum_mapDomain_index_addMonoidHom
+ support_embDomain

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a60ac7c).

+57 new declarations
−0 removed declarations

+AddCommMonoid.toAddMonoid.hcongr_2
+AddMonoid.toAddZeroClass.hcongr_2
+AddZero.toZero.hcongr_2
+AddZeroClass.toAddZero.hcongr_2
+DFinsupp.embDomain
+DFinsupp.embDomain.match_1.congr_eq_1
+DFinsupp.embDomain.match_1.congr_eq_2
+DFinsupp.embDomain_apply_self
+DFinsupp.embDomain_eq_mapDomain
+DFinsupp.embDomain_notin_range
+DFinsupp.equivCongrLeft_symm_eq_mapDomain
+DFinsupp.mapDomain
+DFinsupp.mapDomain.addMonoidHom
+DFinsupp.mapDomain.addMonoidHom_apply
+DFinsupp.mapDomain.addMonoidHom_comp
+DFinsupp.mapDomain.addMonoidHom_comp_mapRange
+DFinsupp.mapDomain.addMonoidHom_id
+DFinsupp.mapDomain.congr_simp
+DFinsupp.mapDomainEmbedding
+DFinsupp.mapDomainEmbedding_apply
+DFinsupp.mapDomain_add
+DFinsupp.mapDomain_apply
+DFinsupp.mapDomain_apply'
+DFinsupp.mapDomain_comp
+DFinsupp.mapDomain_congr
+DFinsupp.mapDomain_dcongr
+DFinsupp.mapDomain_eq_sum
+DFinsupp.mapDomain_equiv_apply
+DFinsupp.mapDomain_finsetSum
+DFinsupp.mapDomain_fun_id
+DFinsupp.mapDomain_id
+DFinsupp.mapDomain_injOn
+DFinsupp.mapDomain_injective
+DFinsupp.mapDomain_mapRange
+DFinsupp.mapDomain_notin_range
+DFinsupp.mapDomain_rightInverse
+DFinsupp.mapDomain_single
+DFinsupp.mapDomain_sub
+DFinsupp.mapDomain_sum
+DFinsupp.mapDomain_support
+DFinsupp.mapDomain_support_of_injOn
+DFinsupp.mapDomain_support_of_injective
+DFinsupp.mapDomain_surjective
+DFinsupp.mapDomain_zero
+DFinsupp.mapRange_fun_comp
+DFinsupp.mapRange_fun_id
+DFinsupp.prod_congr
+DFinsupp.prod_embDomain
+DFinsupp.prod_mapDomain_index
+DFinsupp.prod_mapDomain_index_inj
+DFinsupp.sum_congr
+DFinsupp.sum_embDomain
+DFinsupp.sum_mapDomain_index
+DFinsupp.sum_mapDomain_index_addMonoidHom
+DFinsupp.sum_mapDomain_index_inj
+DFinsupp.support_embDomain
+Function.Injective.subsingleton_fiber

Increase in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
499	1	erw

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5011	1	exposed public sections

Current commit a60ac7cccf
Reference commit 1f165a51de

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

mathlib-merge-conflicts · 2026-05-23T17:44:43Z

This pull request has conflicts, please merge master and resolve them.

mathlib-dependent-issues · 2026-07-13T11:38:28Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Data/Multiset): add the Multiset version of List.find? #40326~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

I am worried that striving for local consistency here means you are spreading some bad design choices about Finsupp.

YaelDillies · 2026-07-15T08:05:23Z

+theorem mapRange_fun_id (g : Π₀ i : ι, β₁ i) :
+    mapRange (fun _ x => x) (fun _ => rfl) g = g := by
  ext
  rfl

+@[simp]
+theorem mapRange_id (g : Π₀ i : ι, β₁ i) :
+    mapRange (fun i => (id : β₁ i → β₁ i)) (fun _ => rfl) g = g :=


Suggested change

theorem mapRange_fun_id (g : Π₀ i : ι, β₁ i) :

mapRange (fun _ x => x) (fun _ => rfl) g = g := by

ext

rfl

@[simp]

theorem mapRange_id (g : Π₀ i : ι, β₁ i) :

mapRange (fun i => (id : β₁ i → β₁ i)) (fun _ => rfl) g = g :=

@[to_fun (attr := simp) mapRange_fun_id]

theorem mapRange_id (g : Π₀ i : ι, β₁ i) :

mapRange (fun i => (id : β₁ i → β₁ i)) (fun _ => rfl) g = g :=

YaelDillies · 2026-07-15T08:05:35Z

+  ext
+  simp only [mapRange_apply]
+
 theorem mapRange_comp (f : ∀ i, β₁ i → β₂ i) (f₂ : ∀ i, β i → β₁ i) (hf : ∀ i, f i 0 = 0)


YaelDillies · 2026-07-15T10:07:19Z

Should it not be Map?

YaelDillies · 2026-07-15T10:12:38Z

+theorem mapDomain_fun_id (x : Π₀ b, M b) : mapDomain (·) x = x :=
+  congr($(sumAddHom_singleAddHom) x)
+
+/-- Note that `x` the RHS is mildly type-incorrect. -/


Suggested change

/-- Note that `x` the RHS is mildly type-incorrect. -/

/-- Note that `x` in the RHS is mildly type-incorrect. -/

YaelDillies · 2026-07-15T10:13:13Z

+/-- Note that `x` the RHS is mildly type-incorrect. -/
+@[simp]
+theorem mapDomain_id (x : Π₀ b, M (id b)) :
+    mapDomain id x = x :=


Doesn't that mean we shouldn't have this lemma?

I tried adding the correct version with suitable casting, but simp simplifies the id in the type anyway and changes it to this form.

Surely this is a bug?

YaelDillies · 2026-07-15T10:13:38Z

+    · grind
+    · exact (hs a).resolve_left ha |>.symm
+
+lemma embDomain_notin_range (f : α ↪ β) (v : Π₀ a, M (f a)) {b : β} (hb : b ∉ Set.range f) :


Let's not spread poor naming

Suggested change

lemma embDomain_notin_range (f : α ↪ β) (v : Π₀ a, M (f a)) {b : β} (hb : b ∉ Set.range f) :

lemma embDomain_of_notMem_range (f : α ↪ β) (v : Π₀ a, M (f a)) {b : β} (hb : b ∉ Set.range f) :

See #41766 for the Finsupp rename

YaelDillies · 2026-07-15T10:13:58Z

+  is the finitely supported function whose value at `a : β` is the sum
+  of `v x` over all `x` such that `f x = a`. -/


Suggested change

is the finitely supported function whose value at `a : β` is the sum

of `v x` over all `x` such that `f x = a`. -/

is the finitely supported function whose value at `a : β` is the sum

of `v x` over all `x` such that `f x = a`. -/

YaelDillies · 2026-07-15T10:20:41Z

+theorem mapDomain_congr {f g : α → β} [(x : N) → Decidable (x ≠ 0)]
+    (v : Π₀ _ : α, N) (h : ∀ x ∈ v.support, f x = g x) :
+    v.mapDomain f = (mapDomain g v : Π₀ _ : β, N) := by


I suggest

Suggested change

theorem mapDomain_congr {f g : α → β} [(x : N) → Decidable (x ≠ 0)]

(v : Π₀ _ : α, N) (h : ∀ x ∈ v.support, f x = g x) :

v.mapDomain f = (mapDomain g v : Π₀ _ : β, N) := by

@[congr]

theorem mapDomain_congr {f g : α → β} [(x : N) → Decidable (x ≠ 0)]

(v : Π₀ _ : α, N) (h : ∀ x ∈ v.support, f x = g x) :

v.mapDomain f = (mapDomain g v : Π₀ _ : β, N) := by

to match #39575

YaelDillies · 2026-07-15T10:21:18Z

+theorem mapDomain_add {f : α → β} (v₁ v₂ : Π₀ a, M (f a)) :
+    mapDomain f (v₁ + v₂) = mapDomain f v₁ + mapDomain f v₂ :=
+  map_add _ _ _
+
+lemma mapDomain_sub {M : β → Type*} [∀ b, AddCommGroup (M b)]
+    {f : α → β} (v₁ v₂ : Π₀ a, M (f a)) :
+    mapDomain f (v₁ - v₂) = mapDomain f v₁ - mapDomain f v₂ :=
+  map_sub _ _ _


Any reason not to make this simp?

feat: DFinsupp.mapDomain

2a296af

github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label May 6, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 23, 2026

uncomment many declarations

47ab12c

eric-wieser temporarily deployed to cache-upload-forks June 5, 2026 22:49 — with GitHub Actions Inactive

embDomain

d765bfa

eric-wieser temporarily deployed to cache-upload-forks June 6, 2026 01:46 — with GitHub Actions Inactive

eric-wieser added 2 commits June 6, 2026 01:49

fewer sorries

3148832

the final lemma

613737b

eric-wieser temporarily deployed to cache-upload-forks June 6, 2026 02:21 — with GitHub Actions Inactive

split file

70eb975

eric-wieser temporarily deployed to cache-upload-forks June 7, 2026 06:18 — with GitHub Actions Inactive

remove a sorry

2458103

eric-wieser temporarily deployed to cache-upload-forks June 7, 2026 07:34 — with GitHub Actions Inactive

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 7, 2026

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 13, 2026

Merge remote-tracking branch 'origin/master' into dfinsupp-mapDomain

65c9093

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 13, 2026

eric-wieser force-pushed the dfinsupp-mapDomain branch from ad52257 to 65c9093 Compare July 13, 2026 22:01

cleanup

98727af

eric-wieser changed the title ~~feat: DFinsupp.mapDomain~~ feat: add DFinsupp.mapDomain to match Finsupp.mapDomain Jul 13, 2026

eric-wieser requested a review from YaelDillies July 13, 2026 22:06

eric-wieser marked this pull request as ready for review July 13, 2026 22:06

eric-wieser added 3 commits July 13, 2026 22:07

stray todo

c429136

generalize proofs

f61674d

fix dependent type issues

a60ac7c

YaelDillies reviewed Jul 15, 2026

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2026

	/-- Note that `x` the RHS is mildly type-incorrect. -/
	/-- Note that `x` in the RHS is mildly type-incorrect. -/

	lemma embDomain_notin_range (f : α ↪ β) (v : Π₀ a, M (f a)) {b : β} (hb : b ∉ Set.range f) :
	lemma embDomain_of_notMem_range (f : α ↪ β) (v : Π₀ a, M (f a)) {b : β} (hb : b ∉ Set.range f) :

		is the finitely supported function whose value at `a : β` is the sum
		of `v x` over all `x` such that `f x = a`. -/

Uh oh!

Conversation

eric-wieser commented May 6, 2026 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a60ac7cccf

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented May 23, 2026

Uh oh!

mathlib-dependent-issues Bot commented Jul 13, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

eric-wieser commented May 6, 2026 •

edited by YaelDillies

Loading

github-actions Bot commented May 6, 2026 •

edited

Loading