refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs

[erdOne]

---

[github-actions[bot]]

PR summary a67d97bfc5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ HasAffineProperty + HasAffineProperty.diagonal_affineProperty_isLocal + HasAffineProperty.diagonal_iff + HasAffineProperty.diagonal_of_diagonal_of_isPullback + HasAffineProperty.diagonal_of_openCover + HasAffineProperty.diagonal_of_openCover_diagonal + IsLocal + IsLocalAtTarget + OpenCover.pullbackCoverAffineRefinementObjIso + OpenCover.pullbackCoverAffineRefinementObjIso_inv_map + OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom + OpenCover.pullbackHom + OpenCover.pullbackHom_map + QuasiSeparated.of_comp + Scheme.resTop + StableUnderBaseChange.mk + arrow_mk_iso_iff + cancel_left_of_respectsIso + cancel_right_of_respectsIso + copy + eq_targetAffineLocally + ext + hasAffinePropertyAffineLocally + id_apply + iff + iff_of_isAffine + instance (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] : + instance (P : MorphismProperty Scheme) [IsLocalAtTarget P] : (of P).IsLocal + instance (P) [IsLocalAtTarget P] : IsLocalAtTarget P.diagonal + instance (P) {Q} [HasAffineProperty P Q] : HasAffineProperty P.diagonal Q.diagonal + instance (Q : AffineTargetMorphismProperty) [Q.IsLocal] : + instance (priority := 900) : IsLocalAtTarget P := by + instance (priority := 900) : P.RespectsIso := by + instance : HasAffineProperty @QuasiCompact (fun X _ _ _ ↦ CompactSpace X) + instance : HasAffineProperty @QuasiSeparated (fun X _ _ _ ↦ QuasiSeparatedSpace X) + instance [IsAffine X] (r : Γ(X, ⊤)) : IsAffine (X ∣_ᵤ X.basicOpen r) + instance {X} [IsAffine X] (i) : IsAffine ((Scheme.openCoverOfIsIso (𝟙 X)).obj i) := by + locallyOfFiniteType_isLocalAtTarget + mk' + of + of_isLocalAtTarget + of_targetAffineLocally_of_isPullback + preimage_of_isIso + quasiCompact_affineProperty_iff_quasiSeparatedSpace + respectsIso_mk + respectsIso_of + stableUnderBaseChange + toProperty + toProperty_apply + topologically_isLocalAtTarget + universallyClosed_fst + universallyClosed_snd ++ iff_of_iSup_eq_top ++ iff_of_openCover ++ of_iSup_eq_top ++ of_id_fst ++ of_id_snd ++ of_isPullback ++ of_openCover ++ restrict - AffineTargetMorphismProperty.IsLocal - AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE - AffineTargetMorphismProperty.IsLocal.affine_openCover_iff - AffineTargetMorphismProperty.IsLocal.affine_target_iff - AffineTargetMorphismProperty.IsLocal.diagonal - AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE - AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal - AffineTargetMorphismProperty.cancel_left_of_respectsIso - AffineTargetMorphismProperty.cancel_right_of_respectsIso - AffineTargetMorphismProperty.diagonal_of_targetAffineLocally - AffineTargetMorphismProperty.isLocalOfOpenCoverImply - AffineTargetMorphismProperty.of - AffineTargetMorphismProperty.respectsIso_mk - AffineTargetMorphismProperty.toProperty - AffineTargetMorphismProperty.toProperty_apply - CommRingCat.id_apply - IsAffineOpen.preimage_of_isIso - IsLocal.stableUnderBaseChange - IsLocal.targetAffineLocally_pullback_fst_of_right_of_stableUnderBaseChange - IsOpenImmersion.openCover_TFAE - IsOpenImmersion.openCover_iff - LocallyOfFiniteType.openCover_iff - PropertyIsLocalAtTarget - PropertyIsLocalAtTarget.openCover_TFAE - PropertyIsLocalAtTarget.openCover_iff - QuasiCompact.affineProperty - QuasiCompact.affineProperty_isLocal - QuasiCompact.affineProperty_stableUnderBaseChange - QuasiCompact.affineProperty_toProperty - QuasiCompact.affine_openCover_iff - QuasiCompact.affine_openCover_tfae - QuasiCompact.isLocalAtTarget - QuasiCompact.openCover_iff - QuasiCompact.openCover_tfae - QuasiSeparated.affineProperty - QuasiSeparated.affineProperty_isLocal - QuasiSeparated.affine_openCover_TFAE - QuasiSeparated.affine_openCover_iff - QuasiSeparated.isLocalAtTarget - QuasiSeparated.openCover_TFAE - QuasiSeparated.openCover_iff - Scheme.affineTargetIsIso - Scheme.isIso - UniversallyClosed.openCover_iff - diagonal_targetAffineLocally_eq_targetAffineLocally - diagonal_targetAffineLocally_of_openCover - instance : Inhabited AffineTargetMorphismProperty := ⟨Scheme.affineTargetIsIso⟩ - instance : QuasiCompact.affineProperty.toProperty.RespectsIso := by - instance {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated f] [QuasiSeparated g] : - is_local_affineLocally - locallyOfFiniteType_respectsIso - of_isLocal_of_isLocalAtTarget - propertyIsLocalAtTarget_of_morphismRestrict - quasiCompact_eq_affineProperty - quasiCompact_iff_affineProperty - quasiCompact_respectsIso - quasiSeparatedOfComp - quasiSeparated_eq_affineProperty - quasiSeparated_eq_affineProperty_diagonal - quasiSeparated_respectsIso - quasi_compact_affineProperty_diagonal_eq - quasi_compact_affineProperty_iff_quasiSeparatedSpace - targetAffineLocallyIsLocal - targetAffineLocallyPullbackFstOfRightOfStableUnderBaseChange - targetAffineLocally_of_eq_of_isLocalAtTarget - targetAffineLocally_of_openCover - targetAffineLocally_respectsIso - topologically_propertyIsLocalAtTarget - universallyClosedFst - universallyClosedSnd - universally_isLocalAtTarget_of_morphismRestrict

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>

[erdOne]

I think I have addressed all the comments. Thanks for the swift review!

[erdOne]

Thanks for the swift review!

[mattrobball]

!bench

[mattrobball]

Let's wait for the benchmarking to finish. AG is a finicky area currently.

bors r-

[mathlib-bors[bot]]

Canceled.

[leanprover-bot]

Here are the benchmark results for commit a67d97bfc51c6f6841ba2b0c2fa9f3e533641ddf. There were significant changes against commit af101290534012f2928c3d6d0d67f0aade6ef428:

  Benchmark                               Metric         Change
  =============================================================
- ~Mathlib.AlgebraicGeometry.Cover.Open   instructions    31.8%

[mattrobball]

Seems minor. I will see if I can track that down later.

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style