Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 10 commits into
base: master
Choose a base branch
from

Conversation

erdOne
Copy link
Member

@erdOne erdOne commented Oct 27, 2024


Open in Gitpod

Copy link

github-actions bot commented Oct 27, 2024

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.

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 27, 2024
@erdOne erdOne added the t-category-theory Category theory label Oct 27, 2024
Copy link
Collaborator

@chrisflav chrisflav left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice result!

Mathlib/Algebra/Category/Ring/Epi.lean Show resolved Hide resolved
@chrisflav chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 29, 2024
@erdOne erdOne removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 29, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 29, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants