Skip to content

feat(RingTheory/Flat/FaithfullyFlat/Basic): prove IsNoetherian and IsArtinian from faithfully flat base change#37104

Open
tb65536 wants to merge 7 commits intoleanprover-community:masterfrom
tb65536:tb_basechange
Open

feat(RingTheory/Flat/FaithfullyFlat/Basic): prove IsNoetherian and IsArtinian from faithfully flat base change#37104
tb65536 wants to merge 7 commits intoleanprover-community:masterfrom
tb65536:tb_basechange

Conversation

@tb65536
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 commented Mar 24, 2026 •
edited
Loading

This PR proves that if the base change of a module M along a faithfully flat ring homomorphism is Noetherian or Artinian, then so is M.

The file Artinian/Module has become rather heavy, so I split off a Artinian/Defs file to avoid the large import.

Open in Gitpod

@tb65536 tb65536 added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory labels Mar 24, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 24, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 24, 2026 •
edited
Loading

PR summary 1cc67e6e43

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
227 files Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.Ring.EqualizerPushout Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Lie.Abelian Mathlib.Algebra.Lie.AdjointAction.Basic Mathlib.Algebra.Lie.AdjointAction.Derivation Mathlib.Algebra.Lie.BaseChange Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Cochain Mathlib.Algebra.Lie.Derivation.BaseChange Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.DirectSum Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.Extension Mathlib.Algebra.Lie.Free Mathlib.Algebra.Lie.Graded Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Lie.Ideal Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Loop Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Normalizer Mathlib.Algebra.Lie.OfAssociative Mathlib.Algebra.Lie.Prod Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.SemiDirect Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.SerreConstruction Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.Subalgebra Mathlib.Algebra.Lie.Submodule Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.LieRinehartAlgebra.Defs Mathlib.Algebra.Symmetrized Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.SingularValues Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.PurelyInseparable.Tower Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.LinearAlgebra.Semisimple Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RepresentationTheory.AlgebraRepresentation.Basic Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.Irreducible Mathlib.RingTheory.AdicCompletion.Completeness Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.Artinian.Algebra Mathlib.RingTheory.Artinian.Instances Mathlib.RingTheory.Artinian.Module Mathlib.RingTheory.Artinian.Ring Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Derivation.Lie Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.FiniteLength Mathlib.RingTheory.Finiteness.Descent Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.KrullDimension.LocalRing Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.Length Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Polynomial Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.SimpleModule.WedderburnArtin Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.LTSeries Mathlib.RingTheory.Spectrum.Prime.Noetherian Mathlib.RingTheory.Spectrum.Prime.Polynomial Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Dedekind Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.LocalStructure Mathlib.RingTheory.ZariskisMainTheorem Mathlib.Topology.Algebra.Ring.Compact
 1
Mathlib.RingTheory.Artinian.Defs (new file) 469

Declarations diff

+ IsArtinian.induction
+ IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
+ IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
+ baseChangeOrderEmbedding
+ baseChange_inj
+ baseChange_injective
+ baseChange_le_iff
+ baseChange_mono
- induction

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 24, 2026
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 24, 2026
robin-carlier
robin-carlier reviewed Apr 3, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier left a comment

Choose a reason for hiding this comment

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

Apart from name bikeshedding, this is very nice!

Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean Outdated
Comment on lines +636 to +641
theorem IsNoetherian.ofFaithfullyFlat (h : IsNoetherian A (A ⊗[R] M)) : IsNoetherian R M := by
rw [isNoetherian_iff'] at h ⊢
exact (baseChangeOrderEmbedding R M A).wellFoundedGT

theorem IsArtinian.ofFaithfullyFlat (h : IsArtinian A (A ⊗[R] M)) : IsArtinian R M :=
(baseChangeOrderEmbedding R M A).wellFoundedLT
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier Apr 3, 2026

Choose a reason for hiding this comment

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

I’m not 100% convinced by the naming here. We have

Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat and Module.Finite.of_finite_tensorProduct_of_faithfullyFlat for similar properties.
That’s rather long names, but I think we should follow the pattern and call these IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
and IsNoetherian.of_isArtinian_tensorProduct_of_faithfullyFlat

@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026
@tb65536 tb65536 added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 3, 2026
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-carlier robin-carlier robin-carlier left review comments

Assignees

No one assigned

Labels

t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@tb65536 @robin-carlier