Pairs of distinct elements

Stream: Is there code for X?

[Vasily Ilin]

Is there a type similar to Sym2 except [a,a] is not allowed? The cardinality of this type would be n(n-1)/2 instead of n(n+1)/2 like for Sym2. I am defining a random graph and I want to say that for every unordered pair of vertices [v,w] with v not equal to w, I can have an edge.

[Eric Wieser]

(x : Sym2 α// ¬x.IsDiag}

[Kyle Miller]

For example, the cardinality result exists as docs#html#Sym2.card_subtype_not_diag

[Kyle Miller]

Sometimes I've thought about introducing UConf2 α := {x : Sym2 α // ¬x.IsDiag} as an abbreviation for this (it's the unordered configuration space of two points). This might be a bit of an obscure name though.

[Kevin Buzzard]

"alpha choose 2" would be a cool name :-)

[Kyle Miller]

Oh, Choose2 α would be a lot better than UConf2 α. Then there could also be Choose α 2. This would mirror Sym2 α and Sym α 2.

[Kyle Miller]

Imagine if we had uniform symbols for everything in the 12-fold way. This one could be α q↪ Fin 2 for "injective functions, quotiented by permutations of the domain"

[Kyle Miller]

Fin n ↠q Fin m (surjective maps, quotiented by permutations of the codomain) could be for Stirling numbers of the second kind $n\brace m$

[Antoine Chambert-Loir]

In my work on the simplicity of the alternating group, I made use of

/-- The type of combinations of `n` elements of a type `α` -/
def Nat.Combination (n : ℕ) := {s : Finset α | s.card = n}

[Antoine Chambert-Loir]

(and then, I study the action of Equiv.Perm α on the corresponding subtype).

[Notification Bot]

Vasily Ilin has marked this topic as resolved.

[Notification Bot]

Vasily Ilin has marked this topic as unresolved.

[Vasily Ilin]

Why does docs#SimpleGraph.edgeSet not use {x : Sym2 α // ¬x.IsDiag} but instead uses Sym2? A simple graph does not have self-edges so there won't be any diagonal elements.

[Ruben Van de Velde]

Probably because it's easier this way

[Kyle Miller]

Rather than working with subtypes, it can be easier working with types themselves and then using accompanying theorems (like docs#SimpleGraph.not_isDiag_of_mem_edgeSet). If you need the subtype, then you can package it up yourself.

It's similar to questions like, for Nat, why doesn't n + 1 land in {m : Nat // 0 < m} rather than Nat.

[Vasily Ilin]

In https://github.com/Vilin97/random_graphs/blob/experimental/RandomGraphs/erdos_renyi.lean#L51 I proved a false theorem -- that an Erdos-Renyi simple graph has pn(n+1)/2 edges in expectation. Instead I need it to be pn(n-1)/2. The problem is that I defined edges to be in Sym2 V, thinking that that's the type of edges. But Sym2 V has the wrong cardinality. Now I am trying to switch to using {x : Sym2 V // ¬x.IsDiag} but I am struggling to convert from this type to Sym2 V.

variable [Fintype V] [DecidableEq V]
def EdgeType (V : Type) := {x : Sym2 V // ¬x.IsDiag}
lemma edge_type_subtype_of_sym2 (e : EdgeType V) : (e : Sym2 V) := sorry

[Kyle Miller]

If you switch def EdgeType to abbrev EdgeType, then if you have e : EdgeType V you should be able to use e wherever a Sym2 V is expected.

[Antoine Chambert-Loir]

If you want it for graphs, I strongly wish that mathlib implements the definition of Serre / Bourbaki that will allow correct automorphisms groups, relation with orientations etc

[Vasily Ilin]

Kyle Miller said:

If you switch def EdgeType to abbrev EdgeType, then if you have e : EdgeType V you should be able to use e wherever a Sym2 V is expected.

That does not work for me. I get the same error with def and abbrev.

[Kyle Miller]

What's the error? This works for me:

import Mathlib

variable {V : Type*} [Fintype V] [DecidableEq V]
abbrev EdgeType (V : Type*) := {x : Sym2 V // ¬x.IsDiag}
lemma edge_type_subtype_of_sym2 (e : EdgeType V) : Sym2 V := e

[Vasily Ilin]

import Mathlib.Combinatorics.SimpleGraph.Basic

variable {V : Type*} [Fintype V] [DecidableEq V]
abbrev EdgeType (V : Type*) := {x : Sym2 V // ¬x.IsDiag}
def Edge (G : SimpleGraph V) (e : EdgeType V) : Prop := e ∈ G.edgeSet -- failed to synthesize instance Membership (EdgeType V) (Set (Sym2 V))

[Vasily Ilin]

Failed to synthesize membership

[Yaël Dillies]

I believe this is because abbrev (very surprisingly) doesn't make the definition reducible.

[Vasily Ilin]

I don't know what reducible means :(

[Kyle Miller]

@Yaël Dillies That's not the case, abbrev does make definitions reducible.

I think the problem is that this isn't a place where Lean will insert a coercion. This works:

def Edge (G : SimpleGraph V) (e : EdgeType V) : Prop := e.1 ∈ G.edgeSet

[Kyle Miller]

When I said "wherever a Sym2 V is expected" I'm technically correct (it does work if Lean is expecting a Sym2 in the sense it will insert a coercion as needed), but I'm practically incorrect because you can't use it wherever a Sym2 would have worked before.

[Kyle Miller]

(I'm not really sure why it shouldn't work here though. One could imagine that because the first argument is an outParam that Lean could insert a coercion, but the fact is that it doesn't.)

[Vasily Ilin]

Thank you!