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 #

source

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.

Instances For

source

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

source

@[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

source

@[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

source

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

source

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'

source

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 #

source

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.

Instances For

source

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

source

@[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

source

@[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

source

@[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

source

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

source

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'

source

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

source

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)

source

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'

source

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'

source

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