[Merged by Bors] - refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs #14430

erdOne · 2024-07-04T22:16:10Z

Previously the contents of Morphism/Basic 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

P respects isomorphisms.
If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any open U of Y.
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.

…-iso-typeclass

…lib4 into erd1/morphismRework

github-actions · 2024-07-04T22:16:49Z

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>

…ypeclass' into erd1/morphismRework

…lib4 into erd1/morphismRework

erdOne · 2024-07-15T05:16:11Z

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

chrisflav

As I said earlier, I really like this change.

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Mathlib/AlgebraicGeometry/Cover/Open.lean

Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

chrisflav · 2024-07-15T10:43:58Z

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

-theorem QuasiCompact.affine_openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.OpenCover.{u} Y)
-    [∀ i, IsAffine (𝒰.obj i)] (f : X ⟶ Y) :
-    QuasiCompact f ↔ ∀ i, CompactSpace (pullback f (𝒰.map i) : _) :=
-  quasiCompact_eq_affineProperty.symm ▸ QuasiCompact.affineProperty_isLocal.affine_openCover_iff f 𝒰
-#align algebraic_geometry.quasi_compact.affine_open_cover_iff AlgebraicGeometry.QuasiCompact.affine_openCover_iff
-


What did come out of this?

chrisflav

LGTM, thanks a lot!

erdOne · 2024-07-18T08:10:14Z

Thanks for the swift review!

mattrobball · 2024-07-18T11:39:21Z

!bench

jcommelin

Thanks 🎉

bors merge

…rom 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. Co-authored-by: Andrew Yang <[email protected]> Co-authored-by: Joël Riou <[email protected]>

mattrobball · 2024-07-18T11:52:08Z

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

bors r-

mathlib-bors · 2024-07-18T11:52:10Z

Canceled.

leanprover-bot · 2024-07-18T12:06:16Z

Here are the benchmark results for commit a67d97b.
There were significant changes against commit af10129:

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

mattrobball · 2024-07-18T12:08:07Z

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

bors merge

…rom 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. Co-authored-by: Andrew Yang <[email protected]> Co-authored-by: Joël Riou <[email protected]>

mathlib-bors · 2024-07-18T12:18:01Z

Pull request successfully merged into master.

Build succeeded:

erdOne and others added 24 commits June 26, 2024 17:48

first commit

c28454a

stash

ce67bdc

stash

3e105cb

chore: make MorphismProperty.RespectsIso a typeclass

f6cf241

fixing the build

27f791d

fixing the build

787a915

fixing the build

f965a58

removing @[simp] attr

73eb1b0

removing bumps in heartBeats

4458a50

reverted mistakes

6210594

fixing the build

85d21ca

fixing the build

c1c2ff4

fixing the build

5b5ab87

wip

d234452

fixing the build

1a78da9

fixing the build

73fd8ec

fixing the build

5b2c52e

fixing the build

d53304b

fixing the build

420f265

fixing the build

c154949

fixing the build

2f36b97

removed set_option maxHeartBeats

5574a51

Merge remote-tracking branch 'origin' into morphism-property-respects…

e2c69ac

…-iso-typeclass

Merge branch 'master' of https://github.com/leanprover-community/math…

3293fad

…lib4 into erd1/morphismRework

erdOne added the WIP Work in progress label Jul 4, 2024

erdOne added 4 commits July 5, 2024 12:01

stash

cac5968

Merge remote-tracking branch 'origin/morphism-property-respects-iso-t…

1e9fb02

…ypeclass' into erd1/morphismRework

fix

2099903

Merge branch 'master' of https://github.com/leanprover-community/math…

5779562

…lib4 into erd1/morphismRework

erdOne added 5 commits July 15, 2024 12:18

fix

5126336

fix

0fe480d

fix

b6e4dae

fix

1da99fb

fix

b102ef4

chrisflav reviewed Jul 15, 2024

View reviewed changes

chrisflav mentioned this pull request Jul 15, 2024

[Merged by Bors] - feat(AlgebraicGeometry): closed immersions are local at the target #14763

Closed

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 16, 2024

erdOne added 4 commits July 16, 2024 20:52

address comments

0a953fa

address comments

48300ec

oops

3df14c1

fix

a67d97b

erdOne removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 16, 2024

chrisflav approved these changes Jul 18, 2024

View reviewed changes

jcommelin reviewed Jul 18, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jul 18, 2024

mathlib-bors bot changed the title ~~refactor(AlgebraicGeometry): Rework Morphisms/Basic to phase away from TFAEs~~ [Merged by Bors] - refactor(AlgebraicGeometry): Rework Morphisms/Basic to phase away from TFAEs Jul 18, 2024

mathlib-bors bot closed this Jul 18, 2024

mathlib-bors bot deleted the erd1/morphismRework branch July 18, 2024 12:18

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs #14430

[Merged by Bors] - refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs #14430

erdOne commented Jul 4, 2024 •

edited by grunweg

Loading

github-actions bot commented Jul 4, 2024 •

edited

Loading

Declarations diff

erdOne commented Jul 15, 2024

chrisflav left a comment

chrisflav Jul 15, 2024

chrisflav left a comment

erdOne commented Jul 18, 2024

mattrobball commented Jul 18, 2024

jcommelin left a comment

mattrobball commented Jul 18, 2024

mathlib-bors bot commented Jul 18, 2024

leanprover-bot commented Jul 18, 2024

mattrobball commented Jul 18, 2024

mathlib-bors bot commented Jul 18, 2024

[Merged by Bors] - refactor(AlgebraicGeometry): Rework Morphisms/Basic to phase away from TFAEs #14430

[Merged by Bors] - refactor(AlgebraicGeometry): Rework Morphisms/Basic to phase away from TFAEs #14430

Conversation

erdOne commented Jul 4, 2024 • edited by grunweg Loading

IsLocalAtTarget

HasAffineProperty

github-actions bot commented Jul 4, 2024 • edited Loading

PR summary a67d97bfc5

Import changes for modified files

Declarations diff

erdOne commented Jul 15, 2024

chrisflav left a comment

Choose a reason for hiding this comment

chrisflav Jul 15, 2024

Choose a reason for hiding this comment

chrisflav left a comment

Choose a reason for hiding this comment

erdOne commented Jul 18, 2024

mattrobball commented Jul 18, 2024

jcommelin left a comment

Choose a reason for hiding this comment

mattrobball commented Jul 18, 2024

mathlib-bors bot commented Jul 18, 2024

leanprover-bot commented Jul 18, 2024

mattrobball commented Jul 18, 2024

mathlib-bors bot commented Jul 18, 2024

[Merged by Bors] - refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs #14430

[Merged by Bors] - refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs #14430

erdOne commented Jul 4, 2024 •

edited by grunweg

Loading

`IsLocalAtTarget`

`HasAffineProperty`

github-actions bot commented Jul 4, 2024 •

edited

Loading