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