# 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.

### Rewriting arrows along equalities of vertices #

def Quiver.Hom.cast {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (e : u v) :
u' v'

Change the endpoints of an arrow using equalities.

Equations
Instances For
theorem Quiver.Hom.cast_eq_cast {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (e : u v) :
Quiver.Hom.cast hu hv e = cast e
@[simp]
theorem Quiver.Hom.cast_rfl_rfl {U : Type u_1} [] {u : U} {v : U} (e : u v) :
= e
@[simp]
theorem Quiver.Hom.cast_cast {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} {u'' : U} {v'' : U} (e : u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
Quiver.Hom.cast hu' hv' (Quiver.Hom.cast hu hv e) =
theorem Quiver.Hom.cast_heq {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (e : u v) :
HEq (Quiver.Hom.cast hu hv e) e
theorem Quiver.Hom.cast_eq_iff_heq {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (e : u v) (e' : u' v') :
Quiver.Hom.cast hu hv e = e' HEq e e'
theorem Quiver.Hom.eq_cast_iff_heq {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (e : u v) (e' : u' v') :
e' = Quiver.Hom.cast hu hv e HEq e' e

### Rewriting paths along equalities of vertices #

def Quiver.Path.cast {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (p : ) :

Change the endpoints of a path using equalities.

Equations
Instances For
theorem Quiver.Path.cast_eq_cast {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (p : ) :
Quiver.Path.cast hu hv p = cast p
@[simp]
theorem Quiver.Path.cast_rfl_rfl {U : Type u_1} [] {u : U} {v : U} (p : ) :
= p
@[simp]
theorem Quiver.Path.cast_cast {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} {u'' : U} {v'' : U} (p : ) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
@[simp]
theorem Quiver.Path.cast_nil {U : Type u_1} [] {u : U} {u' : U} (hu : u = u') :
Quiver.Path.cast hu hu Quiver.Path.nil = Quiver.Path.nil
theorem Quiver.Path.cast_heq {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (p : ) :
HEq (Quiver.Path.cast hu hv p) p
theorem Quiver.Path.cast_eq_iff_heq {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (p : ) (p' : Quiver.Path u' v') :
Quiver.Path.cast hu hv p = p' HEq p p'
theorem Quiver.Path.eq_cast_iff_heq {U : Type u_1} [] {u : U} {v : U} {u' : U} {v' : U} (hu : u = u') (hv : v = v') (p : ) (p' : Quiver.Path u' v') :
p' = Quiver.Path.cast hu hv p HEq p' p
theorem Quiver.Path.cast_cons {U : Type u_1} [] {u : U} {v : U} {w : U} {u' : U} {w' : U} (p : ) (e : v w) (hu : u = u') (hw : w = w') :
Quiver.Path.cast hu hw (p.cons e) = (Quiver.Path.cast hu p).cons (Quiver.Hom.cast hw e)
theorem Quiver.cast_eq_of_cons_eq_cons {U : Type u_1} [] {u : U} {v : U} {v' : U} {w : U} {p : } {p' : Quiver.Path u v'} {e : v w} {e' : v' w} (h : p.cons e = p'.cons e') :
= p'
theorem Quiver.hom_cast_eq_of_cons_eq_cons {U : Type u_1} [] {u : U} {v : U} {v' : U} {w : U} {p : } {p' : Quiver.Path u v'} {e : v w} {e' : v' w} (h : p.cons e = p'.cons e') :
= e'
theorem Quiver.eq_nil_of_length_zero {U : Type u_1} [] {u : U} {v : U} (p : ) (hzero : p.length = 0) :
= Quiver.Path.nil