Mathlib.Combinatorics.Quiver.Push

Quiver.Push definition

(_ : V → W)

Full source

/-- The `Quiver` instance obtained by pushing arrows of `V` along the map `σ : V → W` -/
@[nolint unusedArguments]
def Push (_ : V → W) :=
  W

Pushed quiver structure along a map

Informal description

Given a map $\sigma : V \to W$ and a quiver structure on $V$, the quiver structure on $W$ is defined by associating to each arrow $v \to v'$ in $V$ an arrow $\sigma(v) \to \sigma(v')$ in $W$.

Quiver.instNonemptyPush instance

[h : Nonempty W] : Nonempty (Push σ)

Full source

instance [h : Nonempty W] : Nonempty (Push σ) :=
  h

Nonemptiness of Pushed Quiver Structure

Informal description

For any nonempty type $W$ and map $\sigma : V \to W$, the pushed quiver structure on $W$ is nonempty.

Quiver.PushQuiver inductive

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

Full source

/-- The quiver structure obtained by pushing arrows of `V` along the map `σ : V → W` -/
inductive PushQuiver {V : Type u} [Quiver.{v} V] {W : Type u₂} (σ : V → W) : W → W → Type max u u₂ v
  | arrow {X Y : V} (f : X ⟶ Y) : PushQuiver σ (σ X) (σ Y)

Pushed quiver structure along a map

Informal description

Given a quiver structure on a type $V$ and a map $\sigma : V \to W$, the `PushQuiver` construction defines a quiver structure on $W$ where for any two elements $w, w' \in W$, the type of arrows from $w$ to $w'$ consists of all arrows in $V$ from $v$ to $v'$ such that $\sigma(v) = w$ and $\sigma(v') = w'$.

Quiver.instPush instance

: Quiver (Push σ)

Full source

instance : Quiver (Push σ) :=
  ⟨PushQuiver σ⟩

Pushforward Quiver Structure Along a Map

Informal description

Given a map $\sigma : V \to W$ and a quiver structure on $V$, the pushforward quiver structure on $W$ is defined by associating to each arrow $v \to v'$ in $V$ an arrow $\sigma(v) \to \sigma(v')$ in $W$.

Quiver.Push.of definition

: V ⥤q Push σ

Full source

/-- The prefunctor induced by pushing arrows via `σ` -/
def of : V ⥤q Push σ where
  obj := σ
  map f := PushQuiver.arrow f

Prefunctor induced by pushing arrows via $\sigma$

Informal description

Given a map $\sigma : V \to W$ and a quiver structure on $V$, the prefunctor $\text{Quiver.Push.of}$ maps each vertex $v$ in $V$ to $\sigma(v)$ in $W$ and each arrow $f : v \to v'$ in $V$ to the corresponding arrow $\sigma(v) \to \sigma(v')$ in the pushforward quiver structure on $W$.

Quiver.Push.of_obj theorem

: (of σ).obj = σ

Full source

@[simp]
theorem of_obj : (of σ).obj = σ :=
  rfl

Object Map of Pushforward Prefunctor Equals $\sigma$

Informal description

The object map of the prefunctor $\text{Quiver.Push.of}$ induced by pushing arrows via $\sigma$ is equal to $\sigma$ itself, i.e., $(\text{of}\ \sigma).\text{obj} = \sigma$.

Quiver.Push.lift definition

: Push σ ⥤q W'

Full source

/-- 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 σ`. -/
noncomputable def lift : PushPush σ ⥤q W' where
  obj := τ
  map :=
    @PushQuiver.rec V _ W σ (fun X Y _ => τ X ⟶ τ Y) @fun X Y f => by
      dsimp only
      rw [← h X, ← h Y]
      exact φ.map f

Lift of a prefunctor through a pushforward quiver structure

Informal description

Given a map $\sigma : V \to W$, a prefunctor $\varphi : V \to W'$, and a function $\tau : W \to W'$ such that $\tau \circ \sigma = \varphi$ on objects, the prefunctor $\text{Quiver.Push.lift}$ from the pushforward quiver structure on $W$ to $W'$ is defined by: - On objects: $\tau$ - On arrows: For any arrow $\sigma(v) \to \sigma(v')$ in the pushforward quiver structure (induced by an arrow $v \to v'$ in $V$), the corresponding arrow in $W'$ is $\varphi(v \to v')$.

Quiver.Push.lift_obj theorem

: (lift σ φ τ h).obj = τ

Full source

theorem lift_obj : (lift σ φ τ h).obj = τ :=
  rfl

Object Map of Lifted Prefunctor Equals $\tau$

Informal description

Given a map $\sigma : V \to W$, a prefunctor $\varphi : V \to W'$, and a function $\tau : W \to W'$ such that $\tau \circ \sigma = \varphi$ on objects, the object map of the lifted prefunctor $\text{lift}\ \sigma\ \varphi\ \tau\ h$ is equal to $\tau$.

Quiver.Push.lift_comp theorem

: (of σ ⋙q lift σ φ τ h) = φ

Full source

theorem lift_comp : (ofof σ ⋙q lift σ φ τ h) = φ := by
  fapply Prefunctor.ext
  · rintro X
    simp only [Prefunctor.comp_obj]
    apply Eq.symm
    exact h X
  · rintro X Y f
    simp only [Prefunctor.comp_map]
    apply eq_of_heq
    iterate 2 apply (cast_heq _ _).trans
    apply HEq.symm
    apply (eqRec_heq _ _).trans
    have : ∀ {α γ} {β : α → γ → Sort _} {a a'} (p : a = a') g (b : β a g), HEq (p ▸ b) b := by
      intros
      subst_vars
      rfl
    apply this

Composition of Pushforward and Lift Equals Original Prefunctor

Informal description

Given a map $\sigma : V \to W$, a prefunctor $\varphi : V \to W'$, and a function $\tau : W \to W'$ such that $\tau \circ \sigma = \varphi$ on objects, the composition of the prefunctor $\text{Quiver.Push.of}$ (induced by $\sigma$) with the lifted prefunctor $\text{Quiver.Push.lift}$ equals $\varphi$.

Quiver.Push.lift_unique theorem

(Φ : Push σ ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : (of σ ⋙q Φ) = φ) : Φ = lift σ φ τ h

Full source

theorem lift_unique (Φ : PushPush σ ⥤q W') (Φ₀ : Φ.obj = τ) (Φcomp : (ofof σ ⋙q Φ) = φ) :
    Φ = lift σ φ τ h := by
  dsimp only [of, lift]
  fapply Prefunctor.ext
  · intro X
    simp only
    rw [Φ₀]
  · rintro _ _ ⟨⟩
    subst_vars
    simp only [Prefunctor.comp_map, cast_eq]
    rfl

Uniqueness of Lift in Pushforward Quiver Structure

Informal description

Given a map $\sigma : V \to W$, a prefunctor $\varphi : V \to W'$, and a function $\tau : W \to W'$ such that $\tau \circ \sigma = \varphi$ on objects, any prefunctor $\Phi$ from the pushforward quiver structure on $W$ to $W'$ satisfying: 1. $\Phi$ acts on objects as $\tau$, and 2. the composition of $\text{Quiver.Push.of}$ with $\Phi$ equals $\varphi$, must be equal to the prefunctor $\text{Quiver.Push.lift}$ constructed from $\sigma$, $\varphi$, $\tau$, and the given condition.