!4#2887 Data.MvPolynomial.Monad

Stream: mathlib4

[Jireh Loreaux]

Some help here would be nice. There are two places with issues left. One is in the LawfulMonad instance. Some fields which had autoparams for the LawfulApplicative instance in Lean 3 no longer have them, and the definition of Seq.seq changed to be lazy, which is (I think) part of why these aren't solved by aesop.

Anyway, someone who is comfortable with these MvPolynomial and this monad instance could probably dispose of these sorries quickly, maybe @Johan Commelin?

[Johan Commelin]

This week I unfortunately don't have any time for porting...

[Johan Commelin]

Is this blocking other files? I thought this file was only used by Witt vectors... but that might have changed in the past 3 years :rofl:

[Jireh Loreaux]

It's now in the import hierarchy for analysis (!!!) (e.g., Hahn-Banach). I've looked into disentangling this a bit, but there's a thread going through which I don't know how best to deal with. The thread is this (starting backwards):

analysis stuff → is_R_or_C → finite dimensional stuff → matrix.adjugate → mv_polynomial

The first three arrows I think are mostly unavoiadable, but the last one could be solved by moving the declarations docs#matrix.det_adjugate, docs#matrix.adjugate_adjugate and docs#matrix.adjugate_adjugate' out of linear_algebra.matrix.adjugate and into a new file because this is the only place where docs#mv_polynomial sneaks in (and these decls) aren't needed in the rest of the dependency chain anywhere.

Is this a refactor we want? And exactly how should I split linear_algebra.matrix.adjugate if so?

[Jireh Loreaux]

Of the 3 decls I mentioned, only docs#matrix.det_adjugate is used in mathlib, and only in one place linear_algebra.matrix.special_linear_group, so some sort of split here seems reasonable.

[Jireh Loreaux]

Of course, these imports will then end up in complex analysis via the upper half-plane, but that's not terribly unreasonable.

[Johan Commelin]

A dependency on mv_polynomial isn't that bad. But a dependency on mv_polynomial.monad seems surprising.

[Johan Commelin]

Unless the file now contains more than I remember/expect.

[Jireh Loreaux]

For that the thread seems to be data.mv_polynomial.variables which has some small amount of monad stuff at the tail end. This then infects the rest of mv_polynomial stuff.

[Johan Commelin]

@Jireh Loreaux I see, that file is imported by mv_polynomial.variables, which is then used all over the place.

[Johan Commelin]

I think that import can be reversed.

[Johan Commelin]

The vars_bind₁ and mem_vars_bind₁ can move to .monad.

[Johan Commelin]

The other use of bind₁ can most likely just inline the definition.

[Scott Morrison]

This is done in #18593.

[Scott Morrison]

and #18594, for good measure, splits linear_algebra.matrix.adjugate to separate out the results needs anything about mv_polynomial.

[Eric Wieser]

I'm not a huge fan of splitting out the adjugate results; I think it's nice to have them all together

[Eric Wieser]

(I'm especially not a fan of having the file be deleted without replacement, but I assume that was accidental!)

[Eric Wieser]

Not having mv_polynomial imported there is likely to trick people who need more adjugate results into trying to do things the annoying combinatorial way