Documentation

Mathlib.Combinatorics.Quiver.Cast

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 v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) :
u' ⟶ v'

Change the endpoints of an arrow using equalities.

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

      Change the endpoints of a path using equalities.

      Equations
        Instances For
          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 : Path u v) :
          cast hu hv p = _root_.cast ⋯ p
          source
          @[simp]
          theorem Quiver.Path.cast_rfl_rfl {U : Type u_1} [Quiver U] {u v : U} (p : Path u v) :
          cast ⋯ ⋯ p = p
          source
          @[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
          source
          @[simp]
          theorem Quiver.Path.cast_nil {U : Type u_1} [Quiver U] {u u' : U} (hu : u = u') :
          cast hu hu nil = 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 : Path u v) :
          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 : Path u v) (p' : Path u' v') :
          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 : Path u v) (p' : Path u' v') :
          p' = 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 : 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)
          source
          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'
          source
          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'
          source
          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