feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

[erdOne]

---

• [ ] depends on: #14429

[github-actions[bot]]

PR summary 096443bc5e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.AlgebraicGeometry.IsOpenImmersion.of_isLocalization + coprodIsoSigma + coprodMk + coprodMk_inl + coprodMk_inr + coprodOpenCover.{w} + coprodSpec + coprodSpec_apply + coprodSpec_coprodMk + coprodSpec_inl + coprodSpec_inr + fst_opProdIsoCoprod_hom + inl_opProdIsoCoprod_inv + inr_opProdIsoCoprod_inv + instance (R S : CommRingCatᵒᵖ) : IsIso (coprodComparison Scheme.Spec R S) := by + instance : HasBinaryCoproduct (op A) (op B) := by + instance : IsIso (coprodSpec R S) := by + instance : IsOpenImmersion (coprod.inl : X ⟶ X ⨿ Y) := by + instance : IsOpenImmersion (coprod.inr : Y ⟶ X ⨿ Y) := by + instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec := by + instance : PreservesColimitsOfShape (Discrete WalkingPair) Scheme.Spec + instance [Finite ι] (R : ι → CommRingCat) : IsIso (sigmaSpec R) := by + instance [Finite ι] [∀ i, IsAffine (f i)] : IsAffine (∐ f) + instance [IsAffine X] [IsAffine Y] : IsAffine (X ⨿ Y) + instance {J : Type*} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec + instance {J} [Fintype J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec + isCompl_opensRange_inl_inr + isCompl_range_inl_inr + isIso_stalkMap_coprodSpec + opProdIsoCoprod + opProdIsoCoprod_hom_fst + opProdIsoCoprod_hom_snd + opProdIsoCoprod_inv_inl + opProdIsoCoprod_inv_inr + sigmaSpec + snd_opProdIsoCoprod_hom + ι_left_coprodIsoSigma_inv + ι_right_coprodIsoSigma_inv + ι_sigmaSpec - IsOpenImmersion.of_isLocalization

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#14429~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Canceled.

[erdOne]

good to go now.

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5deb987a91935b7113b152f313d1b23c43332fca. There were significant changes against commit 9c47f211ae5ce5b4778d963e30d433dfb96eb390:

  Benchmark                           Metric         Change
  =========================================================
- ~Mathlib.AlgebraicGeometry.Limits   instructions    80.1%

[erdOne]

!bench

[leanprover-bot]

Here are the benchmark results for commit f8938e93976da25c351c96ffb047f6629b7b50f6. There were significant changes against commit 9c47f211ae5ce5b4778d963e30d433dfb96eb390:

  Benchmark                           Metric         Change
  =========================================================
- ~Mathlib.AlgebraicGeometry.Limits   instructions    45.2%

[erdOne]

!bench

[leanprover-bot]

Here are the benchmark results for commit 096443bc5eb5cbb6c47128a9f85b977fae4b5dcf. There were significant changes against commit 9c47f211ae5ce5b4778d963e30d433dfb96eb390:

  Benchmark                           Metric         Change
  =========================================================
- ~Mathlib.AlgebraicGeometry.Limits   instructions    39.6%

[erdOne]

I think this is the best I can do. @mattrobball any thoughts?

[mattrobball]

• Did you check there are no particular pain points (eg a tactic or instance synthesis that is mainly responsible)?
• Did the file get 40% longer?

[erdOne]

1. There are two defs that aren't instant but the slowness seems to be spread evenly through tactics.
2. The file length is almost 2x

So I think it's fine?

[mattrobball]

Yeah

[mattrobball]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style