Skip to content

[Merged by Bors] - chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own file.#13942

Closed
erdOne wants to merge 2 commits intomasterfrom
erd1/splitcover
Closed

[Merged by Bors] - chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own file.#13942
erdOne wants to merge 2 commits intomasterfrom
erd1/splitcover

Conversation

@erdOne
Copy link
Copy Markdown
Member

@erdOne erdOne commented Jun 19, 2024

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 19, 2024 •
edited
Loading

PR summary 6985802c21

Import changes

No significant changes to the import graph

Declarations diff

+ OpenCover.Hom
+ OpenCover.Hom.comp
+ OpenCover.Hom.id
+ OpenCover.category
+ OpenCover.comp_app
+ OpenCover.comp_idx_apply
+ OpenCover.compactSpace
+ OpenCover.fromAffineRefinement
+ OpenCover.iSup_opensRange
+ OpenCover.iUnion_range
+ OpenCover.id_app
+ OpenCover.id_idx_apply
+ OpenCover.inter
+ OpenCover.pullbackCover
+ OpenCover.pullbackCover'
+ Scheme.Hom.opensRange
+ exists_affine_mem_range_and_range_subset
+ instance (X : LocallyRingedSpace) {U : TopCat} (f : U ⟶ X.toTopCat) (hf : OpenEmbedding f) :
+ openCoverOfSuprEqTop
- Hom.opensRange
- Scheme.OpenCover.Hom
- Scheme.OpenCover.Hom.comp
- Scheme.OpenCover.Hom.id
- Scheme.OpenCover.category
- Scheme.OpenCover.comp_app
- Scheme.OpenCover.comp_idx_apply
- Scheme.OpenCover.compactSpace
- Scheme.OpenCover.fromAffineRefinement
- Scheme.OpenCover.iSup_opensRange
- Scheme.OpenCover.iUnion_range
- Scheme.OpenCover.id_app
- Scheme.OpenCover.id_idx_apply
- Scheme.OpenCover.inter
- Scheme.OpenCover.pullbackCover
- Scheme.OpenCover.pullbackCover'
- Scheme.openCoverOfSuprEqTop

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

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@erdOne erdOne added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebraic-geometry Algebraic geometry labels Jun 19, 2024
@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 Jun 19, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 19, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 19, 2024
@erdOne
chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own f…
1e77bed 
…ile. (#13942)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own file. [Merged by Bors] - chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own file. Jun 19, 2024
@mathlib-bors mathlib-bors bot closed this Jun 19, 2024
@mathlib-bors mathlib-bors bot deleted the erd1/splitcover branch June 19, 2024 15:52
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@erdOne @AntoineChambert-Loir
chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own f…
181fabf 
…ile. (#13942)
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@erdOne @kbuzzard
chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own f…
040b99a 
…ile. (#13942)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

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.

2 participants

@erdOne @joelriou