mathlib3 documentation

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
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) :
quiver.hom.cast hu 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'') :
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) :
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') :
quiver.hom.cast hu 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' = quiver.hom.cast hu 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 : quiver.path u v) :

Change the endpoints of a path using equalities.

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