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.
instance
Quiver.instNonemptyPush
{V : Type u_1}
{W : Type u_2}
(σ : V → W)
[h : Nonempty W]
:
Nonempty (Quiver.Push σ)
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
instance
Quiver.instQuiverPush
{V : Type u_1}
[Quiver V]
{W : Type u_2}
(σ : V → W)
:
Quiver (Quiver.Push σ)
The prefunctor induced by pushing arrows via σ
Instances For
@[simp]
theorem
Quiver.Push.of_obj
{V : Type u_1}
[Quiver V]
{W : Type u_2}
(σ : V → W)
:
(Quiver.Push.of σ).obj = σ
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 σ.
Instances For
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 = φ
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