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 #

source
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
source
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
source
@[simp]
theorem quiver.hom.cast_rfl_rfl {U : Type u_1} [quiver U] {u v : U} (e : u ⟶ v) :
quiver.hom.cast rfl rfl e = e
source
@[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'') :
quiver.hom.cast hu' hv' (quiver.hom.cast hu hv e) = quiver.hom.cast _ _ e
source
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) :
quiver.hom.cast hu hv e == e
source
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'
source
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 #

source
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) :
quiver.path u' v'

Change the endpoints of a path using equalities.

Equations
source
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
source
@[simp]
theorem quiver.path.cast_rfl_rfl {U : Type u_1} [quiver U] {u v : U} (p : quiver.path u v) :
quiver.path.cast rfl rfl p = p
source
@[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'') :
quiver.path.cast hu' hv' (quiver.path.cast hu hv p) = quiver.path.cast _ _ p
source
@[simp]
theorem quiver.path.cast_nil {U : Type u_1} [quiver 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 v u' v' : U} (hu : u = u') (hv : v = v') (p : quiver.path u v) :
quiver.path.cast hu hv p == p
source
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'
source
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
source
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') :
quiver.path.cast hu hw (p.cons e) = (quiver.path.cast hu rfl p).cons (quiver.hom.cast rfl hw e)
source
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') :
quiver.path.cast rfl _ p = p'
source
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') :
quiver.hom.cast _ rfl e = e'
source
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) :
quiver.path.cast _ rfl p = quiver.path.nil