feat(Algebra/Category): for ring homs, epi + finite => surjective

[erdOne]

---

[github-actions]

PR summary 238a276d94

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.TensorProduct.Basic	1042	1054	+12 (+1.15%)
Mathlib.RingTheory.Finiteness	1020	1031	+11 (+1.08%)
Mathlib.RingTheory.Ideal.IsPrincipal	1085	1093	+8 (+0.74%)

Import changes for all files

Files	Import difference
109 files Mathlib.Topology.Algebra.Module.Simple Mathlib.RingTheory.Henselian Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.RingTheory.SimpleModule Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.RingTheory.Artinian Mathlib.Algebra.Lie.Quotient Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Lagrange Mathlib.Algebra.Lie.Submodule Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.RingTheory.Derivation.Lie Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.Topology.Compactification.OnePointEquiv Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.RingTheory.Norm.Defs Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Algebra.Lie.Free Mathlib.RingTheory.Ideal.Cotangent Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.Algebra.Lie.DirectSum Mathlib.LinearAlgebra.FiniteDimensional Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.Algebra.LinearRecurrence Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.Algebra.Lie.SkewAdjoint Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.Algebra.Lie.Matrix Mathlib.Analysis.Convex.Between Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.Algebra.Lie.Abelian Mathlib.FieldTheory.Finiteness Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.Algebra.Module.Torsion Mathlib.Topology.Instances.Matrix Mathlib.Algebra.Jordan.Basic Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Algebra.Lie.Derivation.Basic Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Topology.Algebra.Module.Determinant Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Algebra.Lie.Subalgebra Mathlib.Algebra.Lie.Sl2 Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.Algebra.Lie.Solvable Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Algebra.Category.ModuleCat.Free Mathlib.RingTheory.FiniteLength Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.Algebra.Lie.Classical Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.RingTheory.Localization.Cardinality Mathlib.LinearAlgebra.Dimension.Finite Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Lie.TensorProduct Mathlib.RepresentationTheory.Maschke Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.Algebra.Lie.OfAssociative Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.Data.Nat.Factorial.SuperFactorial	-1
24 files Mathlib.NumberTheory.MulChar.Lemmas Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Localization.Finiteness Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.EssentialFiniteness Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.SurjectiveOnStalks Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Analysis.NormedSpace.DualNumber Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.RingHom.Surjective Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Normed.Algebra.UnitizationL1	1
3 files Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Homology.LocalCohomology	4
10 files Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent	5
32 files Mathlib.Topology.ContinuousMap.Polynomial Mathlib.RingTheory.Flat.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Data.Nat.Choose.Lucas Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Data.ZMod.Coprime Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.RingTheory.Flat.Algebra Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.NumberTheory.PythagoreanTriples Mathlib.RingTheory.ZMod Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Topology.Algebra.Polynomial Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Tactic.ReduceModChar Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.NumberTheory.PrimeCounting Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.RingTheory.Flat.Stability Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Free	6
15 files Mathlib.RingTheory.QuotSMulTop Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Algebra.Module.FinitePresentation Mathlib.NumberTheory.VonMangoldt Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.Sheaves.Sheafify	7
45 files Mathlib.Algebra.Polynomial.FieldDivision Mathlib.RingTheory.Polynomial.Content Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.RingTheory.Lasker Mathlib.Algebra.Category.Ring.Instances Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.NumberTheory.ArithmeticFunction Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.Polynomial.Splits Mathlib.FieldTheory.Minpoly.Basic Mathlib.Data.Nat.Squarefree Mathlib.Algebra.CubicDiscriminant Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.Noetherian Mathlib.RingTheory.Localization.Away.Basic Mathlib.NumberTheory.PellMatiyasevic Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Polynomial.Expand Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Radical Mathlib.RingTheory.Adjoin.Tower Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.RingTheory.Adjoin.FG Mathlib.NumberTheory.SmoothNumbers Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.RingTheory.ChainOfDivisors Mathlib.RingTheory.Polynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.NumberTheory.MaricaSchoenheim Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.RingTheory.UniqueFactorizationDomain Mathlib.NumberTheory.Dioph Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Bezout Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.FieldTheory.Tower Mathlib.NumberTheory.FLT.Basic Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.FieldTheory.RatFunc.Basic Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic	8
19 files Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.RingTheory.Localization.BaseChange Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.Basic Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Geometry.RingedSpace.Stalks Mathlib.RingTheory.RingHomProperties Mathlib.Topology.Sheaves.Operations Mathlib.Algebra.Category.Ring.Constructions Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Topology.Sheaves.Stalks Mathlib.LinearAlgebra.TensorProduct.Vanishing	9
19 files Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.RingTheory.Coalgebra.Hom Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.Module.Basic Mathlib.RingTheory.OrzechProperty Mathlib.Algebra.Category.CoalgebraCat.Monoidal Mathlib.RingTheory.Coalgebra.Equiv Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.RingTheory.Finiteness Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.Algebra.Polynomial.Module.AEval	11
16 files Mathlib.Algebra.Module.Bimodule Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.PolynomialAlgebra Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.RingTheory.HopfAlgebra Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.Bialgebra.Equiv Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial	12
Mathlib.Algebra.Category.Ring.Epi	1162

---

Declarations diff

+ CommRingCat.epi_iff_tmul_eq_tmul
+ Module.exists_isPrincipal_quotient_of_finite
+ Module.exists_surjective_quotient_of_finite
+ RingHom.surjective_iff_epi_and_finite
+ RingHom.surjective_of_epi_of_finite
+ RingHom.surjective_of_tmul_eq_tmul_of_finite
+ instance : Nontrivial (M ⊗[R] M) := by

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.

[chrisflav]

Nice result!