Documentation

Mathlib.Combinatorics.Quiver.Push

Pushing a quiver structure along a map #

Given a map σ : V → W and a Quiver instance on V, this file 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

Instances For
    source
    instance Quiver.instNonemptyPush {V : Type u_1} {W : Type u_2} (σ : V → W) [h : Nonempty W] :
    Nonempty (Push σ)
    source
    inductive Quiver.PushQuiver {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
      source
      @[instance_reducible]
      instance Quiver.instPush {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) :
      Quiver (Push σ)
      source
      def Quiver.Push.of {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) :
      V ⥤q Push σ

      The prefunctor induced by pushing arrows via σ

      Instances For
        source
        @[simp]
        theorem Quiver.Push.of_obj {V : Type u_1} [Quiver V] {W : Type u_2} (σ : V → W) :
        (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)) :
        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 σ.

        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)) :
          (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)) :
          of σ ⋙q 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)) (Φ : Push σ ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : of σ ⋙q Φ = φ) :
          Φ = lift σ φ τ h