feat(AlgebraicGeometry) use addMorphismPropertyInstances

[erdOne]

---

• depends on: feat(CategoryTheory): command that generates instances for MorphismProperty #18785

[github-actions]

PR summary a418de4f16

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.Cover.Open	1694	1702	+8 (+0.47%)
Mathlib.AlgebraicGeometry.Restrict	1697	1705	+8 (+0.47%)
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties	1731	1737	+6 (+0.35%)
Mathlib.AlgebraicGeometry.Morphisms.FiniteType	1740	1746	+6 (+0.34%)
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation	1753	1759	+6 (+0.34%)
Mathlib.AlgebraicGeometry.Morphisms.Smooth	1759	1765	+6 (+0.34%)

Import changes for all files

Files	Import difference
297 files Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.CategoryTheory.Sites.Pullback Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.CategoryTheory.Localization.HasLocalization Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Category.Grp.Subobject Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Condensed.Limits Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.CategoryTheory.Abelian.Ext Mathlib.RingTheory.Flat.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Condensed.TopComparison Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.CategoryTheory.Localization.FiniteProducts Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.Algebra.Category.Grp.AB5 Mathlib.RingTheory.Regular.RegularSequence Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.CategoryTheory.ConcreteCategory.EpiMono Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Condensed.Light.Explicit Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.MorphismProperty.Concrete Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Quasicategory Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Algebra.Category.Grp.Abelian Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.CategoryTheory.Sites.EpiMono Mathlib.AlgebraicTopology.CechNerve Mathlib.Condensed.Explicit Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Condensed.Discrete.Characterization Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Category.Grp.Kernels Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Condensed.Light.CartesianClosed Mathlib.CategoryTheory.Localization.Pi Mathlib.AlgebraicGeometry.Noetherian Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.CategoryTheory.Localization.Construction Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.CategoryTheory.Localization.Opposite Mathlib.CategoryTheory.Localization.HomEquiv Mathlib.AlgebraicGeometry.Spec Mathlib.RingTheory.Unramified.Field Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.AlgebraicGeometry.ResidueField Mathlib.CategoryTheory.Sites.InducedTopology Mathlib.RingTheory.Flat.Localization Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Algebra.Homology.Square Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.AlgebraicGeometry.Over Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.CategoryTheory.Sites.Localization Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.CategoryTheory.Localization.LocalizerMorphism Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Algebra.Category.Ring.Epi Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.RingTheory.Etale.Field Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.Order.Category.NonemptyFinLinOrd Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.RingTheory.Flat.Algebra Mathlib.CategoryTheory.Localization.Prod Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Condensed.Solid Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.Condensed.Discrete.Module Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Widesubcategory Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.AlgebraicTopology.SingularSet Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Gluing Mathlib.NumberTheory.MulChar.Duality Mathlib.Condensed.Light.Epi Mathlib.CategoryTheory.Abelian.Injective Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.Topology.Category.Profinite.Projective Mathlib.RepresentationTheory.Character Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.CategoryTheory.Galois.Decomposition Mathlib.LinearAlgebra.LinearDisjoint Mathlib.CategoryTheory.Abelian.Projective Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Geometry.RingedSpace.Basic Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.CategoryTheory.Localization.Adjunction Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Condensed.TopCatAdjunction Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.Algebra.Module.PID Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.CategoryTheory.Galois.Full Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Triangulated.Opposite Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.Algebra.Homology.Localization Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.CategoryTheory.MorphismProperty.Composition Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Algebra.Module.CharacterModule Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.CategoryTheory.Localization.Composition Mathlib.CategoryTheory.Sites.Equivalence Mathlib.Algebra.Category.Grp.Images Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.SimplexCategory Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.CategoryTheory.Shift.Localization Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.Geometry.RingedSpace.Stalks Mathlib.Condensed.Light.Limits Mathlib.Condensed.Discrete.Colimit Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.FDRep Mathlib.AlgebraicTopology.SimplicialObject Mathlib.Condensed.CartesianClosed Mathlib.Topology.Category.Stonean.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.AlgebraicGeometry.Scheme Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Topology.Sheaves.Functors Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.CategoryTheory.Sites.DenseSubsite Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Topology.Sheaves.Operations Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.CategoryTheory.Localization.SmallHom Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.RingTheory.LinearDisjoint Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.RingTheory.LocalRing.Module Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.CategoryTheory.Localization.StructuredArrow Mathlib.CategoryTheory.Localization.CalculusOfFractions Mathlib.CategoryTheory.Galois.Action Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.Condensed.Epi Mathlib.CategoryTheory.Localization.Predicate Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.Topology.Sheaves.PUnit Mathlib.Algebra.Category.ModuleCat.Free Mathlib.AlgebraicTopology.MooreComplex Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.RingTheory.Flat.Stability Mathlib.CategoryTheory.Sites.Adjunction Mathlib.Condensed.Functors Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Condensed.Equivalence Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.Grp.Injective Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.CategoryTheory.Localization.Resolution Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Topology.Sheaves.Sheafify Mathlib.RingTheory.Unramified.Finite Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.CategoryTheory.Localization.Equivalence Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Topology.Sheaves.Stalks Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.ConcreteCategory Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Topology.Category.Stonean.Limits Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.Algebra.Category.ModuleCat.Presheaf.Free	1
6 files Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.GluingOneHypercover	2
4 files Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType	6
8 files Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Restrict	8
Mathlib.CategoryTheory.MorphismProperty.Tactic	379

---

Declarations diff

+ Bar2
+ Config
+ ContainsIdentities
+ Foo.Bar
+ Foo.Bar3
+ IsStableUnderComposition
+ MorphismProperty.morphismRestrict
+ MorphismProperty.pullbackHom
+ addMorphismPropertyInstancesAux
+ comp_mem
+ getArgs
+ hom
+ instance : ContainsIdentities (@Foo.Bar n) := ⟨fun _ ↦ ⟨⟩⟩
+ instance : ContainsIdentities (@Foo.Bar3 C _) := ⟨fun _ ↦ ⟨⟩⟩
+ instance : IsStableUnderComposition (@Foo.Bar n) := ⟨fun _ _ _ _ ↦ ⟨⟩⟩
+ instance : IsStableUnderComposition (@Foo.Bar3 C _) := ⟨fun _ _ _ _ ↦ ⟨⟩⟩
+ instance : IsStableUnderComposition @Foo.Bar2 := ⟨fun _ _ _ _ ↦ ⟨⟩⟩
+ instance : MorphismProperty.IsMultiplicative @LocallyOfFinitePresentation
+ instance : MorphismProperty.IsMultiplicative @QuasiCompact
+ instance : MorphismProperty.IsMultiplicative @QuasiSeparated
+ instance : RespectsIso (@Foo.Bar n) := @RespectsIso.mk _ _ _ (fun _ _ _ ↦ ⟨⟩) (fun _ _ _ ↦ ⟨⟩)
+ lemma1
+ lemma2
+ lemma3
+ of_isIso
+++ foo
+++ instance {X} : Bar (𝟙 X)
- instance (f : X ⟶ Z) (g : Y ⟶ Z) [QuasiCompact f] : QuasiCompact (pullback.snd f g)
- instance (f : X ⟶ Z) (g : Y ⟶ Z) [QuasiCompact g] : QuasiCompact (pullback.fst f g)
- instance (priority := 900) quasiCompact_of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] :
- instance : MorphismProperty.IsStableUnderComposition @LocallyOfFinitePresentation
- instance [IsAffineHom f] [IsAffineHom g] : IsAffineHom (f ≫ g) := by
- instance {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) [IsOpenImmersion f] :
- instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated f] :
- instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated g] :
- instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmoothOfRelativeDimension 0 f]
- isSmooth_comp
- locallyOfFinitePresentation_comp
- quasiCompact_comp
- quasiCompact_isStableUnderComposition
- quasiSeparatedComp
- stableUnderComposition
- universallyClosedTypeComp
- universallyClosed_fst
- universallyClosed_snd

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(CategoryTheory): command that generates instances for MorphismProperty #18785
  By Dependent Issues (🤖). Happy coding!