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.

source

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

(V → W) → Type u_2

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

Equations

Quiver.Push x = W

Instances For

source

instance Quiver.instNonemptyPush {V : Type u_1} {W : Type u_2} (σ : V → W) [h : Nonempty W] :

Nonempty (Quiver.Push σ)

Equations

(_ : Nonempty (Quiver.Push σ)) = h

source

inductive Quiver.PushQuiver {V : Type u} [Quiver V] {W : Type u₂} (σ : V → W) :

W → W → Type (max u u₂ v)

arrow: {V : Type u} → [inst : Quiver V] → {W : Type u₂} → {σ : V → W} → {X Y : V} → (X ⟶ Y) → Quiver.PushQuiver σ (σ X) (σ Y)

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

Instances For

source

instance Quiver.instQuiverPush {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) :

Quiver (Quiver.Push σ)

Equations

Quiver.instQuiverPush σ = { Hom := Quiver.PushQuiver σ }

source

def Quiver.Push.of {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) :

V ⥤q Quiver.Push σ

The prefunctor induced by pushing arrows via σ

Equations

Quiver.Push.of σ = { obj := σ, map := fun {X Y} f => Quiver.PushQuiver.arrow f }

Instances For

source

@[simp]

theorem Quiver.Push.of_obj {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) :

(Quiver.Push.of σ).obj = σ

source

noncomputable def Quiver.Push.lift {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [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 σ.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Quiver.Push.lift_obj {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)) :

(Quiver.Push.lift σ φ τ h).obj = τ

source

theorem Quiver.Push.lift_comp {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)) :

Quiver.Push.of σ ⋙q Quiver.Push.lift σ φ τ h = φ

source

theorem Quiver.Push.lift_unique {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [Quiver W'] (φ : V ⥤q W') (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)) (Φ : Quiver.Push σ ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : Quiver.Push.of σ ⋙q Φ = φ) :

Φ = Quiver.Push.lift σ φ τ h