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