Lifting an equivalence to sym2

Stream: maths

[Yaël Dillies]

docs#sym2.lift allows to lift symmetric maps f : α → α → β to functions sym2 α → β. Now, I want to define the unoriented edges of a multiset, so instead of the equality f a b = f b a, I have an equivalence f a b ≃ f b a. How do I lift that to a function from sym2?

import data.sym.sym2

universes u
variables {α : Type*}

namespace sym2

def lift_sort (f : α → α → Sort u) (e : Π a b, f a b ≃ f b a) (he : ∀ a b, (e a b).symm = e b a) :
  sym2 α → Sort u := sorry

variables (f : α → α → Sort u) (e : Π a b, f a b ≃ f b a) (he : ∀ a b, (e a b).symm = e b a)

def lift_sort_equiv (a b : α) : lift_sort f e he ⟦(a, b)⟧ ≃ f a b :=
sorry

-- maybe some lemma along the lines of
-- `(lift_sort_equiv f e a b).symm.trans (lift_sort_equiv f e b a) = e a b`?

end sym2

Note that I don't know how to handle the diagonal. If we consider that an edge should always come from two darts, then lift_sort_equiv should take a ≠ b as assumption.
But really any progress would help. I've been stuck on that for several days now.

Maybe @Kyle Miller can help?

[Bhavik Mehta]

import data.sym.sym2

universes u
variables {α : Type*}

namespace sym2

variables (f : α → α → Sort u) (e : Π a b, f a b ≃ f b a) (he : ∀ a b, (e a b).symm = e b a)

def lift_sort (f : α → α → Sort u) :
  sym2 α → Sort u :=
λ x, f (quotient.out x).1 (quotient.out x).2

lemma out_eq (a b : α) : ⟦(a, b)⟧.out = (a, b) ∨ ⟦(a, b)⟧.out = (b, a) :=
begin
  have : ⟦(⟦(a, b)⟧.out.1, ⟦(a, b)⟧.out.2)⟧ = ⟦(a, b)⟧,
  { simp },
  rw sym2.eq_iff at this,
  rwa [prod.ext_iff, prod.ext_iff],
end

open_locale classical

noncomputable def lift_sort_equiv (f : α → α → Sort u) (e : Π a b, f a b ≃ f b a)
  (he : ∀ a b, (e a b).symm = e b a) (a b : α) :
  lift_sort f ⟦(a, b)⟧ ≃ f a b :=
dite (⟦(a, b)⟧.out = (a, b))
  (λ h, equiv.cast (by { change f _ _ = _, rw h }))
  (λ h, (equiv.cast (by { change f _ _ = _, rw (out_eq _ _).resolve_left h })).trans (e _ _))

end sym2

[Bhavik Mehta]

I'm not sure what your lemma is meant to be describing, I can't make it typecheck

[Bhavik Mehta]

Ah, maybe you mean

lemma lift_sort_equiv_symm_trans {a b : α} :
  (lift_sort_equiv f e _ _).symm.trans (equiv.trans (equiv.cast (by rw sym2.eq_swap)) (lift_sort_equiv f e b a)) = e a b :=

[Yaël Dillies]

Yes exactly

[Bhavik Mehta]

When a = b, this lemma implies equiv.refl (f a a) = e a a

[Bhavik Mehta]

And with that assumption, it's not too tricky to prove:

lemma lift_sort_equiv_symm_trans {a b : α}
  (he : ∀ a b, (e a b).symm = e b a) (hf : equiv.refl (f a a) = e a a) :
  (lift_sort_equiv f e _ _).symm.trans
    ((equiv.cast (by rw sym2.eq_swap)).trans (lift_sort_equiv f e b a)) = e a b :=
begin
  rw [lift_sort_equiv, lift_sort_equiv],
  rcases eq_or_ne a b with rfl | hab,
  { simpa },
  cases out_eq a b,
  { rw [dif_pos h, dif_neg],
    { ext x,
      simp },
    rw [sym2.eq_swap, h],
    simp [hab] },
  { rw [dif_neg, dif_pos],
    { ext x,
      simp [he] },
    { rwa [sym2.eq_swap] },
    rw h,
    simp [hab] }
end

[Yaël Dillies]

So Kyle, what do you think of making this sym2 α → Sort u edges map the primitive for multigraph? It seems quite hard to build it from the α → α → Sort u homs. The other way around is trivial and can be handled by the typeclasses I'm offering.

[Reid Barton]

Surprisingly (at least it wasn't my initial reaction) it is also possible to implement this without choice (e.g. quotient.out)

import data.sym.sym2

section

universe u
parameters {α : Type u} (f : α → α → Type u)
parameters (e : Π a b, f a b ≃ f b a) (he : ∀ a b, (e a b).symm = e b a) (he' : ∀ a, e a a = equiv.refl _)

structure aux (s : sym2 α) :=
(a₁ a₂ : α)
(h : ⟦(a₁, a₂)⟧ = s)
(x : f a₁ a₂)

inductive aux_rel (s : sym2 α) : aux s → aux s → Prop
| sym (a₁ a₂ h x) : aux_rel ⟨a₁, a₂, h, x⟩ ⟨a₂, a₁, begin subst h, apply sym2.eq_swap end, e a₁ a₂ x⟩

def lift_type : sym2 α → Type u := λ s, quot (aux_rel s)

end

[Reid Barton]

I didn't try to implement lift_sort_equiv so there may be more surprises there, but it seems like the right construction math-wise.

[Bhavik Mehta]

Woah I wasn't expecting it to be possible computably either, nice!

[Reid Barton]

Basically the h : ⟦(a₁, a₂)⟧ = s is a kind of strictification that produces an equality in Type where you wouldn't expect to obtain one

[Reid Barton]

I think the hypothesis he' that I added "just in case" probably isn't really necessary

[Reid Barton]

The way to arrive at this is rather than trying to build the type family lift_type : sym2 α → Type u, try to build the map X → sym2 α that it classifies

[Kyle Miller]

Here's a translation of @Reid Barton's construction into multigraph language. I wonder if there's a way to keep the universes for edges' from being bumped up?

import data.sym.sym2

universes u v

structure multigraph (α : Type u) :=
(edges : α → α → Sort v)
(flip : Π v w, edges v w ≃ edges w v)
(inv : ∀ v w, (flip v w).symm = flip w v)
(loops : ∀ v, flip v v = equiv.refl _)

namespace multigraph
variables {α : Type u} (G : multigraph.{u v} α)

structure dart_at (s : sym2 α) :=
(v w : α)
(edge : G.edges v w)
(h : ⟦(v, w)⟧ = s)

inductive is_flipped_dart_at (s : sym2 α) : G.dart_at s → G.dart_at s → Prop
| is_flip (v w : α) (e : G.edges v w) (h : ⟦(v, w)⟧ = s) :
  is_flipped_dart_at ⟨v, w, e, h⟩ ⟨w, v, G.flip v w e, by { subst_vars, apply sym2.eq_swap }⟩

def edges' : sym2 α → Sort (max (u+1) v) := λ s, quot (G.is_flipped_dart_at s)

end multigraph

[Kyle Miller]

I find going through a map E -> sym2 V more natural on the way to the edges map, though (like what Reid mentioned):

import data.sym.sym2

universes u v

structure multigraph (α : Type u) :=
(edges : α → α → Sort v)
(flip : Π v w, edges v w ≃ edges w v)
(inv : ∀ v w, (flip v w).symm = flip w v)
(loops : ∀ v, flip v v = equiv.refl _)

namespace multigraph
variables {α : Type u} (G : multigraph.{u v} α)

def dart := Σ' u v, G.edges u v

def dart.flip {G : multigraph α} : G.dart → G.dart
| ⟨u, v, e⟩ := ⟨v, u, G.flip u v e⟩

inductive is_flipped_dart : G.dart → G.dart → Prop
| flip (d : G.dart) : is_flipped_dart d d.flip

def E := quot G.is_flipped_dart

def ends : G.E → sym2 α :=
quot.lift (λ (d : G.dart), ⟦(d.1, d.2.1)⟧)
begin
  rintros ⟨u,v,e⟩ ⟨u',v',e'⟩ ⟨_⟩,
  apply sym2.eq_swap,
end

def edges' (s : sym2 α) : Sort* := {e : G.E // G.ends e = s}

end multigraph

[David Wärn]

If you want to take this perspective seriously you will probably need to work with the transport from edges' ⟦(a, b)⟧ to edges' ⟦(b, a)⟧. I don't think this is any easier than having edges indexed by α × α and making flip explicit. I'm also sceptical of including this loops condition in the basic multigraph class (it means you can't view a groupoid as a multigraph). If you drop the loops condition then you can no longer think of a multigraph as a type family over some set, rather it would be a presheaf over a (non-discrete) groupoid analogue of sym2.