feat: add Orzech's theorem `(IsNoetherian|Module.Finite).injective_of_surjective_of_injective`

[acmepjz]

... which state that if

• R is a ring (not necessarily commutative) and M is a Noetherian R-module (based on the proof in https://math.stackexchange.com/a/1066128), or
• R is a commutative ring and M is a finitely generated R-module (based on the proof in https://math.stackexchange.com/a/1066110),

if N is a submodule of M, f : N -> M is a surjective R-module homomorphism, then it is also injective.

These results generalizes (IsNoetherian|Module.Finite).injective_of_surjective_endomorphism.

This property is abstracted as OrzechProperty and which implies StrongRankCondition for nontrivial rings. The proof of Noetherian rings and commutative rings satisfying StrongRankCondition is changed accordingly.

NOTE: reason to change the imports to several files:

Warning: ././././Mathlib/RingTheory/FiniteType.lean:7:1: warning: unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
././././Mathlib/RingTheory/FiniteType.lean:
  remove #[Mathlib.Algebra.Polynomial.Module.Basic]
  instead
    import [Mathlib.Algebra.Polynomial.Module.Basic] in Mathlib.LinearAlgebra.AnnihilatingPolynomial
Warning: ././././Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean:6:1: warning: unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
Warning: ././././Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean:7:1: warning: import #[Mathlib.RingTheory.FiniteType] instead
././././Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean:
  remove #[Mathlib.LinearAlgebra.Charpoly.Basic]
  add #[Mathlib.RingTheory.FiniteType]
  instead
    import [Mathlib.RingTheory.Ideal.LocalRing] in Mathlib.LinearAlgebra.Dual
    import [Mathlib.RingTheory.Ideal.LocalRing] in Mathlib.FieldTheory.Tower
    import [Mathlib.RingTheory.Algebraic, Mathlib.FieldTheory.Minpoly.Basic] in Mathlib.FieldTheory.IntermediateField
    import [Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff] in Mathlib.LinearAlgebra.Trace
    import [Mathlib.RingTheory.Ideal.LocalRing] in Mathlib.Topology.Algebra.Module.FiniteDimension
    import [Mathlib.LinearAlgebra.Dimension.Constructions] in Mathlib.LinearAlgebra.FreeModule.IdealQuotient
    import [Mathlib.LinearAlgebra.Dimension.StrongRankCondition] in Mathlib.LinearAlgebra.FreeAlgebra

---

discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312076.20Orzech's.20theorem

[acmepjz]

I've checked that IsNoetherian.injective_of_surjective_of_injective could be moved to Mathlib.LinearAlgebra.InvariantBasisNumber, but not Module.Finite.injective_of_surjective_of_injective, since Hilbert basis theorem is not imported by that file.

[AntoineChambert-Loir]

Then it would be nice to have a Orzech file that proves that theorem. It will be small to start with, but additions will be possible.

[acmepjz]

Then it would be nice to have a Orzech file that proves that theorem. It will be small to start with, but additions will be possible.

My idea is nuke the contents of the file Mathlib.LinearAlgebra.FreeModule.StrongRankCondition, replace commRing_strongRankCondition by commRing_orzechProperty. Combined with strongRankCondition_of_orzechProperty it recovers the original commRing_strongRankCondition.

[acmepjz]

Regarding the import problem, I just blindly apply the suggestions from the linter. Let me check later.

[acmepjz]

Unfortunately, but after removing imports those files can't be compiled. :(

[AntoineChambert-Loir]

There is one thing that confuses me now: There are many files with versions of Orzech's theorem, and it is not clear to me that all of them are needed now. Why not add instances whenever possible instead of in StrongRankCondition? and state them using the Orzech property? Moreover, they probably do not need a grand explanation and references once the Orzech property is mentioned.

[acmepjz]

There is one thing that confuses me now: There are many files with versions of Orzech's theorem, and it is not clear to me that all of them are needed now. Why not add instances whenever possible instead of in StrongRankCondition? and state them using the Orzech property? Moreover, they probably do not need a grand explanation and references once the Orzech property is mentioned.

Basically there are two, one is for IsNoetherian, another one is for Module.Finite and commutative rings.

I think the IsNoetherian one cannot be removed, since it assumes nothing on the ring, but only assumes the module being Noetherian. So it implies Noetherian ring satisfies OrzechProperty, but not vice versa.

The Module.Finite one could probably be removed since it just said that commutative ring satisfies OrzechProperty. But there are some dependency problem, because the file defining OrzechProperty is not imported yet...

Maybe the OrzechProperty should be in a separate file, without InvariantBasisNumber etc.? I think it could be better since to define OrzechProperty we probably don't need the following two imports in InvariantBasisNumber:

import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.PrincipalIdealDomain

[jcommelin]

I put your "NOTE" below the fold, because I don't think it should end up in the commit message

[AntoineChambert-Loir]

You can try that, yes. The point is that I was confused yesterday night about all these versions, and was basically unable to sort out which was which. I don't believe it's a problem to delegate one theorem such as this one or the IBN to a specific file. If you have one for Orzech, and one for IBN+RC+SRC, that should look clean, except that the latter will plainly import Orzech and conclude, and Orzech is short. The important thing to me is to be sure that there are no duplicate proofs. (BTW, there could be a Orzech property for modules: for all submodules N...)

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13322~~
• ~~leanprover-community/mathlib4#13425~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style