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

justus-springer · 2026-05-13T18:40:50Z

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.

depends on: [Merged by Bors] - chore(AlgebraicGeometry/): create Birational subdirectory #39316
depends on: [Merged by Bors] - feat(AlgebraicGeometry/Birational/RationalMap): add RationalMap.representative #39656

github-actions · 2026-05-13T18:42:13Z

PR summary 2fee0c09c7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.AlgebraicGeometry.Birational.Dominant` (new file)	2456

Declarations diff

+ PartialMap.isDominant_toRationalMap_iff
+ RationalMap.IsDominant
+ instance (f : X ⤏ Y) [f.IsDominant] :
+ instance (f : X.PartialMap Y) [IsDominant f.hom] :
+ isDominant_hom_iff_isDominant_restrict_hom
+ isDominant_hom_iff_of_equiv
+ isDominant_hom_of_isDominant_restrict_hom
+ isDominant_restrict_hom

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.

No changes to strong technical debt.

No changes to weak technical debt.

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

…us-springer/mathlib4 into justus/rationalMap_dominant

…esentative` (#39656) Split off from #39317

mathlib-dependent-issues · 2026-05-23T12:50:04Z

This PR/issue depends on:

~~[Merged by Bors] - chore(AlgebraicGeometry/): create Birational subdirectory #39316~~
~~[Merged by Bors] - feat(AlgebraicGeometry/Birational/RationalMap): add RationalMap.representative #39656~~
By Dependent Issues (🤖). Happy coding!

chrisflav

Thanks!
maintainer delegate

github-actions · 2026-05-23T14:14:09Z

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

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

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

riccardobrasca · 2026-05-27T10:00:42Z

Thanks!

bors merge

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

mathlib-bors · 2026-05-27T11:17:07Z

Pull request successfully merged into master.

Build succeeded:

…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

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

…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

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

…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

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

…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

dominant rational maps

bfea74f

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

github-actions Bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label May 13, 2026

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

Merge branch 'master' into justus/rationalMap_dominant

d6e490f

github-actions Bot removed the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label May 13, 2026

Merge branch 'master' into justus/rationalMap_dominant

0ccb979

justus-springer mentioned this pull request May 15, 2026

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

Closed

4 tasks

mathlib-triage Bot assigned dagurtomas May 20, 2026

dagurtomas requested a review from chrisflav May 21, 2026 04:02

dagurtomas approved these changes May 21, 2026

View reviewed changes

chrisflav reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicGeometry/Birational/Dominant.lean Outdated

Comment thread Mathlib/AlgebraicGeometry/Birational/Dominant.lean Outdated

Comment thread Mathlib/AlgebraicGeometry/Birational/Dominant.lean Outdated

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

chrisflav self-assigned this May 21, 2026

justus-springer and others added 4 commits May 21, 2026 09:04

Update Mathlib/AlgebraicGeometry/Birational/Dominant.lean

0d9d0aa

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

delete dominantRep, use Quotient.lift

9744a18

add RationalMap.representative

b271176

Merge branch 'justus/rationalMap_dominant' of https://github.com/just…

649f9fc

…us-springer/mathlib4 into justus/rationalMap_dominant

justus-springer mentioned this pull request May 21, 2026

[Merged by Bors] - feat(AlgebraicGeometry/Birational/RationalMap): add RationalMap.representative #39656

Closed

Merge branch 'master' into justus/rationalMap_dominant

4a89d29

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

justus-springer removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 21, 2026

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

feat(AlgebraicGeometry/Birational/RationalMap): add `RationalMap.repr…

7f2af3f

…esentative` (#39656) Split off from #39317

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

Merge branch 'master' into justus/rationalMap_dominant

f5820b9

chrisflav approved these changes May 23, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicGeometry/Birational/Dominant.lean Outdated

Comment thread Mathlib/AlgebraicGeometry/Birational/Dominant.lean Outdated

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

justus-springer and others added 2 commits May 23, 2026 15:56

Update Mathlib/AlgebraicGeometry/Birational/Dominant.lean

84ddc6b

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

Update Mathlib/AlgebraicGeometry/Birational/Dominant.lean

2fee0c0

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

RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 24, 2026

feat(AlgebraicGeometry/Birational/RationalMap): add `RationalMap.repr…

2bf8662

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

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

mathlib-bors Bot changed the title ~~feat(AlgebraicGeometry/Birational): dominant rational maps~~ [Merged by Bors] - feat(AlgebraicGeometry/Birational): dominant rational maps May 27, 2026

mathlib-bors Bot closed this May 27, 2026

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

feat(AlgebraicGeometry/Birational/RationalMap): add `RationalMap.repr…

d408836

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026

feat(AlgebraicGeometry/Birational/RationalMap): add `RationalMap.repr…

d80b948

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

[Merged by Bors] - feat(AlgebraicGeometry/Birational): dominant rational maps#39317
justus-springer wants to merge 11 commits into
leanprover-community:masterfrom
justus-springer:justus/rationalMap_dominant

justus-springer commented May 13, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 13, 2026 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-dependent-issues Bot commented May 23, 2026

Uh oh!

chrisflav left a comment

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 23, 2026

Uh oh!

riccardobrasca commented May 27, 2026

Uh oh!

mathlib-bors Bot commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 2fee0c09c7

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-dependent-issues Bot commented May 23, 2026

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 23, 2026

Uh oh!

riccardobrasca commented May 27, 2026

Uh oh!

mathlib-bors Bot commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

justus-springer commented May 13, 2026 •

edited

Loading

github-actions Bot commented May 13, 2026 •

edited

Loading