[Merged by Bors] - feat(combinatorics/quiver/*) cast arrows and paths along equalities

src/combinatorics/quiver/basic.lean

@@ -86,6 +86,12 @@ def comp {U : Type*} [quiver U] {V : Type*} [quiver V] {W : Type*} [quiver W]
 { obj := λ X, G.obj (F.obj X),
   map := λ X Y f, G.map (F.map f), }
 
+@[simp] lemma comp_id {U : Type*} [quiver U] {V : Type*} [quiver V] (F : prefunctor U V) :
+  F.comp (id _) = F := by { cases F, refl, }
+
+@[simp] lemma id_comp {U : Type*} [quiver U] {V : Type*} [quiver V] (F : prefunctor U V) :
+  (id _).comp F = F := by { cases F, refl, }
+
 @[simp]
 lemma comp_assoc
   {U V W Z : Type*} [quiver U] [quiver V] [quiver W] [quiver Z]
@@ -125,7 +131,6 @@ instance empty_quiver (V : Type u) : quiver.{u} (empty V) := ⟨λ a b, pempty
 
 @[simp] lemma empty_arrow {V : Type u} (a b : empty V) : (a ⟶ b) = pempty := rfl
 
-
 /-- A quiver is thin if it has no parallel arrows. -/
 @[reducible] def is_thin (V : Type u) [quiver V] := ∀ (a b : V), subsingleton (a ⟶ b)
 

src/combinatorics/quiver/cast.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2022 Antoine Labelle, Rémi Bottinelli. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Labelle, Rémi Bottinelli
+-/
+import combinatorics.quiver.basic
+import combinatorics.quiver.path
+
+/-!
+
+# Rewriting arrows and paths along vertex equalities
+
+This files defines `hom.cast` and `path.cast` (and associated lemmas) in order to allow
+rewriting arrows and paths along equalities of their endpoints.
+
+-/
+
+universes v v₁ v₂ u u₁ u₂
+
+variables {U : Type*} [quiver.{u+1} U]
+
+namespace quiver
+
+/-!
+### Rewriting arrows along equalities of vertices
+-/
+
+/-- Change the endpoints of an arrow using equalities. -/
+def hom.cast {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) : u' ⟶ v' :=
+eq.rec (eq.rec e hv) hu
+
+lemma hom.cast_eq_cast {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) :
+  e.cast hu hv = cast (by rw [hu, hv]) e :=
+by { subst_vars, refl }
+
+@[simp] lemma hom.cast_rfl_rfl {u v : U} (e : u ⟶ v) :
+  e.cast rfl rfl = e := rfl
+
+@[simp] lemma hom.cast_cast {u v u' v' u'' v'' : U} (e : u ⟶ v)
+  (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
+  (e.cast hu hv).cast hu' hv' = e.cast (hu.trans hu') (hv.trans hv') :=
+by { subst_vars, refl }
+
+lemma hom.cast_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) :
+  e.cast hu hv == e :=
+by { subst_vars, refl }
+
+lemma hom.cast_eq_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v')
+  (e : u ⟶ v) (e' : u' ⟶ v') : e.cast hu hv = e' ↔ e == e' :=
+by { rw hom.cast_eq_cast, exact cast_eq_iff_heq }
+
+lemma hom.eq_cast_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v')
+  (e : u ⟶ v) (e' : u' ⟶ v') : e' = e.cast hu hv ↔ e' == e :=
+by { rw [eq_comm, hom.cast_eq_iff_heq], exact ⟨heq.symm, heq.symm⟩ }
+
+/-!
+### Rewriting paths along equalities of vertices
+-/
+
+open path
+
+/-- Change the endpoints of a path using equalities. -/
+def path.cast {u v u' v' : U} (hu : u = u') (hv : v = v') (p : path u v) : path u' v' :=
+eq.rec (eq.rec p hv) hu
+
+lemma path.cast_eq_cast {u v u' v' : U} (hu : u = u') (hv : v = v') (p : path u v) :
+  p.cast hu hv = cast (by rw [hu, hv]) p:=
+eq.drec (eq.drec (eq.refl (path.cast (eq.refl u) (eq.refl v) p)) hu) hv
+
+@[simp] lemma path.cast_rfl_rfl {u v : U} (p : path u v) :
+  p.cast rfl rfl = p := rfl
+
+@[simp] lemma path.cast_cast {u v u' v' u'' v'' : U} (p : path u v)
+  (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
+  (p.cast hu hv).cast hu' hv' = p.cast (hu.trans hu') (hv.trans hv') :=
+by { subst_vars, refl }
+
+@[simp] lemma path.cast_nil {u u' : U} (hu : u = u') :
+  (path.nil : path u u).cast hu hu = path.nil :=
+by { subst_vars, refl }
+
+lemma path.cast_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : path u v) :
+  p.cast hu hv == p :=
+by { rw path.cast_eq_cast, exact cast_heq _ _ }
+
+lemma path.cast_eq_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v')
+  (p : path u v) (p' : path u' v') : p.cast hu hv = p' ↔ p == p' :=
+by { rw path.cast_eq_cast, exact cast_eq_iff_heq }
+
+lemma path.eq_cast_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v')
+  (p : path u v) (p' : path u' v') : p' = p.cast hu hv ↔ p' == p :=
+⟨λ h, ((p.cast_eq_iff_heq hu hv p').1 h.symm).symm,
+ λ h, ((p.cast_eq_iff_heq hu hv p').2 h.symm).symm⟩
+
+lemma path.cast_cons {u v w u' w' : U} (p : path u v) (e : v ⟶ w) (hu : u = u') (hw : w = w') :
+  (p.cons e).cast hu hw = (p.cast hu rfl).cons (e.cast rfl hw) :=
+by { subst_vars, refl }
+
+lemma cast_eq_of_cons_eq_cons {u v v' w : U} {p : path u v} {p' : path u v'}
+  {e : v ⟶ w} {e' : v' ⟶ w} (h : p.cons e = p'.cons e') :
+  p.cast rfl (obj_eq_of_cons_eq_cons h) = p' :=
+by { rw path.cast_eq_iff_heq, exact heq_of_cons_eq_cons h }
+
+lemma hom_cast_eq_of_cons_eq_cons {u v v' w : U} {p : path u v} {p' : path u v'}
+  {e : v ⟶ w} {e' : v' ⟶ w} (h : p.cons e = p'.cons e') :
+  e.cast (obj_eq_of_cons_eq_cons h) rfl = e' :=
+by { rw hom.cast_eq_iff_heq, exact hom_heq_of_cons_eq_cons h }
+
+lemma eq_nil_of_length_zero {u v : U} (p : path u v) (hzero : p.length = 0) :
+  p.cast (eq_of_length_zero p hzero) rfl = path.nil :=
+by { cases p; simpa only [nat.succ_ne_zero, length_cons] using hzero, }
+
+end quiver

src/combinatorics/quiver/path.lean

@@ -30,7 +30,20 @@ path.nil.cons e
 
 namespace path
 
-variables {V : Type u} [quiver V] {a b c : V}
+variables {V : Type u} [quiver V] {a b c d : V}
+
+lemma nil_ne_cons (p : path a b) (e : b ⟶ a) : path.nil ≠ p.cons e.
+
+lemma cons_ne_nil (p : path a b) (e : b ⟶ a) : p.cons e ≠ path.nil.
+
+lemma obj_eq_of_cons_eq_cons {p : path a b} {p' : path a c}
+  {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : b = c := by injection h
+
+lemma heq_of_cons_eq_cons {p : path a b} {p' : path a c}
+  {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : p == p' := by injection h
+
+lemma hom_heq_of_cons_eq_cons {p : path a b} {p' : path a c}
+  {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : e == e' := by injection h
 
 /-- The length of a path is the number of arrows it uses. -/
 def length {a : V} : Π {b : V}, path a b → ℕ
@@ -55,10 +68,13 @@ def comp {a b : V} : Π {c}, path a b → path b c → path a c
 
 @[simp] lemma comp_cons {a b c d : V} (p : path a b) (q : path b c) (e : c ⟶ d) :
   p.comp (q.cons e) = (p.comp q).cons e := rfl
+
 @[simp] lemma comp_nil {a b : V} (p : path a b) : p.comp path.nil = p := rfl
+
 @[simp] lemma nil_comp {a : V} : ∀ {b} (p : path a b), path.nil.comp p = p
 | a path.nil := rfl
 | b (path.cons p e) := by rw [comp_cons, nil_comp]
+
 @[simp] lemma comp_assoc {a b c : V} : ∀ {d}
   (p : path a b) (q : path b c) (r : path c d),
     (p.comp q).comp r = p.comp (q.comp r)