[Merged by Bors] - feat(CategoryTheory): equality of morphisms can be checked on a cover

[chrisflav]

We show that equality of two morphisms can be checked on a cover for a topology for which isomorphisms are local at the target.

---

[github-actions]

PR summary acb12fd5f8

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.MorphismProperty.Descent	632	633	+1 (+0.16%)
Mathlib.CategoryTheory.MorphismProperty.Local	640	641	+1 (+0.16%)

Import changes for all files

Files

Import difference

36 files Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Stalk Mathlib.CategoryTheory.MorphismProperty.Descent Mathlib.CategoryTheory.MorphismProperty.Local Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

1

---

Declarations diff

+ eq_of_isomorphisms_descendsAlong
+ eq_of_zeroHypercover_target
+ equalizerPullbackMapIso
+ equalizerPullbackMapIso_hom_fst
+ equalizerPullbackMapIso_hom_snd
+ equalizerPullbackMapIso_inv_ι_fst
+ equalizerPullbackMapIso_inv_ι_snd
+ faithful_overPullback_of_isomorphisms_descendAlong

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 scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[erdOne]

Can you state it in terms of the fact that Over.pullback is faithful?

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step