Strong rank condition for commutative rings

Stream: maths

[Riccardo Brasca]

Is anyone (especially @Scott Morrison ) working on the strong rank condition for commutative rings? I would like to do it, this proof seems pretty Leanable.

[Kevin Buzzard]

I am insulted that you're not formalising my proof ;-)

[Riccardo Brasca]

You should first of all write the relevant API :laughing:

[Kevin Buzzard]

PS it is good that you are maintaining the truth of my claim that every few years this question re-appears in my life.

[Scott Morrison]

I didn't do it, and am not currently working on it.

[Scott Morrison]

However I did already prove that all noetherian rings satisfy the SRC, whether they are commutative or not.

[Scott Morrison]

https://mathoverflow.net/a/2574 gives a fairly cheap proof that you can get from this fact to the SRC for any commutative ring.

It just uses the Hilbert basis theorem.

[Scott Morrison]

I suspect this may be the path of least resistance from the current state of mathlib.

[Scott Morrison]

You don't need to use any API to translate to systems of linear equations. Step 2 of the linked mathoverflow answer can be compiled down to:

Let M be a linear map A^n to A^m. Let B be the subring of A generated by the matrix components of M. This is noetherian, being a quotient of the polynomial ring \int[M_ij]. Let M' be the linear map from B^n to B^m, whose matrix components are identical to M.

Claim: if M is injective, so is M'.

Then n \le m follows from the SRC for B, already established.

[Scott Morrison]

The claim follows trivially from the commuting square with vertical maps the inclusions B^i to A^i, sand horizontal maps M and M'.

[Riccardo Brasca]

I was thinking of using https://mathoverflow.net/a/47846/7845, it seems very Leanable (we have Cayley-Hamilton in full generality).

[Scott Morrison]

Alternatively, we should take this as an opportunity to develop exterior algebras properly, because that proof is the best proof. :-)

[Kevin Buzzard]

(looks sadly at Amelia's MSc koszul_cx branch which she never PR'ed...)

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/0d723cf1f12ac7eb57cab4f6a786a6bd5316ad5f/src/m4r/exterior_power.lean#L15

[Scott Morrison]

I do like the CH proof. Happily it factors into separate pieces: prove first that the minimal polynomial of any injective endomorphism has nonzero constant term.

[Riccardo Brasca]

I have a short proof of the strong rank condition for commutative rings (you need #9128 and #9280 to play with it):

import linear_algebra.charpoly
import linear_algebra.invariant_basis_number

variables {R : Type*} [comm_ring R] [nontrivial R]

open polynomial function fin nat linear_map

lemma comm_ring_strong_rank_condition : strong_rank_condition R :=
begin
  apply (strong_rank_condition_iff_succ R).2 (λ n f hf, _),

--(A generalization of) This should be a global instance
  letI := module.finite.of_basis (pi.basis_fun R (fin (n + 1))),

  let g := (extend_by_zero.linear_map R cast_succ).comp f,
  have hg : injective g :=
    (extend_injective (rel_embedding.injective cast_succ) 0).comp hf,
  have hnex : ¬∃ i : fin n, fin.cast_succ i = fin.last n :=
    λ ⟨i, hi⟩, ne_of_lt (fin.cast_succ_lt_last i) hi,
  let heval := minpoly.aeval R g,
  obtain ⟨P, hP⟩ := X_dvd_iff.2 (erase_same (minpoly R g) 0),
  rw [← monomial_add_erase (minpoly R g) 0, hP, linear_map.ext_iff] at heval,
  replace heval := congr_fun (heval (pi.single (fin.last n) 1)) (fin.last n),
  simpa [hnex, charpoly_coeff_zero_of_injective hg] using heval
end

I am going to PR it soon.

[Scott Morrison]

Want to intersperse a human-readable proof as comments? :-)

[Riccardo Brasca]

It's the proof in https://mathoverflow.net/a/47846/7845

[Scott Morrison]

At very least add that link. But line-by-line comments are even better! Perhaps this is a conversation for another thread, but I think we should aspire to a mathlib-wide expectation that non-trivial proofs have human readable accounts either in the doc-string or as interspersed comments. (I'm not claiming I attain this standard: but I'd be happy to have community pressure to do so. :-)

[Yaël Dillies]

I tried doing it here. What do you think? Should this interspersed instead? https://github.com/leanprover-community/mathlib/pull/8112/files#diff-4c34222b20f057aded6aed74074908860a3035426480c5905e894918f61bc8da

[Reid Barton]

I think a docstring per Lean definition is usually best.

[Reid Barton]

Or a top-level comment describing the overall proof if it is split up into top-level definitions.

[Reid Barton]

It doesn't have to be a docstring, really.

[Reid Barton]

In your PR, if you move those two numbered lists of proof steps to before the corresponding lemmas, then I think it's perfect

[Yaël Dillies]

Okay :smile:
Personally I kind of like the idea of leaving uncluttered the list of declarations. But in that case that list is very short anyway.

[Reid Barton]

Do you mean in the generated documentation?

[Yaël Dillies]

Yes

[Reid Barton]

I think there's no need to make the proofs into docstrings. When do you need to see the human proof, really? Presumably it's exactly when you are trying to decipher the Lean proof. In that case, it should go adjacent to the proof but not in a docstring.

[Yaël Dillies]

Okay there's definitely room for discussion :thinking:

[Patrick Massot]

I agree with Reid.

[Eric Wieser]

It probably makes sense to reference the mathoverflow proof in the docstring if it explains an unexpected choice of assumptions, but I agree the docstring is not the place for walking through the proof.

[Reid Barton]

As for line-by-line or not, it depends on the proof, but on balance, I think it's easier to understand the human proof if it can be summarized in a few lines up front like in @Yaël Dillies's PR, rather than interspersed with the Lean proof. Not a strong preference though.

[Reid Barton]

Maybe it's because I usually don't use a big monitor.

[Reid Barton]

If sentences of the human proof are getting split up across lines of the Lean proof, it's too fine-grained. If there are 15 lines of human proof above 100 lines of Lean proof, it's too coarse-grained.

[Scott Morrison]

I agree splitting sentences across proof lines is bad. I've done this in the past and looking back on them they are not so helpful.

[Reid Barton]

Upon further reflection, my revised opinion on the line-by-line aspect is that comments with the human proof are good and whatever style the author of the code prefers is fine. I don't think it's the sort of thing where a policy or standard format is necessary.

[Scott Morrison]

The policy "more words" is probably worthwhile. :-)

[Riccardo Brasca]

Sorry for the late answer.

I will surely add the link to the mathoverflow answer and some explanation about the proof (it's really simple, but in my opinion it is almost original math, I have no idea if the author found it by himself or it is a known proof, but it was good enough to get the "populist" badge on mathoverflow, that is quite rare).

I will open a WIP PR since I need to modify/split some files: to prove the strong rank condition I need the characteristic polynomial of an endomorphism, but to prove that the characteristic polynomial does not depend on the choice of the base I need (at least, in the proof I have) the two basis have the same cardinalities (the invariant basis number property, that follows from strong rank condition). There are no logical problems, since the strong rank condition can be proved without knowing that the polynomial is independent of the choice of the basis, but I have to think about how to write this in mathlib.

[Riccardo Brasca]

Does anyone have a suggestion for a good place for comm_ring_strong_rank_condition?

The natural file is of course linear_algebra.invariant_basis_number, but to prove the result I use the characteristic polynomial in linear_algebra.charpoly, that imports linear_algebra.invariant_basis_number (currently through linear_algebra.free_module, linear_algebra.matrix.to_lin, linear_algebra.matrix.finite_dimensional, linear_algebra.finite_dimensional, field_theory.finiteness, linear_algebra.dimension, linear_algebra.invariant_basis_number). I don't see any way of avoiding linear_algebra.matrix.to_lin, so this cannot be solved just by splitting linear_algebra.free_module (this is anyway a sensible thing to do, as in #9407).

[Anne Baanen]

If there's no obvious place to put it while preserving the imports, making a new file isn't too bad.

[Riccardo Brasca]

#9486