Cayley graphs (again)

Stream: graph theory

[Rémi Bottinelli]

Hey, i've decided it is time I get some version of Cayley graphs merged.
The approach I settled with is to define graphs as soon as you have a smul and a subset of the "action" set, and then get Schreier graphs for free as given by the action of a group on a set, and similarly Cayley graphs for the self action.
As of now, i've got the following:

I'd like to have a basic "core" that I can merge and can nice enough to be reusable and extendable.
I'm therefore asking for preliminary feedback: is this an acceptable way to do Cayley/Schreier graphs? What would the minimal set of results needed here look like?

import combinatorics.simple_graph.basic
import combinatorics.simple_graph.subgraph
import combinatorics.simple_graph.connectivity
import data.list
import group_theory.group_action.group
import group_theory.subgroup.basic
import group_theory.coset
import group_theory.quotient_group
import group_theory.group_action.quotient

open function

universes u v w

namespace simple_graph

section defs

variables (X : Type*) {M : Type*} [has_smul M X] (S : set M)

inductive schreier_graph.adj_gen : X → X → Prop
| mk (m : S) (x : X) : schreier_graph.adj_gen (x) (m.val • x)

lemma schreier_graph.adj_gen_iff {x y : X} : schreier_graph.adj_gen X S x y ↔ ∃ (m : S), y = m.val • x :=
begin
  split,
  { rintro ⟨m, x⟩, exact ⟨m, rfl⟩, },
  { rintro ⟨m, rfl⟩, constructor, },
end

def schreier_graph : simple_graph X := simple_graph.from_rel (schreier_graph.adj_gen X S)

end defs

namespace schreier_graph

section basic

variables {X : Type*} {M : Type*} [has_smul M X] (S : set M)

lemma mono {S} {T : set M} (h : S ≤ T) : schreier_graph X S ≤ schreier_graph X T :=
begin
  apply simple_graph.from_rel_mono,
  rintros _ _ ⟨⟨m, mS⟩, x⟩,
  exact adj_gen.mk ⟨m, h mS⟩ x,
end

lemma adj_iff {x y : X} : (schreier_graph X S).adj x y ↔ (x ≠ y ∧ ∃ m ∈ S, m • x = y ∨ m • y = x) :=
begin
  simp only [schreier_graph, adj_gen_iff, from_rel_adj, ne.def, set_coe.exists],
  congr', ext, split,
  { rintros (⟨m,h,rfl⟩|⟨m,h,rfl⟩), exact ⟨m,h,or.inl rfl⟩, exact ⟨m,h,or.inr rfl⟩, },
  { rintros ⟨m,h,(rfl|rfl)⟩, exact or.inl ⟨m,h,rfl⟩, exact or.inr ⟨m,h,rfl⟩, },
end

lemma neighbor_set_eq {x : X} :
  (schreier_graph X S).neighbor_set x = {y | x ≠ y ∧ ∃ m ∈ S, m • x = y ∨ m • y = x} :=
by { dsimp [neighbor_set, set_of], ext, rw adj_iff, }

lemma neighbor_set_eq' {x : X} :
  (schreier_graph X S).neighbor_set x
= {y | x ≠ y} ∩ ({y | ∃ m ∈ S, m • x = y} ∪ {y | ∃ m ∈ S, m • y = x}) :=
begin
  simp only [schreier_graph, ne.def, exists_prop], ext,
  simp only [mem_neighbor_set, set.mem_inter_iff, set.mem_set_of_eq, set.mem_union,
             simple_graph.from_rel_adj, adj_gen_iff, ne.def, set_coe.exists, exists_prop,
             and.congr_right_iff],
  rintro, congr'; ext; tauto,
end

end basic

section group_action

variables {X : Type*} {G : Type*} [group G] [mul_action G X] (S : set G)

lemma eq_add_inverses_remove_one :
  (schreier_graph X S) = (schreier_graph X $ (S ∪ (set.image (λ x : G, x ⁻¹) S)) \ {(1 : G)}) :=
begin
  ext x y,
  simp only [adj_iff, ne.def, exists_prop, set.mem_diff, set.mem_union, set.mem_image,
             set.mem_singleton_iff, and.congr_right_iff],
  rintro ne, split,
  { rintro ⟨m,mS,(l|r)⟩,
    { use [m,mS], rintro rfl, simp [one_smul] at l, exact ne l, left, exact l, },
    { use [m,mS], rintro rfl, simp only [one_smul] at r, exact ne r.symm, right, exact r}, },
  { rintros ⟨m,⟨⟨(mS|⟨n,nS,rfl⟩),b⟩,e⟩⟩,
    { use [m,mS,e], },
    { use [n,nS], rw [inv_smul_eq_iff, inv_smul_eq_iff] at e, tauto, }, },
end

lemma reachable_iff {x y : X} :
  (schreier_graph X S).reachable x y ↔ ∃ g ∈ (subgroup.closure S), g • x = y :=
begin
  split,
  { rintro ⟨w⟩,
    induction w,
    { exact ⟨1, subgroup.one_mem _, one_smul _ w⟩, },
    { obtain ⟨g,gS,rfl⟩ := w_ih,
      rw adj_iff at w_h,
      rcases w_h with ⟨ne,⟨m,h,(rfl|rfl)⟩⟩,
      { refine ⟨g*m, _, mul_smul _ _ _⟩,
        exact (subgroup.closure S).mul_mem gS (subgroup.subset_closure h), },
      { refine ⟨g * m ⁻¹, _, _⟩, rotate, simp only [mul_smul, inv_smul_eq_iff, smul_left_cancel_iff],
        exact (subgroup.closure S).mul_mem gS
          ((subgroup.closure S).inv_mem $ subgroup.subset_closure h), }, }, },
  { rintro ⟨g, gS, rfl⟩, revert x,
    apply subgroup.closure_induction gS,
    { rintro g gS x,
      by_cases h' : g • x = x,
      { rw h', },
      { constructor,
        apply adj.to_walk,
        rw adj_iff, refine ⟨ne.symm h', g, gS, or.inl rfl⟩, }, },
    { rintro x, simp, },
    { rintro g₁ g₂ xg₁ xg₂ x,
      rw [mul_smul],
      apply reachable.trans (@xg₂ x) (@xg₁ (g₂ • x)), },
    { rintro g xg x,
      apply reachable.symm,
      convert @xg (g ⁻¹ • x),
      simp only [smul_inv_smul], }, },
end

abbreviation schreier_coset_graph (H : subgroup G) := schreier_graph (G ⧸ H) S

noncomputable def equiv_coset_graph_of_pretransitive [mul_action.is_pretransitive G X] (x₀ : X) :
  schreier_coset_graph S (mul_action.stabilizer G x₀) ≃g schreier_graph X S :=
{ to_equiv     := (mul_action.equiv_quotient_stabilizer G x₀).symm,
  map_rel_iff' := λ x y, by
  { simp only [adj_iff, mul_action.equiv_quotient_stabilizer, equiv.symm_symm,
               equiv.of_bijective_apply, ne.def, exists_prop,
               ←mul_action.of_quotient_stabilizer_smul],
    simp only [injective.eq_iff (mul_action.injective_of_quotient_stabilizer G x₀)], } }

instance [decidable_eq X] [h : fintype S] : locally_finite (schreier_graph X S) :=
begin
  rintro x, rw neighbor_set_eq',
  haveI : fintype ↥{y : X | ∃ (m : G) (H : m ∈ S), m • x = y}, by
  { convert set.fintype_image S (•x),
    simp only [exists_prop], },
  haveI : fintype ↥{y : X | ∃ (m : G) (H : m ∈ S), m • y = x}, by
  { simp_rw [←eq_inv_smul_iff],
    convert set.fintype_image S (λ g, g⁻¹•x),
    simp only [exists_prop],
    ext, congr', ext, tauto, },
  apply_instance,
end

abbreviation cayley_graph := schreier_graph G S

def as_automorphism (g : G) : (cayley_graph S ≃g cayley_graph S) :=
{ to_equiv := equiv.mul_right (g⁻¹),
  map_rel_iff' := λ a b, by
  { simp only [adj_iff, equiv.coe_mul_right, ne.def, mul_left_inj, smul_eq_mul, exists_prop,
               and.congr_right_iff],
    simp only [←mul_assoc, injective.eq_iff (group.mul_right_bijective (g⁻¹)).left],
    exact λ _, iff.rfl, } }

def as_automorphism_group : G →* (cayley_graph S ≃g cayley_graph S) :=
{ to_fun := as_automorphism S,
  map_one' := by { dsimp [as_automorphism], ext, simp, },
  map_mul' := λ g g', by { dsimp [as_automorphism], ext, simp, } }

def injective_as_automorphism_group : function.injective (as_automorphism_group S) :=
begin
  rintro g g' h,
  simp only [as_automorphism_group, as_automorphism, equiv.mul_right, to_units, units.mul_right,
             inv_inv, units.inv_mk, units.coe_mk, mul_equiv.coe_mk, monoid_hom.coe_mk] at h,
  simpa using congr_fun h.left 1,
end

end group_action

end schreier_graph

end simple_graph

[Yaël Dillies]

Do you not want to use markings from branch#geometric_group_theory?

[Rémi Bottinelli]

Well, what I don't really like with markings is that they are assumed surjective

[Rémi Bottinelli]

My thought process was mostly like: there hasn't been much life on this marking code, and my understanding was that perhaps the GGT aspect should start with something even more general than markings, but I'm not sure exactly how to proceed. So instead of wait for it to happen, I should just work out a good enough "combinatorial" version of Cayley graphs that actually gets somewhere.

[Rémi Bottinelli]

Also, this one covers Schreier graphs, which is also useful and not "natively" covered by markings I believe.

[Yaël Dillies]

Okay sure

[Rémi Bottinelli]

I mean, I shared my progress here exactly to discuss this kind of thing, so I'm open to some other path if there is a reasonable argument for it.

[Kyle Miller]

I suspect simple graphs are not the right data structure for Schreier graphs. They're fine for connectivity relations and for graph metrics, but, for example, you're not able to represent the fact that walks in a Schierer graph correspond to words in the given generating set (and you also have to artificially remove loops).

I suspect we want a type of multigraphs with directed labeled edges for this -- this at least matches the definitions of Schreier and Cayley graphs that I know. There are some facts about automorphism groups of Schreier graphs that don't appear to be true when they are turned into simple graphs.

[Rémi Bottinelli]

mmh, yeah, that's a good point. For Cayley graphs and GGT, I think having simple_graphs is good enough since all we care about is the metric, really. But you're probably right about Schreier graphs: in this case the labelling is quite more important in general.
Well, let me reimplement it all on top of quivers then ?

[Kyle Miller]

There's another fact about Schreier graphs, which is that if you have a finitely presented group G with a finitely normally generated subgroup H, then you can "compute" the Schreier graph for G acting on H by iteratively considering Scheier graphs associated to sequences of subgroups of H generated by finite unions of conjugates of the generating set, and these Scheier graphs converge to the true one in the sense that the vertices eventually stabilize (for each vertex, there is some step after which it will never be identified with another vertex). I wonder in which setting this is easiest to formalize? (Btw, I'm describing the Todd-Coxeter algorithm)

[Kyle Miller]

I wonder what the best way to encode Cayley graphs as quivers would be. You'd want your quiver automorphisms to respect edge labelings, right?

[Rémi Bottinelli]

Yeah, that seems the most natural way to do it. I was thinking this:

section defs

variables (X : Type*) {M : Type*} [has_smul M X] {S : Type*} (ι : S → M)

inductive schreier_graph.arrow : X → X → Sort*
| mk (m : S) (x : X) : schreier_graph.arrow (x) (ι m • x)

instance : quiver X := ⟨schreier_graph.arrow X ι⟩

end defs

[Rémi Bottinelli]

wait, scratch my inductive oh no, let's keep it

[Rémi Bottinelli]

by the way, I was wondering if we could add infix notation for prefunctors and their composition

[Kyle Miller]

Do we then define a special type of prefunctor that sends an mk m _ to an mk m _?

I think the sort of formal result that tests whether these are the correct notion of a schreier graph is if they are somehow equivalent to G-sets. So morphisms of G-sets <-> morphisms of Scheier graphs for G, if I've got this right.

[Rémi Bottinelli]

ah, I'm stupid, you're right, the coloring is kind of forgotten when building the quiver. let me think

[Rémi Bottinelli]

well, I guess the most natural way is to add color {x y} : x --> y -> S no?

[Rémi Bottinelli]

structure colored_quiver (V : Type*) (S : Type*) extends (quiver V)  :=
(coloring : ∀ X Y, (to_quiver.hom X Y) → S)

what about this?

[Kyle Miller]

I guess that sort of thing might work (except it'd be a class), though you'd still have to go and make sure you have color-preserving quiver homomorphisms

[Kyle Miller]

Another possibility is to start developing the theory of labeled digraphs

[Kyle Miller]

Here's a very small start:

structure labeled_digraph (α : Type*) (S : Type*) :=
(arrows : α → α → set S)

namespace labeled_digraph

/-- Label-preserving graph homomorphism. -/
protected structure hom {α β : Type*} {S : Type*}
  (G : labeled_digraph α S) (G' : labeled_digraph β S) :=
(map_vert : α → β)
(map_arrow : ∀ (x y) (s ∈ G.arrows x y), s ∈ G'.arrows (map_vert x) (map_vert y))

notation (name := labeled_digraph.hom) G ` →g ` G' := hom G G'

end labeled_digraph

[Rémi Bottinelli]

That's nice indeed. I'm just kind of saddened by the possibility to have one more graph-like definition (making it 3, and 4 if the directed graph PR of Yael gets merged)

[Rémi Bottinelli]

Honestly, for me it's more about settling down on one convention and actually getting at least one definition of cayley graphs in, and I figure we might as well cover schreier graphs in the same stroke

[Kyle Miller]

What do you think are the fundamental theorems that can test whether it's the right definition?

[Kyle Miller]

Given what I know about GGT, when groups act on graphs they're mostly simple graphs, so having a simple_graph.schreier_graph and a simple_graph.cayley_graph might not be so crazy, even if they're not the correct notions

[Kyle Miller]

but I think it's important that definitions be proved by theorems

[Rémi Bottinelli]

yeah, mostly for cayley graphs I agree. But say this might be nice to formalize for instance, and here the labelling is very important..

[Rémi Bottinelli]

I think you were spot on with the remark that forgetting labels and loops is kind of losing everything for schreier graphs.

[Kyle Miller]

Yeah, I had Stallings foldings in mind earlier (not that I know much about their theory -- I've been to enough seminar talks about outer space)

[Rémi Bottinelli]

and e.g. the fact that a group is free iff it acts freely on a tree (iirc) needs to remember loops too I guess.

[Rémi Bottinelli]

or, more basic, the cayley graph of a group is a tree iff the generators generate it freely

[Kyle Miller]

I think I remember in "Office hours with a geometric group theorist" that they work with simple graphs, subdividing edges of graphs as necessary

[Rémi Bottinelli]

without orientation you lose info about involutions, and without labelling you get that your group is not the full automorphism group of the graph, but just embeds in it.

[Rémi Bottinelli]

Kyle Miller said:

I think I remember in "Office hours with a geometric group theorist" that they work with simple graphs, subdividing edges of graphs as necessary

but that's kind of a hack, isn't it?

[Rémi Bottinelli]

now you've convinced me :)

[Rémi Bottinelli]

I guess it's like: if you take your cayley/schreier graphs to contain the full orientation+labelling information, you can always simply get the underlying simple_graph and everything you need should translate easily

[Kyle Miller]

I think it's sort of like working with simplicial complexes (where simplices are identified with vertex subsets), how you need to do barycentric subdivisions to ensure different properties. Though I sometimes feel like this is a hack, since I like delta complexes (like in Hatcher's algebraic topology book)

[Rémi Bottinelli]

sounds right, yeah

[Rémi Bottinelli]

mmh, it's not so easy to map from prefunctor to simple_graph.hom because of the adjacency thing

[Rémi Bottinelli]

but I'm not sure this is such a big deal: we don't have to deal with graph morphisms that much on the simple_graph side

[Rémi Bottinelli]

So, to me, it makes sense to go first with the "full information" version, either based on quivers or on digraphs as you proposed.

[Rémi Bottinelli]

or, yeah, we could just try and push the dumb "geometric" approach and see how far this takes us

[Rémi Bottinelli]

Any idea why lean can't find the correct instance at the bijective_color line?

import combinatorics.quiver.basic
import group_theory.group_action.basic


open function

universes u v w

namespace quiver

section defs

class colored_quiver (V : Type*) (S : Type*) extends (quiver V) :=
(color : ∀ ⦃x y⦄, (hom x y) → S)

variables (V : Type*) {M : Type*} [has_smul M V] {S : Type*} (ι : S → M)

inductive schreier_graph.arrow : V → V → Sort*
| mk (m : S) (x : V) : schreier_graph.arrow (x) (ι m • x)

instance schreier_graph_colored_quiver : colored_quiver V S :=
{ hom := schreier_graph.arrow V ι,
  color := by {apply schreier_graph.arrow.rec, exact (λ s v, s)} }


set_option trace.class_instances true
lemma bijective_color {x y : V} : function.bijective (λ (a : x ⟶ y), colored_quiver.color a) := sorry

end defs

end quiver

[Kyle Miller]

It looks like you're missing [colored_quiver V S] in the arguments

[Rémi Bottinelli]

but why doesn't it get it from the instance just above?

[Kyle Miller]

Oh, right. I think it's because it can't infer S from the x --> y expression

[Rémi Bottinelli]

ah, let me try, thanks!

[Kyle Miller]

If you think you'll only use a single S for a given V (and use term tagging tricks to change S when you need to), then you can safely make S an out_param in the class.

[Rémi Bottinelli]

structure colored_prefunctor {V S V' S' : Type*} [colored_quiver V S] [colored_quiver V' S']
  (σ : S → S') extends prefunctor V V' :=
(color : ∀ {x y} (f : x ⟶ y), σ (color f) = color (map f))

Is it worth having a map of labelling as a parameter?

[Rémi Bottinelli]

Kyle Miller said:

If you think you'll only use a single S for a given V (and use term tagging tricks to change S when you need to), then you can safely make S an out_param in the class.

huh, that's above my technical expertise I fear!

[Rémi Bottinelli]

Rémi Bottinelli said:

structure colored_prefunctor {V S V' S' : Type*} [colored_quiver V S] [colored_quiver V' S']
  (σ : S → S') extends prefunctor V V' :=
(color : ∀ {x y} (f : x ⟶ y), σ (color f) = color (map f))

Is it worth having a map of labelling as a parameter?

Maybe I shouldn't rush with this. In your opinion, what should the way forward with this look like?

[Rémi Bottinelli]

I guess we have the following options:

• simple_graph for Cayley graphs, and potentially also for Schreier graphs, although it doesn't make as much sense.
  The upside is that it's quite easy to setup, and simple_graph has plenty of API to make things work. It should also cover everything we need for the "coarse" aspect of GGT.

• quiver-based Schreier and Cayley graphs. Here the API is quite thin in comparison, but on the theoretical side, we stay close to what we really "think of" as Cayley and Schreier graphs, and, modulo glue code, we should be able to translate to simple_graphs.
  I guess basing this on quivers has a potential advantage that it may actually help getting a better API around those? more lemmas and stuff.

• A new primitive, which allows not having to deal with the idiosyncracies of either encodings, but then you also have to redo most everything from scratch.

[Rémi Bottinelli]

Actually, your labelled_digraph doesn't allow for multiple arrows with same label between the same endpoints, does it?

[Antoine Labelle]

Kyle Miller said:

Given what I know about GGT, when groups act on graphs they're mostly simple graphs, so having a simple_graph.schreier_graph and a simple_graph.cayley_graph might not be so crazy, even if they're not the correct notions

Even if they act on simple graphs, the quotient is often not simple!

[Antoine Labelle]

Also, what about defining the Cayley graphof G with generating set S is as a quiver that comes with a covering map to the quiver that has a single vertex and on edge for each element of S? Then G is the group of automorphisms of this covering map (I think it's a natural way to encode the coloring, and it's personally how I think about Cayley graphs).

[Rémi Bottinelli]

I guess the advantage of this definition is that we don't even have to define any new kind of structure, in theory.

[Rémi Bottinelli]

Mmh, the quiver approach is much less fun to implement. The type dependences make everything quite a bit more painful

[Antoine Labelle]

I agree and I think that's the biggest issue with quiver. After making that comment I tried to see if I could define covering maps for quivers, and I quickly ran into issues of of the type "I want to prove that an edge from a to c is equal to an edge from b to c, where a is equal (but not definitionally) to b, so the two edges don't live in defeq types".

[Antoine Labelle]

That's why I like the approach of #16100, where we have a single type for all of the edges. It has the disadvantage of introducing a new type and thus requiring duplication of a lot of quiver API, but I feel like it's probably the best way to do multigraphs.

[Rémi Bottinelli]

Well, in this case at least we'd need to remove the involution. I'd be kind of sad to have to drop quivers, since that means a pretty big split, but maybe that's the best way… I'll work on this Schreier graph stuff a bit more using quivers and see how it fares

[Kyle Miller]

Would defining something like docs#simple_graph.walk.copy to move edges along some equalities help?

[Kyle Miller]

As far as I know, quivers don't have this (yet) because once you get to category theory you can make do with composition with identities associated to equalities -- but quivers don't have composition of arrows so this trick doesn't work.

[Antoine Labelle]

Rémi Bottinelli said:

Well, in this case at least we'd need to remove the involution. I'd be kind of sad to have to drop quivers, since that means a pretty big split, but maybe that's the best way… I'll work on this Schreier graph stuff a bit more using quivers and see how it fares

Yes, we could have a directed version and an undirected version extending it with the involution added.

[Rémi Bottinelli]

Might try the copy trick, though I'm not sure I've needed it until now (well, I haven't been aware of its need, rather :wink: ).

[Antoine Labelle]

For the record, here's an example of a "non-defeq types" issue that arises when trying to define covering maps. I think it would be solved by copy, but this feels very hacky, it would be nicer if all edges had the same type.

import combinatorics.quiver.path

universes v v₁ v₂ u u₁ u₂

open function quiver

variables {V : Type u₁} {W : Type u₂} [quiver.{v₁+1} V] [quiver.{v₂+1} W]

def in_link (v : V) := Σ w : V, w ⟶ v
def out_link (v : V) := Σ w : V, v ⟶ w

def in_link_map (F : prefunctor V W) (v : V) :
  in_link v → in_link (F.obj v) :=
λ e, ⟨F.obj e.1, F.map e.2⟩

def out_link_map (F : prefunctor V W) (v : V) :
  out_link v → out_link (F.obj v) :=
λ e, ⟨F.obj e.1, F.map e.2⟩

class is_covering_map (F : prefunctor V W) :=
(in_link_map_bijective : ∀ v, bijective (in_link_map F v))
(out_link_map_bijective : ∀ v, bijective (out_link_map F v))

variables (F : prefunctor V W) [is_covering_map F]

noncomputable def lift_edge (w : W) (v : V) (hv : F.obj v = w) :
  out_link w → out_link v :=
begin
  rw ←hv, intro e,
  exact surj_inv (is_covering_map.out_link_map_bijective v).2 e,
end

-- Lean doesn't accept this statement since the RHS has type `out_link w` while the LHS
-- has type `out_link (F.obj v)`.
lemma map_lift_edge (w : W) (v : V) (hv : F.obj v = w) (e : out_link w) :
  out_link_map F v (lift_edge F w v hv e) = e := sorry

[Rémi Bottinelli]

This one is one rec away from typechecking:

lemma map_lift_edge (w : W) (v : V) (hv : F.obj v = w) (e : out_link w) :
  out_link_map F v (lift_edge F w v hv e) = hv.symm.rec_on e := sorry

and the copy trick should work, or maybe rephrasing as

lemma map_lift_edge' (v : V) (e : out_link $ F.obj v) :
  out_link_map F v (lift_edge F (F.obj v) v rfl e) = e := sorry

?

[Rémi Bottinelli]

Ah, and actually, the covering approach provides an example of the argument that working with quivers will improve their api and benefit other sides of mathlib: Covering of groupoids are quite useful (I vaguely started there but then turned to other things). If we had a good api around coverings and lifting of paths in quivers, etc, it would make working with covering of groupoids that much easier.

[Rémi Bottinelli]

Maybe before starting Schreier/Cayley graphs, we'd need some preliminary work on overhauling the quiver code, adding the notion of forests, reduced paths, copy, covering, etc, and only start with Schreier/Cayley graphs then

[Kyle Miller]

@Antoine Labelle Using your example, here's how cast (a better name for copy) could work:

def out_link.cast {u v : V} (e : out_link u) (h : u = v) : out_link v :=
eq.rec e h

@[simp] lemma out_link.cast_rfl {u : V} (e : out_link u) : e.cast rfl = e := rfl

@[simp] lemma out_link.cast_cast {u v w : V} (e : out_link u) (hu : u = v) (hv : v = w) :
  (e.cast hu).cast hv = e.cast (hu.trans hv) := by { subst_vars, refl }

lemma map_lift_edge (w : W) (v : V) (hv : F.obj v = w) (e : out_link w) :
  out_link_map F v (lift_edge F w v hv e) = e.cast hv.symm :=
begin
  subst hv,
  exact surj_inv_eq (is_covering_map.out_link_map_bijective v).2 e,
end

[Kyle Miller]

I think this "cast pattern" should be considered to be a design pattern for working with dependent types. It provides a consistent interface for how you do rewrites on indices, which otherwise can get unweidly if you have unrestricted eq.recs in your expressions.

[Kyle Miller]

It might feel hacky because in category theory this is "evil" (you are not supposed to talk about equalities of objects, only isomorphisms), however quivers and graphs do not have isomorphisms, and maps between graphs (prefunctors) quickly reveal this to be an issue.

docs#simple_graph.walk.map_eq_of_eq is the type of lemma that revealed the need for an index cast

[Rémi Bottinelli]

Hey, so we've defined coverings of quivers here and the goal is to define Schreier graphs as quivers + a covering onto a bouquet.

After some discussions, I'm not sure whether we should bundle it as a struct containing the quiver and the covering, or just have the covering floating vaguely in the context. Similarly, we'll want to talk about covering morphisms and the automorphism group of Cayley graphs (probably), and it's becoming unclear the amount of bundling we should choose. A more basic question already leading to this is: how to define isomorphisms of quivers?

What do people with more experience with this kind of things think?

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/compare/master...bottine:mathlib:bottine/combinatorics.quiver/schreier?expand=1

Here is a new tentative. The file covering.lean has an open PR already. Three remarks/questions:

• For now the "covering" part is unbundled, which makes things a bit painful: all lemmas/defs need to be split into one about the quiver, and one about preserving the covering.
• Similarly, what's the proper way to say that a prefunctor is an isomorphism of quivers, beside providing a def for the inverse and two lemmas witnessing the inverse-ness?
• Finally, I'm breaking my teeth again on dependent types: I've got a sorry in from_coset_graph_to_coset_graph and to_coset_graph_from_coset_graph. This is a recurring pattern, and I always get confused as to how to close such goals (containing an eq.rec). What's the correct way to approach that? Partially solved thanks to Adam Topaz.

[Rémi Bottinelli]

(deleted)