Zulip Chat Archive
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
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,(rflrfl)⟩, 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,(lr)⟩,
{ 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,(rflrfl)⟩⟩,
{ 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 (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.
Yaël Dillies (Nov 08 2022 at 10:37):
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_graph
s 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 ToddCoxeter 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 Gsets. So morphisms of Gsets <> 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)
what about this?
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 colorpreserving 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
/ Labelpreserving 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 graphlike 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 givenV
(and use term tagging tricks to changeS
when you need to), then you can safely makeS
anout_param
in theclass
.
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, andsimple_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 tosimple_graph
s.
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 asimple_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 "nondefeq 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 (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,
exact surj_inv_eq (is_covering_map.out_link_map_bijective v).2 e,
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.rec
s 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):
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 inverseness?
Finally, I'm breaking my teeth again on dependent types: I've got a sorry inPartially solved thanks to Adam Topaz.from_coset_graph_to_coset_graph
andto_coset_graph_from_coset_graph
. This is a recurring pattern, and I always get confused as to how to close such goals (containing aneq.rec
). What's the correct way to approach that?
Rémi Bottinelli (Feb 22 2023 at 16:32):
(deleted)
Last updated: Dec 20 2023 at 11:08 UTC