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]
The quiver instance obtained by pushing arrows of V along the map σ : V → W
Equations
- quiver.push σ = 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] :
nonempty (quiver.push σ)
@[nolint]
- arrow : Π {V : Type u} [_inst_2 : quiver V] {W : Type u₂} {σ : V → W} {X Y : V}, (X ⟶ Y) → quiver.push_quiver σ (σ X) (σ Y)
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) :
quiver (quiver.push σ)
Equations
- quiver.push.quiver σ = {hom := quiver.push_quiver σ}
The prefunctor induced by pushing arrows via σ
Equations
- quiver.push.of σ = {obj := σ, map := λ (X Y : V) (f : X ⟶ Y), quiver.push_quiver.arrow f}
Instances for quiver.push.of
@[simp]
theorem
quiver.push.of_obj
{V : Type u_1}
[quiver V]
{W : Type u_3}
(σ : V → W) :
(quiver.push.of σ).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)) :
quiver.push σ ⥤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 σ.