## Stream: graph theory

### Topic: Cayley graphs (again)

#### Rémi Bottinelli (Nov 08 2022 at 10:31):

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
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,
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)

(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,
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 (Nov 08 2022 at 10:33):

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

#### Rémi Bottinelli (Nov 08 2022 at 10:34):

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

#### Rémi Bottinelli (Nov 08 2022 at 10:36):

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 (Nov 08 2022 at 10:37):

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

Okay sure

#### Rémi Bottinelli (Nov 08 2022 at 10:38):

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 (Nov 08 2022 at 12:42):

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 (Nov 08 2022 at 12:52):

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 (Nov 08 2022 at 12:59):

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 (Nov 08 2022 at 13:03):

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 (Nov 08 2022 at 13:05):

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 (Nov 08 2022 at 13:05):

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

#### Rémi Bottinelli (Nov 08 2022 at 13:06):

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

#### Kyle Miller (Nov 08 2022 at 13:09):

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 (Nov 08 2022 at 13:10):

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

#### Rémi Bottinelli (Nov 08 2022 at 13:16):

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

#### Rémi Bottinelli (Nov 08 2022 at 13:22):

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


#### Kyle Miller (Nov 08 2022 at 13:24):

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 (Nov 08 2022 at 13:24):

Another possibility is to start developing the theory of labeled digraphs

#### Kyle Miller (Nov 08 2022 at 13:24):

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 (Nov 08 2022 at 13:26):

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 (Nov 08 2022 at 13:28):

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 (Nov 08 2022 at 13:32):

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

#### Kyle Miller (Nov 08 2022 at 13:33):

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 (Nov 08 2022 at 13:34):

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

#### Rémi Bottinelli (Nov 08 2022 at 13:34):

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 (Nov 08 2022 at 13:35):

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

#### Kyle Miller (Nov 08 2022 at 13:35):

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 (Nov 08 2022 at 13:35):

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 (Nov 08 2022 at 13:36):

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

#### Kyle Miller (Nov 08 2022 at 13:37):

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 (Nov 08 2022 at 13:37):

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 (Nov 08 2022 at 13:37):

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 (Nov 08 2022 at 13:37):

now you've convinced me :)

#### Rémi Bottinelli (Nov 08 2022 at 13:38):

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 (Nov 08 2022 at 13:38):

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 (Nov 08 2022 at 13:44):

sounds right, yeah

#### Rémi Bottinelli (Nov 08 2022 at 13:49):

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

#### Rémi Bottinelli (Nov 08 2022 at 13:50):

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 (Nov 08 2022 at 13:59):

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 (Nov 08 2022 at 14:29):

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

#### Rémi Bottinelli (Nov 08 2022 at 15:37):

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 (Nov 08 2022 at 15:42):

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

#### Rémi Bottinelli (Nov 08 2022 at 15:44):

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

#### Kyle Miller (Nov 08 2022 at 15:45):

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

#### Rémi Bottinelli (Nov 08 2022 at 15:46):

ah, let me try, thanks!

#### Kyle Miller (Nov 08 2022 at 15:46):

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 (Nov 08 2022 at 15:46):

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 (Nov 08 2022 at 15:47):

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 (Nov 08 2022 at 15:48):

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 (Nov 08 2022 at 15:54):

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 (Nov 08 2022 at 18:19):

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

#### Antoine Labelle (Nov 08 2022 at 19:39):

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 (Nov 08 2022 at 19:45):

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 (Nov 09 2022 at 06:16):

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 (Nov 09 2022 at 10:45):

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

#### Antoine Labelle (Nov 09 2022 at 15:52):

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 (Nov 09 2022 at 15:54):

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 (Nov 09 2022 at 16:15):

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 (Nov 09 2022 at 16:31):

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

#### Kyle Miller (Nov 09 2022 at 16:31):

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 (Nov 09 2022 at 16:42):

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 (Nov 09 2022 at 18:24):

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 (Nov 09 2022 at 20:51):

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) :
λ e, ⟨F.obj e.1, F.map e.2⟩

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

class is_covering_map (F : prefunctor V W) :=

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

noncomputable def lift_edge (w : W) (v : V) (hv : F.obj v = w) :
begin
rw ←hv, intro 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 (Nov 10 2022 at 06:21):

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 (Nov 10 2022 at 07:21):

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 (Nov 10 2022 at 07:25):

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 (Nov 10 2022 at 09:16):

@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,
end


#### Kyle Miller (Nov 10 2022 at 09:18):

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 (Nov 10 2022 at 09:22):

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 (Dec 05 2022 at 12:34):

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 (Feb 22 2023 at 16:31):

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 (Feb 22 2023 at 16:32):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC