Matrix.fromRows TU (help wanted)

Stream: mathlib4

[Martin Dvořák]

I'm searching for help with proving Matrix.fromRows_one_isTotallyUnimodular_iff in #19076 .

[Eric Wieser]

Tangentially, it would be great if docs#Matrix.IsTotallyUnimodular had a docstring that actually explained what total unimodularity meant

[Martin Dvořák]

Would you just copy the description from "## Main definitions" or write something else?

[Eric Wieser]

Yes, that would be better than nothing

[Martin Dvořák]

And what would be even better?

[Eric Wieser]

Maybe it's also the optimum; the key thing is that docstring should do more than un-camel-case the name of the type!

[Eric Wieser]

It's possible for your theorem that having

lemma isTotallyUnimodular_iff.{w} (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [Fintype ι], ∀ f : ι → m, ∀ g : ι → n,
      (A.submatrix f g).det = 0 ∨
      (A.submatrix f g).det = 1 ∨
      (A.submatrix f g).det = -1 := by

might be handy, since that lets you pick any index type you like

[Martin Dvořák]

I'm just worried that if I simply write the sentence "A matrix is totally unimodular iff every square submatrix (not necessarily contiguous) has determinant 0 or 1 or -1." it will sound more like a statement than a definition. How would you phrase it so that it is clear we define it this way?

[Eric Wieser]

(and rename isTotallyUnimodular_iff to isTotallyUnimodular_iff_fin)

[Eric Wieser]

You could write

IsTotallyUnimodular A means that every square submatrix of A (not necessarily contiguous) has determinant 0 or 1 or -1.

[Edward van de Meent]

i feel like it'd be easier to prove this when the type of the columns is not a single sum type but an iterated sum with Unit, then recursion or something...

[Edward van de Meent]

(i've looked at the same thing for the seymour project)

[Edward van de Meent]

actually, i forgot that for lean matrices, the rows and columns don't come with a natural ordering... :upside_down: it might still work, but let me take another look.

[Martin Dvořák]

Edward van de Meent said:

(i've looked at the same thing for the seymour project)

Yes, exactly! This lemma will not only be useful for Mathlib, but will also earn you coäuthorship in the Seymour project.

[Martin Dvořák]

Eric Wieser said:

Tangentially, it would be great if docs#Matrix.IsTotallyUnimodular had a docstring that actually explained what total unimodularity meant

https://github.com/leanprover-community/mathlib4/pull/19338

[Edward van de Meent]

btw, i feel it is somewhat compacter to write ∈ ({0,1,-1}:Set R) rather than = 0 ∨ = 1 ∨ = -1, where you repeat exactly what determinant you are taking 3 times... would such a change be welcome?

[Edward van de Meent]

it declutters the infoview, imo.

[Eric Wieser]

Or you could write that it is in the range of the coercion from SignType

[Edward van de Meent]

that's a great idea... ideally we'd even use a (currently nonexistent) SubgroupWithZero structure with instances for Setlike and associate algebra variants, to be easily able to reason about multiplying these values...

[Edward van de Meent]

or really, SubmonoidWithZero should be enough here...

[Eric Wieser]

I don't see that being particularly useful vs just working in SignType

[Eric Wieser]

#19345 implements the SignType idea

[Edward van de Meent]

my goal/idea was to use Signtype.castHom.range, which hypothetically would give a structure with MulMemClass and the like, allowing for easy proving that certain things are still members of the set.

[Edward van de Meent]

so it's the same, but with :sparkles: API :sparkles:

[Eric Wieser]

Certainly that's a useful proof technique, though it's not clear to me that the bundled version should be used in the definition vs making theorems rewrite to that form if they want the API

[Eric Wieser]

I guess you could use the same argument to justify det ∈ ({0,1,-1}:Set R) instead of det ∈ Set.range SignType.cast, but both are better than the current spelling since det isn't repeated

[Edward van de Meent]

why should Matrix.det go through Matrix.detRowAlternating, rather than just making Matrix.det_apply defeq? (because then by default you get better api)

[Edward van de Meent]

same applies in this case, imo.

[Bhavik Mehta]

Eric Wieser said:

#19345 implements the SignType idea

I have a proof of the theorem in the first message in the thread which uses SignType

[Edward van de Meent]

awesome!

[Eric Wieser]

Edward van de Meent said:

why should Matrix.det go through Matrix.detRowAlternating, rather than just making Matrix.det_apply defeq? (because then by default you get better api)

That's a fair argument, especially since I'm responsible for things being that way. I'm slightly surprised to see that det is an abbrev, but maybe I'm responsible for that too.

[Eric Wieser]

How about we go with Set.range for now, but change it to Signtype.castHom.range as soon as we have a proof that makes that more convenient?

[Edward van de Meent]

sounds good, especially since neither SubmonoidWithZero nor MonoidWithZeroHom.range exist yet

[Martin Dvořák]

Eric Wieser said:

It's possible for your theorem that having

lemma isTotallyUnimodular_iff.{w} (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [Fintype ι], ∀ f : ι → m, ∀ g : ι → n,
      (A.submatrix f g).det = 0 ∨
      (A.submatrix f g).det = 1 ∨
      (A.submatrix f g).det = -1 := by

might be handy, since that lets you pick any index type you like

I can easily do

lemma isTotallyUnimodular_iff_fintype (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ (ι : Type) [Fintype ι] [DecidableEq ι], ∀ f : ι → m, ∀ g : ι → n,
      (A.submatrix f g).det = 0 ∨
      (A.submatrix f g).det = 1 ∨
      (A.submatrix f g).det = -1 := by
  rw [isTotallyUnimodular_iff]
  constructor
  · intro hA ι _ _ f g
    specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
    rwa [←submatrix_submatrix, det_submatrix_equiv_self] at hA
  · intro hA k
    exact hA (Fin k)

but don't know how to approach the general universe thing.

[Martin Dvořák]

Can I say something like Fin k from higher universe?

[Edward van de Meent]

Using ULift, I think?

[Martin Dvořák]

import Mathlib

variable {m n R : Type*} [CommRing R]

lemma Matrix.isTotallyUnimodular_iff_fintype.{w} (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [Fintype ι] [DecidableEq ι], ∀ f : ι → m, ∀ g : ι → n,
      (A.submatrix f g).det ∈ Set.range SignType.cast := by
  rw [isTotallyUnimodular_iff]
  constructor
  · intro hA ι _ _ f g
    specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
    rw [←submatrix_submatrix, det_submatrix_equiv_self] at hA
    exact hA
  · intro hA k f g
    specialize hA (ULift (Fin k)) (f ∘ ULift.down) (g ∘ ULift.down)
    rw [←submatrix_submatrix] at hA
    convert hA
    sorry -- TODO `ULift.down` does not change the determinant!

[Edward van de Meent]

using Equiv.ulift might improve available API?

[Martin Dvořák]

This works:

import Mathlib

variable {m n R : Type*} [CommRing R]

lemma Matrix.isTotallyUnimodular_iff_fintype.{w} (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [Fintype ι] [DecidableEq ι], ∀ f : ι → m, ∀ g : ι → n,
      (A.submatrix f g).det ∈ Set.range SignType.cast := by
  rw [isTotallyUnimodular_iff]
  constructor
  · intro hA ι _ _ f g
    specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
    rw [←submatrix_submatrix, det_submatrix_equiv_self] at hA
    exact hA
  · intro hA k f g
    specialize hA (ULift (Fin k)) (f ∘ Equiv.ulift) (g ∘ Equiv.ulift)
    rwa [←submatrix_submatrix, det_submatrix_equiv_self] at hA

[Martin Dvořák]

Would you @Edward van de Meent like to PR the lemma?

[Edward van de Meent]

sure :+1:

[Edward van de Meent]

#19366

[Bhavik Mehta]

Bhavik Mehta said:

Eric Wieser said:

#19345 implements the SignType idea

I have a proof of the theorem in the first message in the thread which uses SignType

@Martin Dvořák do you mind if I push my proof to your branch+PR?

[Martin Dvořák]

Please do!

[Martin Dvořák]

I finished what I needed to finish:
https://github.com/leanprover-community/mathlib4/pull/19076
It remains to find home for neg_one_pow_mem_signType_range or inline it.