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
Instances For
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 ⋯ e
@[simp]
theorem
Quiver.Hom.cast_rfl_rfl
{U : Type u_1}
[Quiver U]
{u : U}
{v : U}
(e : u ⟶ v)
:
Quiver.Hom.cast ⋯ ⋯ 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 ⋯ ⋯ 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
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
Instances For
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 ⋯ 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 ⋯ ⋯ 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 ⋯ ⋯ 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 (p.cons e) = (Quiver.Path.cast hu ⋯ p).cons (Quiver.Hom.cast ⋯ 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 : p.cons e = p'.cons e')
:
Quiver.Path.cast ⋯ ⋯ 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 : p.cons e = p'.cons e')
:
Quiver.Hom.cast ⋯ ⋯ 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 : p.length = 0)
:
Quiver.Path.cast ⋯ ⋯ p = Quiver.Path.nil