feat(AlgebraicGeometry): integral = universally closed + affine

[erdOne]

as a corollary, finite = proper + affine

---

[github-actions]

PR summary ed6b24e956

Import changes exceeding 2%

%	File
+6.50%	Mathlib.AlgebraicGeometry.Morphisms.Integral

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.Morphisms.Integral	1847	1967	+120 (+6.50%)
Mathlib.Algebra.Category.Ring.Constructions	1295	1305	+10 (+0.77%)
Mathlib.AlgebraicGeometry.Morphisms.Proper	1971	1977	+6 (+0.30%)
Mathlib.RingTheory.PolynomialAlgebra	998	999	+1 (+0.10%)

Import changes for all files

Files	Import difference
295 files Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.RingTheory.IsAdjoinRoot Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.FieldTheory.IsPerfectClosure Mathlib.NumberTheory.Wilson Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.PowerBasis Mathlib.FieldTheory.Finite.Trace Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.AlgebraicGeometry.EllipticCurve.J Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.RingTheory.WittVector.Domain Mathlib.FieldTheory.Laurent Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.LocalRing.Quotient Mathlib.Data.Real.GoldenRatio Mathlib.RingTheory.WittVector.InitTail Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.RingTheory.Localization.NormTrace Mathlib.FieldTheory.AbelRuffini Mathlib.RingTheory.ClassGroup Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.LinearAlgebra.PID Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.NumberField.Norm Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.FieldTheory.Isaacs Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.RingTheory.Trace.Basic Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.RingTheory.WittVector.MulCoeff Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Topology.Sheaves.CommRingCat Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.FieldTheory.Normal Mathlib.RingTheory.Jacobson Mathlib.RingTheory.WittVector.Identities Mathlib.FieldTheory.Adjoin Mathlib.RingTheory.Localization.Integral Mathlib.Algebra.Lie.Derivation.Killing Mathlib.FieldTheory.SeparableClosure Mathlib.RingTheory.WittVector.Truncated Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.LinearAlgebra.JordanChevalley Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.Analysis.Fourier.ZMod Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.AlgebraicGeometry.Spec Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.RingTheory.Nullstellensatz Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Trace Mathlib.AlgebraicGeometry.Over Mathlib.NumberTheory.NumberField.Completion Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.FieldTheory.Finite.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.FieldTheory.Extension Mathlib.NumberTheory.SumFourSquares Mathlib.Data.Real.Pi.Irrational Mathlib.LinearAlgebra.Semisimple Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.NumberTheory.Rayleigh Mathlib.FieldTheory.KrullTopology Mathlib.RingTheory.LittleWedderburn Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.RingTheory.PolynomialAlgebra Mathlib.FieldTheory.Relrank Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.FieldTheory.Galois.Profinite Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.FieldTheory.Finite.GaloisField Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.RingTheory.Algebraic Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Algebra.AlgebraicCard Mathlib.Data.Real.Irrational Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.FieldTheory.PrimitiveElement Mathlib.RingTheory.Smooth.Basic Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.RingTheory.Valuation.LocalSubring Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.SumTwoSquares Mathlib.Algebra.Module.PID Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.FieldTheory.Perfect Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.NumberTheory.JacobiSum.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.NumberTheory.KummerDedekind Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.AlgebraicIndependent Mathlib.NumberTheory.Pell Mathlib.FieldTheory.AlgebraicClosure Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.NumberTheory.NumberField.Basic Mathlib.FieldTheory.CardinalEmb Mathlib.RingTheory.WittVector.Basic Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.Analysis.Normed.Algebra.Basic Mathlib.RepresentationTheory.FDRep Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.RingTheory.WittVector.Isocrystal Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.RingTheory.Polynomial.Selmer Mathlib.FieldTheory.NormalClosure Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.NumberTheory.FermatPsp Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.LinearAlgebra.Matrix.LDL Mathlib.RingTheory.AdjoinRoot Mathlib.Algebra.Lie.Weights.Killing Mathlib.RingTheory.Smooth.Pi Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.AlgebraicGeometry.Scheme Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.FieldTheory.KummerExtension Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.AlgebraicGeometry.Gluing Mathlib.Topology.Instances.Irrational Mathlib.FieldTheory.Minpoly.Field Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.FieldTheory.JacobsonNoether Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.RingTheory.WittVector.Teichmuller Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.FieldTheory.PurelyInseparable Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Algebra.Lie.Weights.Cartan Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.RingTheory.Valuation.Minpoly Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Lie.Rank Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Algebra.Polynomial.Bivariate Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.AlgebraicGeometry.Restrict Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.AxGrothendieck Mathlib.Tactic Mathlib.FieldTheory.SplittingField.Construction Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.NormTrace Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.FieldTheory.RatFunc.Degree Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.RingTheory.Perfection Mathlib.RingTheory.Norm.Basic Mathlib.NumberTheory.FunctionField Mathlib.Algebra.DirectSum.LinearMap Mathlib.NumberTheory.DiophantineApproximation Mathlib.Topology.Instances.RatLemmas Mathlib.RingTheory.WittVector.MulP	1
Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Etale.Field	4
Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.ValuativeCriterion	6
38 files Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Localization.Finiteness Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.NumberTheory.Cyclotomic.Three Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Localization.Free Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.RingTheory.RingHom.Locally Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.LocalProperties.Basic Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.DedekindDomain.PID Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.AdeleRing	9
Mathlib.Algebra.Category.Ring.Constructions	10
Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Finite	120

---

Declarations diff

+ IsFinite.eq_isProper_inf_isAffineHom
+ IsFinite.iff_isProper_and_isAffineHom
+ eq_universallyClosed_inf_isAffineHom
+ iff_of_Spec
+ iff_universallyClosed_and_isAffineHom
+ instance (priority := 100) {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f] :
+ instance (priority := 900) [IsFinite f] : IsProper f
+ instance {R S} [CommRing R] [CommRing S] [Algebra R S] :
+ isPushout_of_isPushout
- instance (priority := 900) [IsClosedImmersion f] : IsProper f

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.

---

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]

About the large-import: Morphism/Integral is a leaf file that was added in the last PR.