Rewriting arrows and paths along vertex equalities

This file 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.

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) : cast hu hv e = _root_.cast ⋯ e

@[simp]

theorem Quiver.Hom.cast_rfl_rfl {U : Type u_1} [Quiver U] {u v : U} (e : u ⟶ v) : cast ⋯ ⋯ e = e

@[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'') : cast hu' hv' (cast hu hv e) = cast ⋯ ⋯ 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) : cast hu 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') : 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' = 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 : Path u v) : Path u' v'

Change the endpoints of a path using equalities.

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

@[simp]

theorem Quiver.Path.cast_rfl_rfl {U : Type u_1} [Quiver U] {u v : U} (p : Path u v) : cast ⋯ ⋯ p = p

@[simp]

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

@[simp]

theorem Quiver.Path.cast_nil {U : Type u_1} [Quiver U] {u u' : U} (hu : u = u') : cast hu hu nil = nil

theorem Quiver.Path.cast_heq {U : Type u_1} [Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) : cast hu 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 : Path u v) (p' : Path u' v') : 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 : Path u v) (p' : Path u' v') : p' = cast hu hv p ↔ p' ≍ p

theorem Quiver.Path.cast_cons {U : Type u_1} [Quiver U] {u v w u' w' : U} (p : Path u v) (e : v ⟶ w) (hu : u = u') (hw : w = w') : cast hu hw (p.cons e) = (cast hu ⋯ p).cons (Hom.cast ⋯ hw e)

theorem Quiver.cast_eq_of_cons_eq_cons {U : Type u_1} [Quiver U] {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') : Path.cast ⋯ ⋯ p = p'

theorem Quiver.hom_cast_eq_of_cons_eq_cons {U : Type u_1} [Quiver U] {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') : Hom.cast ⋯ ⋯ e = e'

theorem Quiver.eq_nil_of_length_zero {U : Type u_1} [Quiver U] {u v : U} (p : Path u v) (hzero : p.length = 0) : Path.cast ⋯ ⋯ p = Path.nil