mathlib3documentation

combinatorics.quiver.cast

Rewriting arrows and paths along vertex equalities #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u v) :
u' v'

Change the endpoints of an arrow using equalities.

Equations
• hv e = eq.rec (eq.rec e hv) hu
theorem quiver.hom.cast_eq_cast {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u v) :
hv e = cast _ e
@[simp]
theorem quiver.hom.cast_rfl_rfl {U : Type u_1} [quiver U] {u v : U} (e : u v) :
@[simp]
theorem quiver.hom.cast_cast {U : Type u_1} [quiver U] {u v u' v' u'' v'' : U} (e : u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
hv' hv e) = e
theorem quiver.hom.cast_heq {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u v) :
hv e == e
theorem quiver.hom.cast_eq_iff_heq {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u v) (e' : u' v') :
hv e = e' e == e'
theorem quiver.hom.eq_cast_iff_heq {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u v) (e' : u' v') :
e' = hv e e' == e

Rewriting paths along equalities of vertices #

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

Change the endpoints of a path using equalities.

Equations
• hv p = eq.rec (eq.rec p hv) hu
theorem quiver.path.cast_eq_cast {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : v) :
hv p = cast _ p
@[simp]
theorem quiver.path.cast_rfl_rfl {U : Type u_1} [quiver U] {u v : U} (p : v) :
@[simp]
theorem quiver.path.cast_cast {U : Type u_1} [quiver U] {u v u' v' u'' v'' : U} (p : v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
hv' hv p) = p
@[simp]
theorem quiver.path.cast_nil {U : Type u_1} [quiver U] {u u' : U} (hu : u = u') :
theorem quiver.path.cast_heq {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : v) :
hv p == p
theorem quiver.path.cast_eq_iff_heq {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : v) (p' : v') :
hv p = p' p == p'
theorem quiver.path.eq_cast_iff_heq {U : Type u_1} [quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : v) (p' : v') :
p' = hv p p' == p
theorem quiver.path.cast_cons {U : Type u_1} [quiver U] {u v w u' w' : U} (p : v) (e : v w) (hu : u = u') (hw : w = w') :
hw (p.cons e) = p).cons e)
theorem quiver.cast_eq_of_cons_eq_cons {U : Type u_1} [quiver U] {u v v' w : U} {p : v} {p' : 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} [quiver U] {u v v' w : U} {p : v} {p' : 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} [quiver U] {u v : U} (p : v) (hzero : p.length = 0) :