Skip to content

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

Closed
justus-springer wants to merge 7 commits into
leanprover-community:masterfrom
justus-springer:justus/restrict_lemmas
Closed

[Merged by Bors] - feat(AlgebraicGeometry/Restrict): a few more restriction lemmas#39442
justus-springer wants to merge 7 commits into
leanprover-community:masterfrom
justus-springer:justus/restrict_lemmas

Conversation

@justus-springer

@justus-springer justus-springer commented May 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

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

Open in Gitpod

@github-actions

github-actions Bot commented May 15, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 197a97edf7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Scheme.Hom.isoImage_hom_homOfLE
+ Scheme.Hom.isoImage_inv_homOfLE
+ Scheme.Hom.isoImage_preimage_hom_homOfLE
+ Scheme.Opens.isoImage_ι_inv_ι
+ isoImage_ι_inv_morphismRestrict_homOfLE
+ morphismRestrict_homOfLE
+ morphismRestrict_homOfLE_isoImage_ι_hom
+ morphismRestrict_morphismRestrict_ι_isoImage_hom
+ morphismRestrict_ι_image_ι_isoImage_inv

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.

@github-actions github-actions Bot added the t-algebraic-geometry Algebraic geometry label May 15, 2026
@justus-springer justus-springer mentioned this pull request May 15, 2026
Closed
4 tasks
@chrisflav chrisflav self-assigned this May 21, 2026
chrisflav
chrisflav reviewed May 25, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicGeometry/Restrict.lean Outdated
Comment thread Mathlib/AlgebraicGeometry/Restrict.lean Outdated
Comment thread Mathlib/AlgebraicGeometry/Restrict.lean Outdated
Comment thread Mathlib/AlgebraicGeometry/Restrict.lean Outdated
Comment thread Mathlib/AlgebraicGeometry/Restrict.lean Outdated
@chrisflav chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label May 25, 2026
justus-springer and others added 5 commits May 26, 2026 11:48
@justus-springer @chrisflav
Apply suggestion from @chrisflav
3343cbb 
Co-authored-by: Christian Merten <christian@merten.dev>
@justus-springer @chrisflav
Apply suggestion from @chrisflav
a7b8053 
Co-authored-by: Christian Merten <christian@merten.dev>
@justus-springer @chrisflav
Apply suggestion from @chrisflav
700394a 
Co-authored-by: Christian Merten <christian@merten.dev>
@justus-springer @chrisflav
Apply suggestion from @chrisflav
865d904 
Co-authored-by: Christian Merten <christian@merten.dev>
@justus-springer
review
0cee355
chrisflav
chrisflav approved these changes May 26, 2026
View reviewed changes

@chrisflav chrisflav left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Thanks!
maintainer merge

@chrisflav chrisflav removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 26, 2026
@chrisflav

chrisflav commented May 26, 2026

Copy link
Copy Markdown
Member

(CI is broken at the moment, so there might be some delays.)

@chrisflav

chrisflav commented May 26, 2026

Copy link
Copy Markdown
Member

Could you please merge master to re-trigger CI? It seems github is alive again.

@chrisflav chrisflav added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 26, 2026
@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 26, 2026
@chrisflav

chrisflav commented May 27, 2026

Copy link
Copy Markdown
Member

Thanks!
maintainer merge

@github-actions

github-actions Bot commented May 27, 2026

Copy link
Copy Markdown

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

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

riccardobrasca commented May 27, 2026

Copy link
Copy Markdown
Member

Thanks!

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 May 27, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 27, 2026
@justus-springer
feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (#39442)
8d95dbc 
These will be used later to define composition of rational maps in #39445.
@mathlib-bors

mathlib-bors Bot commented May 27, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(AlgebraicGeometry/Restrict): a few more restriction lemmas [Merged by Bors] - feat(AlgebraicGeometry/Restrict): a few more restriction lemmas May 27, 2026
@mathlib-bors mathlib-bors Bot closed this May 27, 2026
grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026
@justus-springer @grunweg
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
@justus-springer @b-mehta
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.
This was referenced Jun 3, 2026
Closed
Closed
mathlib-bors Bot pushed a commit that referenced this pull request Jun 3, 2026
@justus-springer
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
6fd9ef1 
…ed by toolchain bump (#40189)

These two lemmas were originally added in #39442. Then the toolchain bump #39980 mysteriously deleted them two days later without replacement.
mathlib-bors Bot pushed a commit that referenced this pull request Jun 3, 2026
@justus-springer
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
630116a 
…ed by toolchain bump (#40189)

These two lemmas were originally added in #39442. Then the toolchain bump #39980 mysteriously deleted them two days later without replacement.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@justus-springer @Bergschaf
feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (lean…
d82bdee 
…prover-community#39442)

These will be used later to define composition of rational maps in leanprover-community#39445.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@justus-springer @Bergschaf
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
01599e5 
…ed by toolchain bump (leanprover-community#40189)

These two lemmas were originally added in leanprover-community#39442. Then the toolchain bump leanprover-community#39980 mysteriously deleted them two days later without replacement.
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@justus-springer @ReemMelamed
chore(AlgebraicGeometry/Restrict): restore two lemmas that were delet…
4790bc7 
…ed by toolchain bump (leanprover-community#40189)

These two lemmas were originally added in leanprover-community#39442. Then the toolchain bump leanprover-community#39980 mysteriously deleted them two days later without replacement.
mathlib-bors Bot pushed a commit that referenced this pull request Jul 10, 2026
@justus-springer
feat(AlgebraicGeometry/Birational): composition of rational maps (#39445
d45663d 
)

Define composition of partial and rational maps.

- [x] depends on: #39442
- [x] depends on: #39443
- [x] depends on: #39317
- [x] depends on: #40189
michaellee94 pushed a commit to michaellee94/mathlib4 that referenced this pull request Jul 11, 2026
@justus-springer @michaellee94
feat(AlgebraicGeometry/Birational): composition of rational maps (lea…
7a70c89 
…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
mpacholski pushed a commit to mpacholski/mathlib4 that referenced this pull request Jul 16, 2026
@justus-springer @mpacholski
feat(AlgebraicGeometry/Birational): composition of rational maps (lea…
1d511b9 
…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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chrisflav chrisflav chrisflav approved these changes

Assignees

@chrisflav chrisflav

Labels

ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@justus-springer @chrisflav @riccardobrasca