Pushing a quiver structure along a map #

Given a map σ : V → W and a Quiver instance on V, this files defines a Quiver instance on W by associating to each arrow v ⟶ v' in V an arrow σ v ⟶ σ v' in W.

def Quiver.Push {V : Type u_1} {W : Type u_2} :
(VW)Type u_2

The Quiver instance obtained by pushing arrows of V along the map σ : V → W

Equations
Instances For
instance Quiver.instNonemptyPush {V : Type u_1} {W : Type u_2} (σ : VW) [h : ] :
Equations
• = h
inductive Quiver.PushQuiver {V : Type u} [] {W : Type u₂} (σ : VW) :
WWType (max u u₂ v)

The quiver structure obtained by pushing arrows of V along the map σ : V → W

Instances For
instance Quiver.instPush {V : Type u_1} [] {W : Type u_2} (σ : VW) :
Equations
• = { Hom := }
def Quiver.Push.of {V : Type u_1} [] {W : Type u_2} (σ : VW) :

The prefunctor induced by pushing arrows via σ

Equations
• = { obj := σ, map := fun {X Y : V} (f : X Y) => }
Instances For
@[simp]
theorem Quiver.Push.of_obj {V : Type u_1} [] {W : Type u_2} (σ : VW) :
().obj = σ
noncomputable def Quiver.Push.lift {V : Type u_1} [] {W : Type u_2} (σ : VW) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), φ.obj x = τ (σ x)) :
⥤q W'

Given a function τ : W → W' and a prefunctor φ : V ⥤q W', one can extend τ to be a prefunctor W ⥤q W' if τ and σ factorize φ at the level of objects, where W is given the pushforward quiver structure Push σ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Quiver.Push.lift_obj {V : Type u_1} [] {W : Type u_2} (σ : VW) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), φ.obj x = τ (σ x)) :
(Quiver.Push.lift σ φ τ h).obj = τ
theorem Quiver.Push.lift_comp {V : Type u_1} [] {W : Type u_2} (σ : VW) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), φ.obj x = τ (σ x)) :
⋙q Quiver.Push.lift σ φ τ h = φ
theorem Quiver.Push.lift_unique {V : Type u_1} [] {W : Type u_2} (σ : VW) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), φ.obj x = τ (σ x)) (Φ : ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : = φ) :
Φ = Quiver.Push.lift σ φ τ h