Is Finset totally ordered?

Stream: maths

[Christopher Hoskin]

Given an arbitrary (ι : Type*) , given (F : Finset ι) is it possible to pick some 1,...,n in ℕ to represent the elements of F? Or more generally to totally order the elements of F?

(Given a Quadratic map Q and an element a of a free module, I'm wondering if it's possible to represent Q(a) as an upper triangular matrix?)

[Alex J. Best]

There are some equivalences defined near https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Card.html#Finset.equivFin that might be helpful

[Christopher Hoskin]

Ah, thanks! This makes sense:

variable (ι : Type*)

variable (F : Finset ι)

variable (a b : ι) (ha: a ∈ F) (hb : b ∈ F )

#check F.equivFin.toFun ⟨a,ha⟩  < F.equivFin.toFun ⟨b,hb⟩

[Vincent Beffara]

Or you could use docs#Finset.toList

[Christopher Hoskin]

For block matrices I need a map into a Type with LT https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/LinearAlgebra/Matrix/Block.lean#L55 so I think F.equivFin.toFun works better for that?

[Christopher Hoskin]

After spending the evening thinking about it, this is where I've got to:

variable {ι : Type*}

variable {R : Type*} [CommSemiring R]

variable (Q : QuadraticForm R (ι →₀ R))

noncomputable def e (i : ι) : (ι →₀ R) :=  Finsupp.single i (1 : R)

noncomputable def UTmatrix (a : (ι →₀ R)) : Matrix ι ι R := Matrix.of fun i j =>
  haveI := Classical.decEq ι
  if H : i ∈ a.support ∧ j ∈ a.support then
    if (a.support.equivFin.toFun ⟨i,H.1⟩) = (a.support.equivFin.toFun ⟨j,H.2⟩) then
      Q (e i)
    else if (a.support.equivFin.toFun ⟨i,H.1⟩) < (a.support.equivFin.toFun ⟨j,H.2⟩) then
      Q.exists_companion.choose (e i) (e j)
    else
      (0 : R)
  else
    (0 : R)

[Eric Wieser]

You should drop the .toFuns there, that's not the preferred spelling

[Christopher Hoskin]

c.f. https://github.com/leanprover-community/mathlib4/pull/14292/files#diff-b2e63ded24baf2b6dbf29bf1c8d5ff01b0db9b4201ce0726503848038e25b241R25

[Antoine Chambert-Loir]

Isn't it simpler to just assume a LinearOrder on iota? Which could be transferred via equivFin if necessary?

[Eric Wieser]

Antoine, I'm not quite sure if you're responding to the original or most recent message, but docs#QuadraticMap.toBilin assumes a linear order, while the non-constructive docs#LinearMap.BilinMap.toQuadraticMap_surjective does not.

[Eric Wieser]

(those links won't become valid for a few hours)

[Eric Wieser]

Regarding the original question, it does seem like there should be a Fintype ι → Trunc (LinearOrder ι) somewhere.

[Eric Wieser]

But as you say, you could just make do with the equiv with Fin and do your work there instead

[Antoine Chambert-Loir]

I was indeed responding to a mixture of the most recent messages, sorry.

[Antoine Chambert-Loir]

Regarding the usefulness of some Fintype ι → Trunc (LinearOrder ι), there are many instances of this kind to have (one for every abstract existence theorem), and it is probably tedious to enter them all by hand. (Well orderings, bases, fixed points, minimal elements, etc.) What would be a sustainable design so that they are easily accessed, in a relatively standard way, without any risk of missing one.

[Antoine Chambert-Loir]

For example, docs#Finite.equivFin is just an invocation of docs#Finite.exists_equiv_fin. It would probably be nice to have them created using a @[choose] tag.