Documentation

Mathlib.Combinatorics.Quiver.Push

Pushing a quiver structure along a map #

Given a map σ : V → W→ W and a Quiver instance on V, this files defines a quiver instance on W by associating to each arrow v ⟶ v'⟶ v' in V an arrow σ v ⟶ σ 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→ W

Equations
inductive Quiver.PushQuiver {V : Type u} [inst : Quiver V] {W : Type u₂} (σ : VW) :
WWType (maxuu₂v)

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

Instances For
    instance Quiver.instQuiverPush {V : Type u_1} [inst : Quiver V] {W : Type u_3} (σ : VW) :
    Equations
    def Quiver.Push.of {V : Type u_1} [inst : Quiver V] {W : Type u_3} (σ : VW) :

    The prefunctor induced by pushing arrows via σ

    Equations
    @[simp]
    theorem Quiver.Push.of_obj {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : VW) :
    (Quiver.Push.of σ).obj = σ
    noncomputable def Quiver.Push.lift {V : Type u_1} [inst : Quiver V] {W : Type u_3} (σ : VW) {W' : Type u_4} [inst : Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), Prefunctor.obj φ x = τ (σ x)) :

    Given a function τ : W → W'→ W' and a prefunctor φ : V ⥤q W'⥤q W', one can extend τ to be a prefunctor W ⥤q 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.
    theorem Quiver.Push.lift_obj {V : Type u_3} [inst : Quiver V] {W : Type u_1} (σ : VW) {W' : Type u_2} [inst : Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), Prefunctor.obj φ x = τ (σ x)) :
    (Quiver.Push.lift σ φ τ h).obj = τ
    theorem Quiver.Push.lift_comp {V : Type u_1} [inst : Quiver V] {W : Type u_5} (σ : VW) {W' : Type u_3} [inst : Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), Prefunctor.obj φ x = τ (σ x)) :
    theorem Quiver.Push.lift_unique {V : Type u_1} [inst : Quiver V] {W : Type u_3} (σ : VW) {W' : Type u_5} [inst : Quiver W'] (φ : V ⥤q W') (τ : WW') (h : ∀ (x : V), Prefunctor.obj φ x = τ (σ x)) (Φ : Quiver.Push σ ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : Quiver.Push.of σ ⋙q Φ = φ) :
    Φ = Quiver.Push.lift σ φ τ h