# mathlib3documentation

combinatorics.quiver.push

# Pushing a quiver structure along a map #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[nolint]
def quiver.push {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) :
Type u_3

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

Equations
• = W
Instances for quiver.push
@[protected, instance]
def quiver.push.nonempty {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) [h : nonempty W] :
@[nolint]
inductive quiver.push_quiver {V : Type u} [quiver V] {W : Type u₂} (σ : V W) :
W W Type (max u u₂ v)

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

Instances for quiver.push_quiver
• quiver.push_quiver.has_sizeof_inst
@[protected, instance]
def quiver.push.quiver {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) :
Equations
def quiver.push.of {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) :

The prefunctor induced by pushing arrows via σ

Equations
Instances for quiver.push.of
@[simp]
theorem quiver.push.of_obj {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) :
.obj = σ
def quiver.push.lift {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) {W' : Type u_4} [quiver W'] (φ : V ⥤q W') (τ : W W') (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
• τ h = {obj := τ, map := quiver.push_quiver.rec (λ (X Y : V) (f : X Y), _.mpr (_.mpr (φ.map f)))}
theorem quiver.push.lift_obj {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) {W' : Type u_4} [quiver W'] (φ : V ⥤q W') (τ : W W') (h : (x : V), φ.obj x = τ (σ x)) :
φ τ h).obj = τ
theorem quiver.push.lift_comp {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) {W' : Type u_4} [quiver W'] (φ : V ⥤q W') (τ : W W') (h : (x : V), φ.obj x = τ (σ x)) :
⋙q τ h = φ
theorem quiver.push.lift_unique {V : Type u_1} [quiver V] {W : Type u_3} (σ : V W) {W' : Type u_4} [quiver W'] (φ : V ⥤q W') (τ : W W') (h : (x : V), φ.obj x = τ (σ x)) (Φ : ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : = φ) :
Φ = τ h