[Merged by Bors] - feat(AlgebraicGeometry/Birational): composition of rational maps by justus-springer · Pull Request #39445 · leanprover-community/mathlib4

justus-springer · 2026-05-15T22:44:43Z

Define composition of partial and rational maps.

depends on: [Merged by Bors] - feat(AlgebraicGeometry/Restrict): a few more restriction lemmas #39442
depends on: [Merged by Bors] - feat(Data/Set/Image): nonempty_preimage_iff #39443
depends on: [Merged by Bors] - feat(AlgebraicGeometry/Birational): dominant rational maps #39317
depends on: [Merged by Bors] - chore(AlgebraicGeometry/Restrict): restore two lemmas that were deleted by toolchain bump #40189

github-actions · 2026-05-15T22:45:56Z

PR summary 99cf452522

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.AlgebraicGeometry.Birational.Composition` (new file)	2464

Declarations diff (regex)

+ PartialMap.id_comp
+ RationalMap.id
+ RationalMap.id_comp
+ RationalMap.id_compHom
+ _root_.AlgebraicGeometry.Scheme.Hom.toPartialMap_compHom
+ compHom_id
+ comp_def
+ comp_equiv_of_equiv
+ comp_equiv_of_equiv_left
+ comp_equiv_of_equiv_right
+ comp_restrict_left
+ comp_restrict_right
+ comp_toPartialMap
+ comp_toRationalMap
+ equiv.refl
+ equiv.symm
+ equiv.trans
+ equiv_of_restrict_eq
+ id
+ id_compHom
+ instance (f : X ⟶ Y) [IsDominant f] : IsDominant f.toPartialMap.hom := by
+ instance (f : X ⤏ Y) [f.IsDominant] (g : Y ⤏ Z) [g.IsDominant] : (f.comp g).IsDominant := by
+ inv_preimage
+ isDominant_comp_hom
+ isOver_comp
+ toRationalMap_comp
++ comp
++ comp_assoc
++ comp_id

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 89f3c49).

+36 new declarations
−0 removed declarations

+AlgebraicGeometry.Scheme.Hom.inv_preimage
+AlgebraicGeometry.Scheme.Hom.toPartialMap_compHom
+AlgebraicGeometry.Scheme.PartialMap.comp
+AlgebraicGeometry.Scheme.PartialMap.comp.congr_simp
+AlgebraicGeometry.Scheme.PartialMap.compHom_id
+AlgebraicGeometry.Scheme.PartialMap.comp_assoc
+AlgebraicGeometry.Scheme.PartialMap.comp_domain
+AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv
+AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_left
+AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_right
+AlgebraicGeometry.Scheme.PartialMap.comp_hom
+AlgebraicGeometry.Scheme.PartialMap.comp_id
+AlgebraicGeometry.Scheme.PartialMap.comp_restrict_left
+AlgebraicGeometry.Scheme.PartialMap.comp_restrict_right
+AlgebraicGeometry.Scheme.PartialMap.comp_toPartialMap
+AlgebraicGeometry.Scheme.PartialMap.equiv.refl
+AlgebraicGeometry.Scheme.PartialMap.equiv.symm
+AlgebraicGeometry.Scheme.PartialMap.equiv.trans
+AlgebraicGeometry.Scheme.PartialMap.equiv_of_restrict_eq
+AlgebraicGeometry.Scheme.PartialMap.id
+AlgebraicGeometry.Scheme.PartialMap.id_comp
+AlgebraicGeometry.Scheme.PartialMap.id_compHom
+AlgebraicGeometry.Scheme.PartialMap.instIsDominantHomToPartialMap
+AlgebraicGeometry.Scheme.PartialMap.isDominant_comp_hom
+AlgebraicGeometry.Scheme.RationalMap.comp
+AlgebraicGeometry.Scheme.RationalMap.comp.congr_simp
+AlgebraicGeometry.Scheme.RationalMap.comp_assoc
+AlgebraicGeometry.Scheme.RationalMap.comp_def
+AlgebraicGeometry.Scheme.RationalMap.comp_id
+AlgebraicGeometry.Scheme.RationalMap.comp_toRationalMap
+AlgebraicGeometry.Scheme.RationalMap.id
+AlgebraicGeometry.Scheme.RationalMap.id_comp
+AlgebraicGeometry.Scheme.RationalMap.id_compHom
+AlgebraicGeometry.Scheme.RationalMap.instIsDominantComp
+AlgebraicGeometry.Scheme.RationalMap.isOver_comp
+AlgebraicGeometry.Scheme.RationalMap.toRationalMap_comp

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

Current number	Change	Type (strong)
4532	11	backward.defeqAttrib.useBackward

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

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

Current commit 99cf452522
Reference commit b2b4255167

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).

Co-authored-by: Christian Merten <christian@merten.dev>

…tion

Add a predicate `RationalMap.IsDominant` and add basic API. This is in preparation for defining composition of rational maps (see #39445). See also [stacks#01RR](https://stacks.math.columbia.edu/tag/01RR). - [x] depends on: #39316 - [x] depends on: #39656

These will be used later to define composition of rational maps in #39445.

mathlib-merge-conflicts · 2026-05-30T01:24:48Z

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

…r-community#39317) Add a predicate `RationalMap.IsDominant` and add basic API. This is in preparation for defining composition of rational maps (see leanprover-community#39445). See also [stacks#01RR](https://stacks.math.columbia.edu/tag/01RR). - [x] depends on: leanprover-community#39316 - [x] depends on: leanprover-community#39656

…prover-community#39442) These will be used later to define composition of rational maps in leanprover-community#39445.

…r-community#39317) Add a predicate `RationalMap.IsDominant` and add basic API. This is in preparation for defining composition of rational maps (see leanprover-community#39445). See also [stacks#01RR](https://stacks.math.columbia.edu/tag/01RR). - [x] depends on: leanprover-community#39316 - [x] depends on: leanprover-community#39656

…prover-community#39442) These will be used later to define composition of rational maps in leanprover-community#39445.

chrisflav

Modulo the remaining question above, LGTM!

chrisflav · 2026-06-30T20:47:17Z

Thanks!
maintainer merge

github-actions · 2026-06-30T20:47:37Z

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

riccardobrasca · 2026-07-10T02:16:26Z

Thanks!

bors merge

) Define composition of partial and rational maps. - [x] depends on: #39442 - [x] depends on: #39443 - [x] depends on: #39317 - [x] depends on: #40189

mathlib-bors · 2026-07-10T02:27:45Z

Pull request successfully merged into master.

Build succeeded:

…parency` Master's leanprover-community#39445 (composition of rational maps) added `RationalMap.id_compHom` / `equiv.refl` and the whole `Birational/Composition` file, none of which carry a nightly guard. Without one the defeq is not accepted at `implicit` transparency, so `simp`/`simp_rw` are left with goals like `⊤.ι ≫ f = 𝟙 _ ≫ ⊤.ι ≫ f` and even `f.hom = f.hom`. Add `set_option backward.isDefEq.respectTransparency false in` to the affected declarations, as the rest of these files already do. With the guard in place `simp_rw` closes `comp_toPartialMap` outright, so its trailing `rfl` is now dead and is removed.

…nprover-community#39445) Define composition of partial and rational maps. - [x] depends on: leanprover-community#39442 - [x] depends on: leanprover-community#39443 - [x] depends on: leanprover-community#39317 - [x] depends on: leanprover-community#40189

justus-springer added 2 commits May 15, 2026 23:30

restriction lemmas

a884fb6

composition of rational maps

35ec727

github-actions Bot added the t-algebraic-geometry Algebraic geometry label May 15, 2026

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 May 15, 2026

This was referenced May 16, 2026

[Merged by Bors] - feat(AlgebraicGeometry/Birational): dominant rational maps #39317

Closed

[Merged by Bors] - feat(AlgebraicGeometry/Restrict): a few more restriction lemmas #39442

Closed

justus-springer and others added 10 commits May 21, 2026 13:29

add RationalMap.representative

d6e61c7

delete dominantRep, use Quotient.lift

74eb10f

update composition

6ae21f2

Apply suggestion from @chrisflav

3343cbb

Co-authored-by: Christian Merten <christian@merten.dev>

Apply suggestion from @chrisflav

a7b8053

Co-authored-by: Christian Merten <christian@merten.dev>

Apply suggestion from @chrisflav

700394a

Co-authored-by: Christian Merten <christian@merten.dev>

Apply suggestion from @chrisflav

865d904

Co-authored-by: Christian Merten <christian@merten.dev>

review

0cee355

Merge branch 'justus/restrict_lemmas' into justus/rationalMap_composi…

842024c

…tion

fix

8dc99e1

mathlib-bors Bot pushed a commit that referenced this pull request May 27, 2026

feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (#39442)

8d95dbc

These will be used later to define composition of rational maps in #39445.

Merge branch 'master' into justus/rationalMap_composition

e5f6a1e

justus-springer mentioned this pull request May 28, 2026

[Merged by Bors] - feat(AlgebraicGeometry/Birational): Birationality and rationality of schemes #39122

Closed

1 task

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 30, 2026

Merge branch 'master' into justus/rationalMap_composition

1c749e8

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 May 30, 2026

grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026

feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (lean…

4576665

…prover-community#39442) These will be used later to define composition of rational maps in leanprover-community#39445.

b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026

feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (lean…

4d43f07

…prover-community#39442) These will be used later to define composition of rational maps in leanprover-community#39445.

Merge branch 'master' into justus/rationalMap_composition

294d6dc

simpNF

db56d18

justus-springer added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 27, 2026

github-actions Bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 27, 2026

Merge branch 'master' into justus/rationalMap_composition

d2db27f

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 Jun 28, 2026

mk_all

36a8855

mathlib-triage Bot assigned joelriou Jun 29, 2026

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 30, 2026

chrisflav approved these changes Jun 30, 2026

View reviewed changes

justus-springer added 2 commits June 30, 2026 17:33

add comment

99cf452

Merge branch 'master' into justus/rationalMap_composition

89f3c49

justus-springer added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 30, 2026

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 30, 2026

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 30, 2026

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jul 10, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 10, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jul 10, 2026

mathlib-bors Bot changed the title ~~feat(AlgebraicGeometry/Birational): composition of rational maps~~ [Merged by Bors] - feat(AlgebraicGeometry/Birational): composition of rational maps Jul 10, 2026

mathlib-bors Bot closed this Jul 10, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - feat(AlgebraicGeometry/Birational): composition of rational maps#39445

[Merged by Bors] - feat(AlgebraicGeometry/Birational): composition of rational maps#39445
justus-springer wants to merge 37 commits into
leanprover-community:masterfrom
justus-springer:justus/rationalMap_composition

justus-springer commented May 15, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 15, 2026 •

edited

Loading

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented May 30, 2026

Uh oh!

chrisflav left a comment

Uh oh!

chrisflav commented Jun 30, 2026

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

riccardobrasca commented Jul 10, 2026

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Uh oh!

Conversation

justus-springer commented May 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 99cf452522

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented May 30, 2026

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

chrisflav commented Jun 30, 2026

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

riccardobrasca commented Jul 10, 2026

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

justus-springer commented May 15, 2026 •

edited

Loading

github-actions Bot commented May 15, 2026 •

edited

Loading