Sym2 of Fintype is Fintype

Stream: new members

[Vasily Ilin]

It feels like this should be an existing theorem but I can't figure it out. What am I doing wrong?

import Mathlib.Data.Fintype.Basic
variable [Fintype V]
example : Fintype (Sym2 V) := by
  apply? -- gives `exact Fintype.ofFinite (Sym2 V)`
  -- still have an unfinished goal

[Kyle Miller]

I think if you add [DecidableEq V] you get Fintype (Sym2 V)

[Kyle Miller]

You need another import too:

import Mathlib.Data.Sym.Card
import Mathlib.Data.Fintype.Basic

variable {V : Type*} [Fintype V] [DecidableEq V]

#synth Fintype (Sym2 V)

[Vasily Ilin]

It works!

[Vasily Ilin]

Why do I need DecidableEq V here? It feels like it should not be needed since V × V is a Fintype and taking a quotient can only shrink the size.

[Kyle Miller]

docs#Quotient.fintype needs the relation to be decidable. The data of a Fintype is an actual list that has all the elements, and that needs to be computed.

The docs#Finite typeclass is the mere fact a type is finite.

[Kyle Miller]

I don't think Sym2 needs DecidableEq for a Fintype instance though, if you write a custom one.

[Vasily Ilin]

I don't quite understand but in order to not exhaust my budget of questions to ask I will leave it there. Thank you for making the code work!

[Kyle Miller]

Quotient.fintype works by calculating a set of representatives, which it does by removing elements one at a time that are related to other elements by the relation your quotienting by. That requires decidable equality to do the computation for Sym2

[Vasily Ilin]

So it has to do with the implementation, not whether it's possible to prove that a quotient of a finite type is finite (seems mathmatically obvious)

[Kyle Miller]

Indeed:

import Mathlib.Data.Sym.Card
import Mathlib.Data.Set.Finite

variable {V : Type*} [Finite V]

#synth Finite (Sym2 V)

[Kyle Miller]

The reason Sym2 should be a Fintype without needing DecidableEq is because there's this function that can enumerate elements.

def subtriangle {α : Type*} : List α → List (α × α)
  | [] => []
  | x::xs => ((x::xs).map fun y => (x, y)) ++ subtriangle xs

#eval subtriangle [1,2,3]
-- [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)]

I wonder if this exists in mathlib somewhere already?

[Kyle Miller]

Here's the fintype instance minus proofs

import Mathlib.Data.Sym.Card
import Mathlib.Data.Set.Finite

def List.subtriangle {α : Type*} : List α → List (Sym2 α)
  | [] => []
  | x::xs => ((x::xs).map fun y => Quotient.mk' (x, y)) ++ subtriangle xs

theorem List.subtriangle.perm {α : Type*} (xs ys : List α) (h : xs ~ ys) :
    xs.subtriangle ~ ys.subtriangle := by
  sorry

theorem List.Nodup.subtriangle {α : Type*} (xs : List α) (h : xs.Nodup) :
    xs.subtriangle.Nodup := by
  sorry

def Multiset.subtriangle {α : Type*} (m : Multiset α) : Multiset (Sym2 α) :=
  m.liftOn (fun xs => xs.subtriangle) <| by
    intro xs ys h
    rw [coe_eq_coe]
    exact List.subtriangle.perm _ _ h

def Finset.subtriangle {α : Type*} (s : Finset α) : Finset (Sym2 α) where
  val := s.val.subtriangle
  nodup := by
    cases' s with val nodup
    revert nodup
    refine val.recOnSubsingleton ?_
    intro _ nodup
    exact nodup.subtriangle

instance (α : Type*) [Fintype α] : Fintype (Sym2 α) where
  elems := Finset.univ.subtriangle
  complete := by
    sorry

[Yaël Dillies]

Kyle, you just solved a problem that @Eric Wieser and I couldn't solve a year ago! Do you mind opening a PR that fixes docs#Finset.sym2 ?

[Kevin Buzzard]

Vasily Ilin said:

So it has to do with the implementation, not whether it's possible to prove that a quotient of a finite type is finite (seems mathmatically obvious)

It might be obvious to you but it's not true constructively, and Fintype is constructive finiteness -- Fintype V is not a Prop, it's data. It's not a true/false statement.

[Kyle Miller]

@Yaël Dillies I just created a PR: #8211 (Feel free to golf)

[Kyle Miller]

I just pushed some fixes to take into account how Quotient.mk vs Quotient.mk'' is a mess right now... I think we ought to finally switch to Sym2.mk and maybe make notation like s(a, b) for Sym2.mk a b (or maybe u(a, b) for "unordered pair"?)