feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API

[chrisflav]

trafficstars

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.

---

[github-actions[bot]]

PR summary 3e0c4c31e6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.Morphisms.Constructors	1555	1557	+2 (+0.13%)

Import changes for all files

Files	Import difference
3 files Mathlib.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>

[erdOne]

Please merge master, thanks.

[chrisflav]

Please merge master, thanks.

Done.

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

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

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style