[Merged by Bors] - refactor(AlgebraicGeometry): Introduce `Scheme.Opens`. #15001

erdOne · 2024-07-22T06:41:38Z

Introduced Scheme.Opens as the type of open sets of a scheme. Provided instance : CoeOut X.Opens Scheme to replace the notation X ∣_ᵤ U, and renamed Scheme.ιOpens to Scheme.Opens.ι to enable dot notation.

Main changes are in Restrict.lean.

github-actions · 2024-07-22T06:42:15Z

PR summary 5916387248

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Scheme.Opens.ι_image_basicOpen
+ Scheme.component_nontrivial
+ Scheme.openCoverOfSuprEqTop
+ eqToHom_eq_homOfLE
+ eq_presheaf_map_eqToHom
+ germ_stalkIso_hom
+ instance : CoeOut X.Opens Scheme := ⟨toScheme⟩
+ instance : IsOpenImmersion U.ι := inferInstanceAs (IsOpenImmersion (X.ofRestrict _))
+ instance [IrreducibleSpace X] (U : X.Opens) [Nonempty U] :
+ instance [IsAffine X] (r : Γ(X, ⊤)) : IsAffine (X.basicOpen r)
+ instance [IsIntegral X] : IsDomain Γ(X, ⊤)
+ instance {X : Scheme} [IsIntegral X] {U : X.Opens} [Nonempty U] :
+ instance {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) [IsOpenImmersion f] :
+ instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] (U : Y.Opens) : IsIso (f ∣_ U) := by
+ instance {Y : Scheme.{u}} (U : Y.affineOpens) : IsAffine U
+ instance ΓRestrictAlgebra {X : Scheme.{u}} (U : X.Opens) :
+ instance ι_appLE_isIso :
+ nonempty_iff
+ opensRange_ι
+ preimage_comp
+ range_ι
+ stalkIso
+ toScheme
+ toScheme_carrier
+ toScheme_presheaf_map
+ toScheme_presheaf_obj
+ topIso
+ ι
+ ι_app
+ ι_appIso
+ ι_appLE
+ ι_app_self
+ ι_basicOpen_preimage
+ ι_image_top
+ ι_preimage_self
- Scheme.eq_restrict_presheaf_map_eqToHom
- Scheme.map_basicOpen
- Scheme.ofRestrict_app_self
- Scheme.resTop
- Scheme.ιOpens_appLE_isIso
- Scheme.ιOpens_image_top
- instance [IrreducibleSpace X] (U : Opens X) [Nonempty U] :
- instance [IsAffine X] (r : Γ(X, ⊤)) : IsAffine (X ∣_ᵤ X.basicOpen r)
- instance [h : IsIntegral X] : IsDomain Γ(X, ⊤)
- instance {X : Scheme} [IsIntegral X] {U : Opens X} [hU : Nonempty U] :
- instance {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Opens Y) [IsOpenImmersion f] :
- instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] (U : Opens Y) : IsIso (f ∣_ U) := by
- instance {Y : Scheme.{u}} (U : Y.affineOpens) :
- instance ΓRestrictAlgebra {X : Scheme.{u}} {Y : TopCat.{u}} {f : Y ⟶ X} (hf : OpenEmbedding f) :
- openCoverOfSuprEqTop
- opensRange_ιOpens
- ιOpens_basicOpen_preimage
--++ iff_of_iSup_eq_top
--++ of_iSup_eq_top

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 · 2024-07-22T09:50:30Z

!bench

leanprover-bot · 2024-07-22T10:28:06Z

Here are the benchmark results for commit 89bba21.
The entire run failed.
Found no significant differences.

erdOne · 2024-07-22T10:36:41Z

!bench

leanprover-bot · 2024-07-22T11:11:49Z

Here are the benchmark results for commit 2fc3307.
There were significant changes against commit a5fb11c:

  Benchmark                                                Metric         Change
  ==============================================================================
- build                                                    linting          6.4%
- ~Mathlib.AlgebraicGeometry.AffineScheme                  instructions    22.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.Basic               instructions   -46.9%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties   instructions   -50.6%
+ ~Mathlib.AlgebraicGeometry.Restrict                      instructions   -59.5%
+ ~Mathlib.AlgebraicGeometry.Scheme                        instructions   -22.4%

chrisflav

I'll review more tomorrow.

Mathlib/AlgebraicGeometry/Restrict.lean

chrisflav · 2024-07-23T00:06:14Z

Mathlib/AlgebraicGeometry/Restrict.lean

+def Scheme.openCoverOfSuprEqTop {s : Type*} (X : Scheme.{u}) (U : s → X.Opens)
+    (hU : ⨆ i, U i = ⊤) : X.OpenCover where


Suggested change

def Scheme.openCoverOfSuprEqTop {s : Type*} (X : Scheme.{u}) (U : s → X.Opens)

(hU : ⨆ i, U i = ⊤) : X.OpenCover where

def Scheme.openCoverOfiSupEqTop {s : Type*} (X : Scheme.{u}) (U : s → X.Opens)

(hU : ⨆ i, U i = ⊤) : X.OpenCover where

This is copy pasted from elsewhere. I'll make this change in a follow-up PR.

chrisflav

It looks like it does not make anything worse and some things definitely look better. The old X ∣_ᵤ U looked a bit funky in some places. Also that we can use dot notation on the open set is nice and opens up a potential refactor of IsAffineOpen.

Mathlib/AlgebraicGeometry/Restrict.lean

chrisflav · 2024-07-23T08:03:19Z

Mathlib/AlgebraicGeometry/Restrict.lean

+instance ΓRestrictAlgebra {X : Scheme.{u}} (U : X.Opens) :
+    Algebra (Scheme.Γ.obj (op X)) (Scheme.Γ.obj (op U)) :=
+  (Scheme.Γ.map U.ι.op).toAlgebra


Suggested change

instance ΓRestrictAlgebra {X : Scheme.{u}} (U : X.Opens) :

Algebra (Scheme.Γ.obj (op X)) (Scheme.Γ.obj (op U)) :=

(Scheme.Γ.map U.ι.op).toAlgebra

instance ΓRestrictAlgebra {X : Scheme.{u}} (U : X.Opens) :

Algebra Γ(X, ⊤) Γ(U, ⊤) :=

(Scheme.Γ.map U.ι.op).toAlgebra

This change will break other things. I'll make this change in a follow-up PR.

Mathlib/AlgebraicGeometry/Properties.lean

Co-authored-by: Christian Merten <[email protected]>

chrisflav

Thanks! LGTM.

erdOne · 2024-07-23T19:43:57Z

Mathlib/AlgebraicGeometry/AffineScheme.lean

-  rw [Scheme.comp_app, Scheme.comp_app, ΓSpecIso_obj_hom,
-    Scheme.ofRestrict_app_self]
-  simp only [Category.assoc]
-  dsimp only [asIso_inv, Functor.op_obj, unop_op]
-  rw [← Functor.map_comp_assoc, ← op_comp, eqToHom_trans, Scheme.eq_restrict_presheaf_map_eqToHom,
+  rw [Scheme.comp_app, Scheme.comp_app, ΓSpecIso_obj_hom, Scheme.Opens.ι_app_self]
+  simp only [asIso_inv, Scheme.comp_coeBase, Opens.map_comp_obj, Scheme.Opens.topIso_inv,
+    Opens.map_top, Functor.id_obj, Functor.comp_obj,
+    Functor.rightOp_obj, Scheme.Γ_obj, unop_op, Scheme.Spec_obj, Scheme.Opens.topIso_hom,
+    Category.assoc]
+  rw [← Functor.map_comp_assoc, ← op_comp, eqToHom_trans, Scheme.Opens.eq_presheaf_map_eqToHom,


The slowdown on this file comes from this proof and it will be improved in a later PR where the unit of the gamma-spec adjunction is specialized and be provided dedicated API.

This whole proof can be solved by a single simp only [many things are here] and the have can be deleted.

I am guessing the rw are unfolding things at default transparency that are very unpleasant. At least with simp, you can control the unfolding a bit more

Do you mean introducing intermediate lemmas? I'm not sure how to make this work.

Okay I managed to condense it into two blobs of simp and removed the nolint and the maxheartbeat.

Hmm. I think it is supposed to operate at reducible but I can't tell if it is doing anything atm

The actual substitution via kabstract is done at reducible transparency but there is at least one other isDefEq call that is done at default. So we start unfolding these more than is desired here

Is that intended? If this happens to rw everywhere, it sounds like a performance hazard to me.

With the huge caveat that I just looked at the file for a couple of minutes, no.

I'll check on this at office hours tomorrow at the latest

…lib4 into erd1/schemeOpens2

mattrobball · 2024-07-23T20:14:55Z

You might be able to improve your performance by removing the attribute making Quiver.Hom reducible at the start of AffineScheme. It doesn't seem to do anything except make Lean work harder now

erdOne · 2024-07-23T20:44:22Z

!bench

leanprover-bot · 2024-07-23T21:09:11Z

Here are the benchmark results for commit 5916387.
There were significant changes against commit d9ce431:

  Benchmark                                    Metric         Change
  ==================================================================
+ ~Mathlib.AlgebraicGeometry.AffineScheme      instructions   -35.1%
+ ~Mathlib.AlgebraicGeometry.Morphisms.Basic   instructions   -46.0%
+ ~Mathlib.AlgebraicGeometry.Restrict          instructions   -59.2%
+ ~Mathlib.AlgebraicGeometry.Scheme            instructions   -21.7%

mattrobball · 2024-07-23T21:11:39Z

Ready to go?

erdOne · 2024-07-23T21:13:04Z

Yes. Thanks! The improvements mentioned above will come in a later PR.

mattrobball · 2024-07-23T21:13:23Z

bors merge

Introduced `Scheme.Opens` as the type of open sets of a scheme. Provided `instance : CoeOut X.Opens Scheme` to replace the notation `X ∣_ᵤ U`, and renamed `Scheme.ιOpens` to `Scheme.Opens.ι` to enable dot notation. Co-authored-by: Andrew Yang <[email protected]>

mathlib-bors · 2024-07-23T21:23:33Z

Pull request successfully merged into master.

Build succeeded:

refactor(AlgebraicGeometry): Introduce Scheme.Opens.

17386bd

erdOne added 13 commits July 22, 2024 14:53

fix

cbf4058

fix

889bb33

fix

d37c66d

fix

453ab00

better fix

277e5fc

fix

3d0e8d1

fix

f057ce6

fix

3b3da22

move

9e12f85

fix

7db9486

fix

5ab4261

fixy fix

3f63774

fix

89bba21

erdOne added 3 commits July 22, 2024 18:05

fix lint

4b39650

fix

c08f944

fix

2fc3307

erdOne mentioned this pull request Jul 22, 2024

refactor(AlgebraicGeometry): Introduce Scheme.Opens. #14947

Closed

erdOne requested a review from chrisflav July 22, 2024 10:42

erdOne added the t-algebraic-geometry Algebraic geometry label Jul 22, 2024

chrisflav reviewed Jul 23, 2024

View reviewed changes

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

Apply suggestions from code review

07ad10e

Co-authored-by: Christian Merten <[email protected]>

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

Apply suggestions from code review

9886064

Co-authored-by: Christian Merten <[email protected]>

chrisflav approved these changes Jul 23, 2024

View reviewed changes

erdOne commented Jul 23, 2024

View reviewed changes

erdOne added 3 commits July 24, 2024 03:49

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

5514352

…lib4 into erd1/schemeOpens2

fix

e37c45b

fix proof

f97838f

erdOne added 2 commits July 24, 2024 04:27

fix

855ac33

fix

5916387

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 23, 2024

mathlib-bors bot changed the title ~~refactor(AlgebraicGeometry): Introduce Scheme.Opens.~~ [Merged by Bors] - refactor(AlgebraicGeometry): Introduce Scheme.Opens. Jul 23, 2024

mathlib-bors bot closed this Jul 23, 2024

mathlib-bors bot deleted the erd1/schemeOpens2 branch July 23, 2024 21:23

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): Introduce `Scheme.Opens`. #15001

[Merged by Bors] - refactor(AlgebraicGeometry): Introduce `Scheme.Opens`. #15001

erdOne commented Jul 22, 2024 •

edited by mattrobball

Loading

github-actions bot commented Jul 22, 2024 •

edited

Loading

Declarations diff

erdOne commented Jul 22, 2024

leanprover-bot commented Jul 22, 2024

erdOne commented Jul 22, 2024

leanprover-bot commented Jul 22, 2024

chrisflav left a comment

chrisflav Jul 23, 2024

erdOne Jul 23, 2024

chrisflav left a comment

chrisflav Jul 23, 2024

erdOne Jul 23, 2024 •

edited

Loading

chrisflav left a comment

erdOne Jul 23, 2024

mattrobball Jul 23, 2024

mattrobball Jul 23, 2024

erdOne Jul 23, 2024

erdOne Jul 23, 2024

mattrobball Jul 23, 2024

mattrobball Jul 23, 2024 •

edited

Loading

erdOne Jul 23, 2024

mattrobball Jul 23, 2024

mattrobball Jul 23, 2024

mattrobball commented Jul 23, 2024 •

edited

Loading

erdOne commented Jul 23, 2024

leanprover-bot commented Jul 23, 2024

mattrobball commented Jul 23, 2024

erdOne commented Jul 23, 2024

mattrobball commented Jul 23, 2024

mathlib-bors bot commented Jul 23, 2024

		def Scheme.openCoverOfSuprEqTop {s : Type*} (X : Scheme.{u}) (U : s → X.Opens)
		(hU : ⨆ i, U i = ⊤) : X.OpenCover where

[Merged by Bors] - refactor(AlgebraicGeometry): Introduce Scheme.Opens. #15001

[Merged by Bors] - refactor(AlgebraicGeometry): Introduce Scheme.Opens. #15001

Conversation

erdOne commented Jul 22, 2024 • edited by mattrobball Loading

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

PR summary 5916387248

Import changes for modified files

Declarations diff

erdOne commented Jul 22, 2024

leanprover-bot commented Jul 22, 2024

erdOne commented Jul 22, 2024

leanprover-bot commented Jul 22, 2024

chrisflav left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrisflav left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erdOne Jul 23, 2024 • edited Loading

Choose a reason for hiding this comment

chrisflav left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mattrobball Jul 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mattrobball commented Jul 23, 2024 • edited Loading

erdOne commented Jul 23, 2024

leanprover-bot commented Jul 23, 2024

mattrobball commented Jul 23, 2024

erdOne commented Jul 23, 2024

mattrobball commented Jul 23, 2024

mathlib-bors bot commented Jul 23, 2024

[Merged by Bors] - refactor(AlgebraicGeometry): Introduce `Scheme.Opens`. #15001

[Merged by Bors] - refactor(AlgebraicGeometry): Introduce `Scheme.Opens`. #15001

erdOne commented Jul 22, 2024 •

edited by mattrobball

Loading

github-actions bot commented Jul 22, 2024 •

edited

Loading

erdOne Jul 23, 2024 •

edited

Loading

mattrobball Jul 23, 2024 •

edited

Loading

mattrobball commented Jul 23, 2024 •

edited

Loading