Commit 2024-07-18 12:08 65d6572c

refactor(AlgebraicGeometry): Rework Morphisms/Basic to phase away from TFAEs (#14430) Previously the contents of Morphism/Baisic were all implementation detail that needed to be copied over to each new morphism class. In this PR we clean up the file and promote it into a proper interface of the API. We also phase away from TFAEs in favor of easier to use iff lemmas. We introduce the following two interfaces:

IsLocalAtTarget

• AlgebraicGeometry.IsLocalAtTarget: We say that IsLocalAtTarget P for P : MorphismProperty Scheme if

1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any open U of Y.
3. If P holds for f ∣_ U for an open cover U of Y, then P holds for f. For a morphism property P local at the target and f : X ⟶ Y, we provide these API lemmas:

• AlgebraicGeometry.IsLocalAtTarget.of_isPullback: P is preserved under pullback along open immersions.
• AlgebraicGeometry.IsLocalAtTarget.restrict: P f → P (f ∣_ U) for an open U of Y.
• AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top: P f ↔ ∀ i, P (f ∣_ U i) for a family U i of open sets covering Y.
• AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover: P f ↔ ∀ i, P (𝒰.pullbackHom f i) for 𝒰 : Y.openCover.

HasAffineProperty

• AlgebraicGeometry.HasAffineProperty: HasAffineProperty P Q is a type class asserting that P is local at the target, and over affine schemes, it is equivalent to Q : AffineTargetMorphismProperty. For HasAffineProperty P Q and f : X ⟶ Y, we provide these API lemmas:
• AlgebraicGeometry.HasAffineProperty.of_isPullback: P is preserved under pullback along open immersions from affine schemes.
• AlgebraicGeometry.HasAffineProperty.restrict: P f → Q (f ∣_ U) for affine U of Y.
• AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top: P f ↔ ∀ i, Q (f ∣_ U i) for a family U i of affine open sets covering Y.
• AlgebraicGeometry.HasAffineProperty.iff_of_openCover: P f ↔ ∀ i, P (𝒰.pullbackHom f i) for affine open covers 𝒰 of Y.
• AlgebraicGeometry.HasAffineProperty.stableUnderBaseChange_mk: If Q is stable under affine base change, then P is stable under arbitrary base change.