[Merged by Bors] - feat(AlgebraicGeometry): preimmersions are stable under base change#18915
[Merged by Bors] - feat(AlgebraicGeometry): preimmersions are stable under base change#18915
Conversation
erdOne
commented
Nov 12, 2024
PR summary 625dd2971c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.AlgebraicGeometry.Morphisms.Preimmersion | 1753 | 1758 | +5 (+0.29%) |
| Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion | 1785 | 1787 | +2 (+0.11%) |
Import changes for all files
| Files | Import difference |
|---|---|
8 filesMathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed |
2 |
4 filesMathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.PullbackCarrier |
5 |
Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks |
1756 |
Declarations diff
+ Cover.exists_eq
+ Hom.homeomorph_apply
+ Spec_iff
+ SurjectiveOnStalks
+ comp
+ eq_stalkwise
+ homeoOfIso_apply
+ homeoOfIso_symm
+ iff_of_isAffine
+ instance (priority := 900) [IsOpenImmersion f] : SurjectiveOnStalks f
+ instance : HasRingHomProperty @SurjectiveOnStalks RingHom.SurjectiveOnStalks
+ instance : IsLocalAtSource @SurjectiveOnStalks
+ instance : IsLocalAtTarget @SurjectiveOnStalks
+ instance : IsStableUnderBaseChange @IsPreimmersion := by
+ instance : MorphismProperty.IsMultiplicative @SurjectiveOnStalks
+ isEmbedding_of_iSup_eq_top_of_preimage_subset_range
+ isEmbedding_pullback
+ of_comp
+ stableUnderBaseChange
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
Thanks! bors d+ |
|
✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
bors merge |
…18915) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |