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} [Quiver U] {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

• Quiver.Hom.cast hu hv e = hu ▸ hv ▸ e

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

@[simp]

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

@[simp]

theorem Quiver.Hom.cast_cast {U : Type u_1} [Quiver U] {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) = Quiver.Hom.cast (_ : u = u'') (_ : v = v'') e

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

Change the endpoints of a path using equalities.

Equations

• Quiver.Path.cast hu hv p = hu ▸ hv ▸ p

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Quiver.Path.cast_eq_iff_heq {U : Type u_1} [Quiver U] {u : U} {v : U} {u' : 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' ↔ HEq p p'

theorem Quiver.Path.eq_cast_iff_heq {U : Type u_1} [Quiver U] {u : U} {v : U} {u' : 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 ↔ HEq p' p

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

theorem Quiver.cast_eq_of_cons_eq_cons {U : Type u_1} [Quiver U] {u : U} {v : U} {v' : U} {w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w} {e' : v' ⟶ w} (h : Quiver.Path.cons p e = Quiver.Path.cons p' e') : Quiver.Path.cast (_ : u = u) (_ : v = v') p = p'

theorem Quiver.hom_cast_eq_of_cons_eq_cons {U : Type u_1} [Quiver U] {u : U} {v : U} {v' : U} {w : U} {p : Quiver.Path u v} {p' : Quiver.Path u v'} {e : v ⟶ w} {e' : v' ⟶ w} (h : Quiver.Path.cons p e = Quiver.Path.cons p' e') : Quiver.Hom.cast (_ : v = v') (_ : w = w) e = e'

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