doc-next-gen

Mathlib.Combinatorics.Quiver.Prefunctor

Module docstring

{"# Morphisms of quivers "}

Prefunctor structure
(V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W]
Full source 
/-- A morphism of quivers. As we will later have categorical functors extend this structure,
we call it a `Prefunctor`. -/
structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
  /-- The action of a (pre)functor on vertices/objects. -/
  obj : V → W
  /-- The action of a (pre)functor on edges/arrows/morphisms. -/
  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)
Prefunctor between quivers
Informal description
A prefunctor between two quivers \( V \) and \( W \) consists of: - A function \( \text{obj} : V \to W \) mapping objects of \( V \) to objects of \( W \). - For every pair of objects \( X, Y \) in \( V \), a function \( \text{map} : (X \longrightarrow Y) \to (\text{obj}(X) \longrightarrow \text{obj}(Y)) \) mapping arrows in \( V \) to arrows in \( W \). This structure is called a prefunctor because it will later be extended to define categorical functors.
Prefunctor.mk_obj theorem
{V W : Type*} [Quiver V] [Quiver W] {obj : V → W} {map} {X : V} : (Prefunctor.mk obj map).obj X = obj X
Full source 
lemma mk_obj {V W : Type*} [Quiver V] [Quiver W] {obj : V → W} {map} {X : V} :
    (Prefunctor.mk obj map).obj X = obj X := rfl
Object Component of Prefunctor Construction
Informal description
For any quivers $V$ and $W$, given a function $\text{obj} \colon V \to W$ and a family of functions $\text{map} \colon (X \longrightarrow Y) \to (\text{obj}(X) \longrightarrow \text{obj}(Y))$ for all $X, Y \in V$, the object component of the prefunctor $\text{Prefunctor.mk obj map}$ evaluated at any object $X \in V$ equals $\text{obj}(X)$. That is, $(\text{Prefunctor.mk obj map}).\text{obj}(X) = \text{obj}(X)$.
Prefunctor.mk_map theorem
{V W : Type*} [Quiver V] [Quiver W] {obj : V → W} {map} {X Y : V} {f : X ⟶ Y} : (Prefunctor.mk obj map).map f = map f
Full source 
lemma mk_map {V W : Type*} [Quiver V] [Quiver W] {obj : V → W} {map} {X Y : V} {f : X ⟶ Y} :
    (Prefunctor.mk obj map).map f = map f := rfl
Arrow Component of Prefunctor Construction
Informal description
For any quivers $V$ and $W$, given a function $\text{obj} \colon V \to W$ and a family of functions $\text{map} \colon (X \longrightarrow Y) \to (\text{obj}(X) \longrightarrow \text{obj}(Y))$ for all $X, Y \in V$, the arrow component of the prefunctor $\text{Prefunctor.mk obj map}$ evaluated at any arrow $f \colon X \to Y$ in $V$ equals $\text{map}(f)$. That is, $(\text{Prefunctor.mk obj map}).\text{map}(f) = \text{map}(f)$.
Prefunctor.ext theorem
{V : Type u} [Quiver.{v₁} V] {W : Type u₂} [Quiver.{v₂} W] {F G : Prefunctor V W} (h_obj : ∀ X, F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn (h_obj Y).symm (Eq.recOn (h_obj X).symm (G.map f))) : F = G
Full source 
@[ext (iff := false)]
theorem ext {V : Type u} [Quiver.{v₁} V] {W : Type u₂} [Quiver.{v₂} W] {F G : Prefunctor V W}
    (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ (X Y : V) (f : X ⟶ Y),
      F.map f = Eq.recOn (h_obj Y).symm (Eq.recOn (h_obj X).symm (G.map f))) : F = G := by
  obtain ⟨F_obj, _⟩ := F
  obtain ⟨G_obj, _⟩ := G
  obtain rfl : F_obj = G_obj := by
    ext X
    apply h_obj
  congr
  funext X Y f
  simpa using h_map X Y f
Extensionality Principle for Prefunctors
Informal description
Let $V$ and $W$ be quivers, and let $F, G \colon V \to W$ be prefunctors between them. If $F$ and $G$ agree on objects (i.e., $F(X) = G(X)$ for all objects $X$ in $V$) and for all objects $X, Y$ in $V$ and all arrows $f \colon X \to Y$, the map $F(f)$ is equal to $G(f)$ (after appropriately transporting along the equality of objects), then $F = G$.
Prefunctor.ext' theorem
{V W : Type u} [Quiver V] [Quiver W] {F G : Prefunctor V W} (h_obj : ∀ X, F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) (h_obj _).symm (h_obj _).symm) : F = G
Full source 
/-- This may be a more useful form of `Prefunctor.ext`. -/
theorem ext' {V W : Type u} [Quiver V] [Quiver W] {F G : Prefunctor V W}
    (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ (X Y : V) (f : X ⟶ Y),
      F.map f = Quiver.homOfEq (G.map f) (h_obj _).symm (h_obj _).symm) : F = G := by
  obtain ⟨Fobj, Fmap⟩ := F
  obtain ⟨Gobj, Gmap⟩ := G
  obtain rfl : Fobj = Gobj := funext h_obj
  simp only [mk.injEq, heq_eq_eq, true_and]
  ext X Y f
  simpa only [Quiver.homOfEq_rfl] using h_map X Y f
Extensionality Principle for Prefunctors (Alternative Form)
Informal description
Let $V$ and $W$ be quivers, and let $F, G \colon V \to W$ be prefunctors between them. If $F$ and $G$ agree on objects (i.e., $F(X) = G(X)$ for all objects $X$ in $V$) and for all objects $X, Y$ in $V$ and all arrows $f \colon X \to Y$, the map $F(f)$ is equal to $G(f)$ (after appropriately transporting along the equality of objects), then $F = G$.
Prefunctor.id definition
(V : Type*) [Quiver V] : Prefunctor V V
Full source 
/-- The identity morphism between quivers. -/
@[simps]
def id (V : Type*) [Quiver V] : Prefunctor V V where
  obj := fun X => X
  map f := f
Identity prefunctor
Informal description
The identity prefunctor on a quiver \( V \) is the prefunctor that maps each object \( X \) in \( V \) to itself and each arrow \( f : X \to Y \) in \( V \) to itself.
Prefunctor.instInhabited instance
(V : Type*) [Quiver V] : Inhabited (Prefunctor V V)
Full source 
instance (V : Type*) [Quiver V] : Inhabited (Prefunctor V V) :=
  ⟨id V⟩
Inhabited Type of Prefunctors on a Quiver
Informal description
For any quiver $V$, the type of prefunctors from $V$ to $V$ is inhabited by the identity prefunctor.
Prefunctor.comp definition
{U : Type*} [Quiver U] {V : Type*} [Quiver V] {W : Type*} [Quiver W] (F : Prefunctor U V) (G : Prefunctor V W) : Prefunctor U W
Full source 
/-- Composition of morphisms between quivers. -/
@[simps]
def comp {U : Type*} [Quiver U] {V : Type*} [Quiver V] {W : Type*} [Quiver W]
    (F : Prefunctor U V) (G : Prefunctor V W) : Prefunctor U W where
  obj X := G.obj (F.obj X)
  map f := G.map (F.map f)
Composition of prefunctors
Informal description
Given quivers \( U \), \( V \), and \( W \), the composition of prefunctors \( F : U \to V \) and \( G : V \to W \) is the prefunctor \( G \circ F : U \to W \) defined by: - On objects: \( (G \circ F)(X) = G(F(X)) \) for any object \( X \) in \( U \). - On arrows: \( (G \circ F)(f) = G(F(f)) \) for any arrow \( f : X \to Y \) in \( U \).
Prefunctor.comp_id theorem
{U V : Type*} [Quiver U] [Quiver V] (F : Prefunctor U V) : F.comp (id _) = F
Full source 
@[simp]
theorem comp_id {U V : Type*} [Quiver U] [Quiver V] (F : Prefunctor U V) :
    F.comp (id _) = F := rfl
Right Identity Law for Prefunctor Composition
Informal description
For any quivers $U$ and $V$, and any prefunctor $F : U \to V$, the composition of $F$ with the identity prefunctor on $V$ equals $F$, i.e., $F \circ \text{id}_V = F$.
Prefunctor.id_comp theorem
{U V : Type*} [Quiver U] [Quiver V] (F : Prefunctor U V) : (id _).comp F = F
Full source 
@[simp]
theorem id_comp {U V : Type*} [Quiver U] [Quiver V] (F : Prefunctor U V) :
    (id _).comp F = F := rfl
Left Identity Law for Prefunctor Composition
Informal description
For any quivers $U$ and $V$, and any prefunctor $F : U \to V$, the composition of the identity prefunctor on $U$ with $F$ equals $F$, i.e., $\text{id}_U \circ F = F$.
Prefunctor.comp_assoc theorem
{U V W Z : Type*} [Quiver U] [Quiver V] [Quiver W] [Quiver Z] (F : Prefunctor U V) (G : Prefunctor V W) (H : Prefunctor W Z) : (F.comp G).comp H = F.comp (G.comp H)
Full source 
@[simp]
theorem comp_assoc {U V W Z : Type*} [Quiver U] [Quiver V] [Quiver W] [Quiver Z]
    (F : Prefunctor U V) (G : Prefunctor V W) (H : Prefunctor W Z) :
    (F.comp G).comp H = F.comp (G.comp H) :=
  rfl
Associativity of Prefunctor Composition
Informal description
For any quivers $U$, $V$, $W$, and $Z$, and any prefunctors $F : U \to V$, $G : V \to W$, and $H : W \to Z$, the composition of prefunctors is associative, i.e., $(F \circ G) \circ H = F \circ (G \circ H)$.
Prefunctor.term_⋙q_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Notation for composition of prefunctors. -/
infixl:60 " ⋙q " => Prefunctor.comp
Composition of prefunctors
Informal description
The notation `⋙q` represents the composition of prefunctors, where for two prefunctors $F$ and $G$, the composition $F \mathbin{⋙q} G$ is defined as the prefunctor obtained by composing the actions of $F$ and $G$ in sequence.
Prefunctor.congr_map theorem
{U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y} (h : f = g) : F.map f = F.map g
Full source 
theorem congr_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y}
    (h : f = g) : F.map f = F.map g := by
  rw [h]
Prefunctor Preserves Equality of Arrows
Informal description
For any two quivers $U$ and $V$, and any prefunctor $F \colon U \to V$, if two arrows $f, g \colon X \to Y$ in $U$ are equal (i.e., $f = g$), then their images under $F$ are also equal (i.e., $F(f) = F(g)$).
Prefunctor.congr_obj theorem
{U V : Type*} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) (X : U) : F.obj X = G.obj X
Full source 
/-- An equality of prefunctors gives an equality on objects. -/
theorem congr_obj {U V : Type*} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) (X : U) :
    F.obj X = G.obj X := by cases e; rfl
Equality of Prefunctors Implies Equality on Objects
Informal description
For any two quivers $U$ and $V$, and any two prefunctors $F, G \colon U \to V$, if $F = G$, then for every object $X$ in $U$, we have $F(X) = G(X)$.
Prefunctor.congr_hom theorem
{U V : Type*} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) {X Y : U} (f : X ⟶ Y) : Quiver.homOfEq (F.map f) (congr_obj e X) (congr_obj e Y) = G.map f
Full source 
/-- An equality of prefunctors gives an equality on homs. -/
theorem congr_hom {U V : Type*} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) {X Y : U}
    (f : X ⟶ Y) : Quiver.homOfEq (F.map f) (congr_obj e X) (congr_obj e Y) = G.map f := by
  subst e
  simp
Equality of Prefunctors Implies Equality on Arrows via homOfEq
Informal description
For any two quivers $U$ and $V$, and any two prefunctors $F, G \colon U \to V$, if $F = G$, then for every arrow $f \colon X \to Y$ in $U$, the equality \[ \text{homOfEq}(F(f), \text{congr\_obj}(e, X), \text{congr\_obj}(e, Y)) = G(f) \] holds, where $\text{homOfEq}$ constructs an equality of arrows given an equality of objects, and $\text{congr\_obj}(e, X)$ is the proof that $F(X) = G(X)$ obtained from $e \colon F = G$.
Prefunctor.homOfEq_map theorem
{U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y) {X' Y' : U} (hX : X = X') (hY : Y = Y') : F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) (congr_arg F.obj hX) (congr_arg F.obj hY)
Full source 
/-- Prefunctors commute with `homOfEq`. -/
@[simp]
theorem homOfEq_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y)
    {X' Y' : U} (hX : X = X') (hY : Y = Y') :
    F.map (Quiver.homOfEq f hX hY) =
      Quiver.homOfEq (F.map f) (congr_arg F.obj hX) (congr_arg F.obj hY) := by subst hX hY; simp
Prefunctor Commutes with `homOfEq`
Informal description
Let $F \colon U \to V$ be a prefunctor between quivers $U$ and $V$. For any morphism $f \colon X \to Y$ in $U$ and any equalities $h_X \colon X = X'$ and $h_Y \colon Y = Y'$, the prefunctor $F$ maps the morphism $\text{homOfEq}(f, h_X, h_Y)$ (which is the morphism $f$ adjusted by the equalities $h_X$ and $h_Y$) to the morphism $\text{homOfEq}(F(f), \text{congr\_arg}(F.obj, h_X), \text{congr\_arg}(F.obj, h_Y))$ (which is the morphism $F(f)$ adjusted by the equalities of objects induced by $h_X$ and $h_Y$ via $F$). In other words, the following equality holds: \[ F(\text{homOfEq}(f, h_X, h_Y)) = \text{homOfEq}(F(f), F(X) = F(X'), F(Y) = F(Y')). \]