[Merged by Bors] - feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API#14328
[Merged by Bors] - feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API#14328
Conversation
PR summary 3e0c4c31e6
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.AlgebraicGeometry.Morphisms.Constructors | 1555 | 1557 | +2 (+0.13%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed |
2 |
Declarations diff
+ AffineTargetMorphismProperty.of
+ of_isLocal_of_isLocalAtTarget
+ stableUnderBaseChange_of_stableUnderBaseChangeOnAffine_of_isLocalAtTarget
+ stalkwise
+ stalkwiseIsLocalAtTarget_of_respectsIso
+ stalkwise_respectsIso
+ targetAffineLocally_of_eq_of_isLocalAtTarget
+ toMorphismProperty
+ toMorphismProperty_respectsIso_iff
+ topologically
+ topologically_isStableUnderComposition
+ topologically_iso_le
+ topologically_propertyIsLocalAtTarget
+ topologically_respectsIso
- MorphismProperty.topologically
- MorphismProperty.topologically_isStableUnderComposition
- MorphismProperty.topologically_iso_le
- MorphismProperty.topologically_propertyIsLocalAtTarget
- MorphismProperty.topologically_respectsIso
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>|
Please merge master, thanks. |
Done. |
|
|
||
| /-- A morphism property of schemes is `StableUnderAffineBaseChange` if | ||
| the base change along a morphism of affine schemes of a morphism with affine target is affine. -/ | ||
| def StableUnderAffineBaseChange (P : MorphismProperty Scheme) : Prop := |
There was a problem hiding this comment.
Is this just (of P).StableUnderBaseChange?
There was a problem hiding this comment.
Yes, I added this to hide the interaction with of P and AffineTargetMorphismProperty in StableUnderAffineBaseChange.stableUnderBaseChange, but I am happy to just assume (of P).StableUnderBaseChange in this lemma instead. What do you think?
There was a problem hiding this comment.
I think it makes sense to use (of P).StableUnderBaseChange directly.
There was a problem hiding this comment.
Okay, I removed that part.
|
Thanks! |
|
🚀 Pull request has been placed on the maintainer queue by erdOne. |
|
Thanks! bors merge |
…#14328) Adds a `MorphismProperty.stalkwise` constructor for morphism properties of schemes from a property of ring homomorphisms. Also adds API for reducing proofs of stability under base change to affine situations for properties local at the target.
|
Pull request successfully merged into master. Build succeeded: |
Adds a
MorphismProperty.stalkwiseconstructor for morphism properties of schemes from a property of ring homomorphisms. Also adds API for reducing proofs of stability under base change to affine situations for properties local at the target.