From 85e29307e7dd45b763f368e20254ae6d90b1a757 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 29 Sep 2024 20:16:33 +0000 Subject: [PATCH] feat(Combinatorics/Quiver/ReflQuiver): reflexive quivers (#16780) Reflexive quivers are an intermediate structure between categories and quivers, containing only an identity element. This PR constructs `ReflQuiver` as a class and `ReflQuiv` which is the category of reflexive quivers and reflexive prefunctors. Co-Authored-By: Emily Riehl and Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Co-authored-by: Mario Carneiro Co-authored-by: Emily Riehl Co-authored-by: Mario Carneiro --- Mathlib.lean | 2 + Mathlib/CategoryTheory/Category/Cat.lean | 8 + Mathlib/CategoryTheory/Category/Quiv.lean | 22 +- Mathlib/CategoryTheory/Category/ReflQuiv.lean | 251 ++++++++++++++++++ Mathlib/Combinatorics/Quiver/ReflQuiver.lean | 131 +++++++++ 5 files changed, 405 insertions(+), 9 deletions(-) create mode 100644 Mathlib/CategoryTheory/Category/ReflQuiv.lean create mode 100644 Mathlib/Combinatorics/Quiver/ReflQuiver.lean diff --git a/Mathlib.lean b/Mathlib.lean index 277d2dffaca09..9f3160338f29b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1445,6 +1445,7 @@ import Mathlib.CategoryTheory.Category.PartialFun import Mathlib.CategoryTheory.Category.Pointed import Mathlib.CategoryTheory.Category.Preorder import Mathlib.CategoryTheory.Category.Quiv +import Mathlib.CategoryTheory.Category.ReflQuiv import Mathlib.CategoryTheory.Category.RelCat import Mathlib.CategoryTheory.Category.TwoP import Mathlib.CategoryTheory.Category.ULift @@ -1960,6 +1961,7 @@ import Mathlib.Combinatorics.Quiver.ConnectedComponent import Mathlib.Combinatorics.Quiver.Covering import Mathlib.Combinatorics.Quiver.Path import Mathlib.Combinatorics.Quiver.Push +import Mathlib.Combinatorics.Quiver.ReflQuiver import Mathlib.Combinatorics.Quiver.SingleObj import Mathlib.Combinatorics.Quiver.Subquiver import Mathlib.Combinatorics.Quiver.Symmetric diff --git a/Mathlib/CategoryTheory/Category/Cat.lean b/Mathlib/CategoryTheory/Category/Cat.lean index 3d4788b016f0d..9838804baf16f 100644 --- a/Mathlib/CategoryTheory/Category/Cat.lean +++ b/Mathlib/CategoryTheory/Category/Cat.lean @@ -133,6 +133,14 @@ lemma associator_inv_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ (α_ F G H).inv.app X = eqToHom (by simp) := rfl +/-- The identity in the category of categories equals the identity functor.-/ +theorem id_eq_id (X : Cat) : 𝟙 X = 𝟭 X := rfl + +/-- Composition in the category of categories equals functor composition.-/ +theorem comp_eq_comp {X Y Z : Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙ G := rfl + +@[simp] theorem of_α (C) [Category C] : (of C).α = C := rfl + /-- Functor that gets the set of objects of a category. It is not called `forget`, because it is not a faithful functor. -/ def objects : Cat.{v, u} ⥤ Type u where diff --git a/Mathlib/CategoryTheory/Category/Quiv.lean b/Mathlib/CategoryTheory/Category/Quiv.lean index bdb427995bad6..be83ad9b038c2 100644 --- a/Mathlib/CategoryTheory/Category/Quiv.lean +++ b/Mathlib/CategoryTheory/Category/Quiv.lean @@ -11,10 +11,8 @@ import Mathlib.CategoryTheory.PathCategory # The category of quivers The category of (bundled) quivers, and the free/forgetful adjunction between `Cat` and `Quiv`. - -/ - universe v u namespace CategoryTheory @@ -51,6 +49,12 @@ def forget : Cat.{v, u} ⥤ Quiv.{v, u} where obj C := Quiv.of C map F := F.toPrefunctor +/-- The identity in the category of quivers equals the identity prefunctor.-/ +theorem id_eq_id (X : Quiv) : 𝟙 X = 𝟭q X := rfl + +/-- Composition in the category of quivers equals prefunctor composition.-/ +theorem comp_eq_comp {X Y Z : Quiv} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙q G := rfl + end Quiv namespace Cat @@ -65,14 +69,14 @@ def free : Quiv.{v, u} ⥤ Cat.{max u v, u} where map_comp := fun f g => F.mapPath_comp f g } map_id V := by change (show Paths V ⥤ _ from _) = _ - ext; swap - · apply eq_conj_eqToHom + ext · rfl + · exact eq_conj_eqToHom _ map_comp {U _ _} F G := by change (show Paths U ⥤ _ from _) = _ - ext; swap - · apply eq_conj_eqToHom + ext · rfl + · exact eq_conj_eqToHom _ end Cat @@ -105,9 +109,9 @@ def adj : Cat.free ⊣ Quiv.forget := exact Category.id_comp _ } homEquiv_naturality_left_symm := fun {V _ _} f g => by change (show Paths V ⥤ _ from _) = _ - ext; swap - · apply eq_conj_eqToHom - · rfl } + ext + · rfl + · apply eq_conj_eqToHom } end Quiv diff --git a/Mathlib/CategoryTheory/Category/ReflQuiv.lean b/Mathlib/CategoryTheory/Category/ReflQuiv.lean new file mode 100644 index 0000000000000..f26afec53930b --- /dev/null +++ b/Mathlib/CategoryTheory/Category/ReflQuiv.lean @@ -0,0 +1,251 @@ +/- +Copyright (c) 2024 Mario Carneiro and Emily Riehl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, Emily Riehl +-/ +import Mathlib.Combinatorics.Quiver.ReflQuiver +import Mathlib.CategoryTheory.Category.Cat +import Mathlib.CategoryTheory.Category.Quiv + +/-! +# The category of refl quivers + +The category `ReflQuiv` of (bundled) reflexive quivers, and the free/forgetful adjunction between +`Cat` and `ReflQuiv`. +-/ + +namespace CategoryTheory +universe v u + +/-- Category of refl quivers. -/ +@[nolint checkUnivs] +def ReflQuiv := + Bundled ReflQuiver.{v + 1, u} + +namespace ReflQuiv + +instance : CoeSort ReflQuiv (Type u) where coe := Bundled.α + +instance (C : ReflQuiv.{v, u}) : ReflQuiver.{v + 1, u} C := C.str + +/-- The underlying quiver of a reflexive quiver.-/ +def toQuiv (C : ReflQuiv.{v, u}) : Quiv.{v, u} := Quiv.of C.α + +/-- Construct a bundled `ReflQuiv` from the underlying type and the typeclass. -/ +def of (C : Type u) [ReflQuiver.{v + 1} C] : ReflQuiv.{v, u} := Bundled.of C + +instance : Inhabited ReflQuiv := ⟨ReflQuiv.of (Discrete default)⟩ + +@[simp] theorem of_val (C : Type u) [ReflQuiver C] : (ReflQuiv.of C) = C := rfl + +/-- Category structure on `ReflQuiv` -/ +instance category : LargeCategory.{max v u} ReflQuiv.{v, u} where + Hom C D := ReflPrefunctor C D + id C := ReflPrefunctor.id C + comp F G := ReflPrefunctor.comp F G + +theorem id_eq_id (X : ReflQuiv) : 𝟙 X = 𝟭rq X := rfl +theorem comp_eq_comp {X Y Z : ReflQuiv} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙rq G := rfl + +/-- The forgetful functor from categories to quivers. -/ +@[simps] +def forget : Cat.{v, u} ⥤ ReflQuiv.{v, u} where + obj C := ReflQuiv.of C + map F := F.toReflPrefunctor + +theorem forget_faithful {C D : Cat.{v, u}} (F G : C ⥤ D) + (hyp : forget.map F = forget.map G) : F = G := by + cases F; cases G; cases hyp; rfl + +theorem forget.Faithful : Functor.Faithful (forget) where + map_injective := fun hyp ↦ forget_faithful _ _ hyp + +/-- The forgetful functor from categories to quivers. -/ +@[simps] +def forgetToQuiv : ReflQuiv.{v, u} ⥤ Quiv.{v, u} where + obj V := Quiv.of V + map F := F.toPrefunctor + +theorem forgetToQuiv_faithful {V W : ReflQuiv} (F G : V ⥤rq W) + (hyp : forgetToQuiv.map F = forgetToQuiv.map G) : F = G := by + cases F; cases G; cases hyp; rfl + +theorem forgetToQuiv.Faithful : Functor.Faithful (forgetToQuiv) where + map_injective := fun hyp ↦ forgetToQuiv_faithful _ _ hyp + +theorem forget_forgetToQuiv : forget ⋙ forgetToQuiv = Quiv.forget := rfl + +end ReflQuiv + +namespace ReflPrefunctor + +/-- A refl prefunctor can be promoted to a functor if it respects composition.-/ +def toFunctor {C D : Cat} (F : (ReflQuiv.of C) ⟶ (ReflQuiv.of D)) + (hyp : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), + F.map (CategoryStruct.comp (obj := C) f g) = + CategoryStruct.comp (obj := D) (F.map f) (F.map g)) : C ⥤ D where + obj := F.obj + map := F.map + map_id := F.map_id + map_comp := hyp + +end ReflPrefunctor + +namespace Cat + +/-- The hom relation that identifies the specified reflexivity arrows with the nil paths.-/ +inductive FreeReflRel {V} [ReflQuiver V] : (X Y : Paths V) → (f g : X ⟶ Y) → Prop + | mk {X : V} : FreeReflRel X X (Quiver.Hom.toPath (𝟙rq X)) .nil + +/-- A reflexive quiver generates a free category, defined as as quotient of the free category +on its underlying quiver (called the "path category") by the hom relation that uses the specified +reflexivity arrows as the identity arrows. -/ +def FreeRefl (V) [ReflQuiver V] := + Quotient (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V)) + +instance (V) [ReflQuiver V] : Category (FreeRefl V) := + inferInstanceAs (Category (Quotient _)) + +/-- The quotient functor associated to a quotient category defines a natural map from the free +category on the underlying quiver of a refl quiver to the free category on the reflexive quiver.-/ +def FreeRefl.quotientFunctor (V) [ReflQuiver V] : Cat.free.obj (Quiv.of V) ⥤ FreeRefl V := + Quotient.functor (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V)) + +/-- This is a specialization of `Quotient.lift_unique'` rather than `Quotient.lift_unique`, hence +the prime in the name.-/ +theorem FreeRefl.lift_unique' {V} [ReflQuiver V] {D} [Category D] (F₁ F₂ : FreeRefl V ⥤ D) + (h : quotientFunctor V ⋙ F₁ = quotientFunctor V ⋙ F₂) : + F₁ = F₂ := + Quotient.lift_unique' (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V)) _ _ h + +/-- The functor sending a reflexive quiver to the free category it generates, a quotient of +its path category.-/ +@[simps!] +def freeRefl : ReflQuiv.{v, u} ⥤ Cat.{max u v, u} where + obj V := Cat.of (FreeRefl V) + map f := Quotient.lift _ ((by exact Cat.free.map f.toPrefunctor) ⋙ FreeRefl.quotientFunctor _) + (fun X Y f g hfg => by + apply Quotient.sound + cases hfg + simp [ReflPrefunctor.map_id] + constructor) + map_id X := by + dsimp + refine (Quotient.lift_unique _ _ _ _ ((Functor.comp_id _).trans <| + (Functor.id_comp _).symm.trans ?_)).symm + congr 1 + exact (free.map_id X.toQuiv).symm + map_comp {X Y Z} f g := by + dsimp + apply (Quotient.lift_unique _ _ _ _ _).symm + have : free.map (f ≫ g).toPrefunctor = + free.map (X := X.toQuiv) (Y := Y.toQuiv) f.toPrefunctor ⋙ + free.map (X := Y.toQuiv) (Y := Z.toQuiv) g.toPrefunctor := by + show _ = _ ≫ _ + rw [← Functor.map_comp]; rfl + rw [this, Functor.assoc] + show _ ⋙ _ ⋙ _ = _ + rw [← Functor.assoc, Quotient.lift_spec, Functor.assoc, FreeRefl.quotientFunctor, + Quotient.lift_spec] + +theorem freeRefl_naturality {X Y} [ReflQuiver X] [ReflQuiver Y] (f : X ⥤rq Y) : + free.map (X := Quiv.of X) (Y := Quiv.of Y) f.toPrefunctor ⋙ + FreeRefl.quotientFunctor ↑Y = + FreeRefl.quotientFunctor ↑X ⋙ freeRefl.map (X := ReflQuiv.of X) (Y := ReflQuiv.of Y) f := by + simp only [free_obj, FreeRefl.quotientFunctor, freeRefl, ReflQuiv.of_val] + rw [Quotient.lift_spec] + +/-- We will make use of the natural quotient map from the free category on the underlying +quiver of a refl quiver to the free category on the reflexive quiver.-/ +def freeReflNatTrans : ReflQuiv.forgetToQuiv ⋙ Cat.free ⟶ freeRefl where + app V := FreeRefl.quotientFunctor V + naturality _ _ f := freeRefl_naturality f + +end Cat + +namespace ReflQuiv +open Category Functor + +/-- The unit components are defined as the composite of the corresponding unit component for the +adjunction between categories and quivers with the map underlying the quotient functor.-/ +@[simps! toPrefunctor obj map] +def adj.unit.app (V : ReflQuiv.{max u v, u}) : V ⥤rq forget.obj (Cat.freeRefl.obj V) where + toPrefunctor := Quiv.adj.unit.app (V.toQuiv) ⋙q + Quiv.forget.map (Cat.FreeRefl.quotientFunctor V) + map_id := fun _ => Quotient.sound _ ⟨⟩ + +/-- This is used in the proof of both triangle equalities.-/ +theorem adj.unit.component_eq (V : ReflQuiv.{max u v, u}) : + forgetToQuiv.map (adj.unit.app V) = Quiv.adj.unit.app (V.toQuiv) ≫ + Quiv.forget.map (Y := Cat.of _) (Cat.FreeRefl.quotientFunctor V) := rfl + +/-- The counit components are defined using the universal property of the quotient +from the corresponding counit component for the adjunction between categories and quivers.-/ +@[simps!] +def adj.counit.app (C : Cat) : Cat.freeRefl.obj (forget.obj C) ⥤ C := by + fapply Quotient.lift + · exact Quiv.adj.counit.app C + · intro x y f g rel + cases rel + unfold Quiv.adj + simp only [Adjunction.mkOfHomEquiv_counit_app, Equiv.coe_fn_symm_mk, + Quiv.lift_map, Prefunctor.mapPath_toPath, composePath_toPath] + rfl + +/-- The counit of `ReflQuiv.adj` is closely related to the counit of `Quiv.adj`.-/ +@[simp] +theorem adj.counit.component_eq (C : Cat) : + Cat.FreeRefl.quotientFunctor C ⋙ adj.counit.app C = + Quiv.adj.counit.app C := rfl + +/-- The counit of `ReflQuiv.adj` is closely related to the counit of `Quiv.adj`. For ease of use, +we introduce primed version for unbundled categories.-/ +@[simp] +theorem adj.counit.component_eq' (C) [Category C] : + Cat.FreeRefl.quotientFunctor C ⋙ adj.counit.app (Cat.of C) = + Quiv.adj.counit.app (Cat.of C) := rfl + +/-- +The adjunction between forming the free category on a reflexive quiver, and forgetting a category +to a reflexive quiver. +-/ +nonrec def adj : Cat.freeRefl.{max u v, u} ⊣ ReflQuiv.forget := + Adjunction.mkOfUnitCounit { + unit := { + app := adj.unit.app + naturality := fun V W f ↦ by exact rfl + } + counit := { + app := adj.counit.app + naturality := fun C D F ↦ Quotient.lift_unique' _ _ _ (Quiv.adj.counit.naturality F) + } + left_triangle := by + ext V + apply Cat.FreeRefl.lift_unique' + simp only [id_obj, Cat.free_obj, comp_obj, Cat.freeRefl_obj_α, NatTrans.comp_app, + forget_obj, whiskerRight_app, associator_hom_app, whiskerLeft_app, id_comp, + NatTrans.id_app'] + rw [Cat.id_eq_id, Cat.comp_eq_comp] + simp only [Cat.freeRefl_obj_α, Functor.comp_id] + rw [← Functor.assoc, ← Cat.freeRefl_naturality, Functor.assoc] + dsimp [Cat.freeRefl] + rw [adj.counit.component_eq' (Cat.FreeRefl V)] + conv => + enter [1, 1, 2] + apply (Quiv.comp_eq_comp (X := Quiv.of _) (Y := Quiv.of _) (Z := Quiv.of _) ..).symm + rw [Cat.free.map_comp] + show (_ ⋙ ((Quiv.forget ⋙ Cat.free).map (X := Cat.of _) (Y := Cat.of _) + (Cat.FreeRefl.quotientFunctor V))) ⋙ _ = _ + rw [Functor.assoc, ← Cat.comp_eq_comp] + conv => enter [1, 2]; apply Quiv.adj.counit.naturality + rw [Cat.comp_eq_comp, ← Functor.assoc, ← Cat.comp_eq_comp] + conv => enter [1, 1]; apply Quiv.adj.left_triangle_components V.toQuiv + exact Functor.id_comp _ + right_triangle := by + ext C + exact forgetToQuiv_faithful _ _ (Quiv.adj.right_triangle_components C) + } + +end ReflQuiv + +end CategoryTheory diff --git a/Mathlib/Combinatorics/Quiver/ReflQuiver.lean b/Mathlib/Combinatorics/Quiver/ReflQuiver.lean new file mode 100644 index 0000000000000..b0f9c85ac7250 --- /dev/null +++ b/Mathlib/Combinatorics/Quiver/ReflQuiver.lean @@ -0,0 +1,131 @@ +/- +Copyright (c) 2024 Mario Carneiro and Emily Riehl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, Emily Riehl +-/ +import Mathlib.Data.Set.Function +import Mathlib.CategoryTheory.Category.Cat + +/-! +# Reflexive Quivers + +This module defines reflexive quivers. A reflexive quiver, or "refl quiver" for short, extends +a quiver with a specified endoarrow on each term in its type of objects. + +We also introduce morphisms between reflexive quivers, called reflexive prefunctors or "refl +prefunctors" for short. + +Note: Currently Category does not extend ReflQuiver, although it could. (TODO: do this) +-/ +namespace CategoryTheory +universe v v₁ v₂ u u₁ u₂ + +/-- A reflexive quiver extends a quiver with a specified arrow `id X : X ⟶ X` for each `X` in its +type of objects. We denote these arrows by `id` since categories can be understood as an extension +of refl quivers. +-/ +class ReflQuiver (obj : Type u) extends Quiver.{v} obj : Type max u v where + /-- The identity morphism on an object. -/ + id : ∀ X : obj, Hom X X + +/-- Notation for the identity morphism in a category. -/ +scoped notation "𝟙rq" => ReflQuiver.id -- type as \b1 + +instance catToReflQuiver {C : Type u} [inst : Category.{v} C] : ReflQuiver.{v+1, u} C := + { inst with } + +@[simp] theorem ReflQuiver.id_eq_id {C : Type*} [Category C] (X : C) : 𝟙rq X = 𝟙 X := rfl + +/-- A morphism of reflexive quivers called a `ReflPrefunctor`. -/ +structure ReflPrefunctor (V : Type u₁) [ReflQuiver.{v₁} V] (W : Type u₂) [ReflQuiver.{v₂} W] + extends Prefunctor V W where + /-- A functor preserves identity morphisms. -/ + map_id : ∀ X : V, map (𝟙rq X) = 𝟙rq (obj X) := by aesop_cat + +namespace ReflPrefunctor + +-- These lemmas can not be `@[simp]` because after `whnfR` they have a variable on the LHS. +-- Nevertheless they are sometimes useful when building functors. +lemma mk_obj {V W : Type*} [ReflQuiver V] [ReflQuiver W] {obj : V → W} {map} {X : V} : + (Prefunctor.mk obj map).obj X = obj X := rfl + +lemma mk_map {V W : Type*} [ReflQuiver V] [ReflQuiver W] {obj : V → W} {map} {X Y : V} {f : X ⟶ Y} : + (Prefunctor.mk obj map).map f = map f := rfl + +/-- Proving equality between reflexive prefunctors. This isn't an extensionality lemma, + because usually you don't really want to do this. -/ +theorem ext {V : Type u} [ReflQuiver.{v₁} V] {W : Type u₂} [ReflQuiver.{v₂} W] + {F G : ReflPrefunctor 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 := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _ + congr + funext X Y f + simpa using h_map X Y f + +/-- The identity morphism between reflexive quivers. -/ +@[simps!] +def id (V : Type*) [ReflQuiver V] : ReflPrefunctor V V where + __ := Prefunctor.id _ + map_id _ := rfl + +instance (V : Type*) [ReflQuiver V] : Inhabited (ReflPrefunctor V V) := + ⟨id V⟩ + +/-- Composition of morphisms between reflexive quivers. -/ +@[simps!] +def comp {U : Type*} [ReflQuiver U] {V : Type*} [ReflQuiver V] {W : Type*} [ReflQuiver W] + (F : ReflPrefunctor U V) (G : ReflPrefunctor V W) : ReflPrefunctor U W where + __ := F.toPrefunctor.comp G.toPrefunctor + map_id _ := by simp [F.map_id, G.map_id] + +@[simp] +theorem comp_id {U V : Type*} [ReflQuiver U] [ReflQuiver V] (F : ReflPrefunctor U V) : + F.comp (id _) = F := rfl + +@[simp] +theorem id_comp {U V : Type*} [ReflQuiver U] [ReflQuiver V] (F : ReflPrefunctor U V) : + (id _).comp F = F := rfl + +@[simp] +theorem comp_assoc {U V W Z : Type*} [ReflQuiver U] [ReflQuiver V] [ReflQuiver W] [ReflQuiver Z] + (F : ReflPrefunctor U V) (G : ReflPrefunctor V W) (H : ReflPrefunctor W Z) : + (F.comp G).comp H = F.comp (G.comp H) := rfl + +/-- Notation for a prefunctor between reflexive quivers. -/ +infixl:50 " ⥤rq " => ReflPrefunctor + +/-- Notation for composition of reflexive prefunctors. -/ +infixl:60 " ⋙rq " => ReflPrefunctor.comp + +/-- Notation for the identity prefunctor on a reflexive quiver. -/ +notation "𝟭rq" => id + +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 := congrArg F.map h + +end ReflPrefunctor + +/-- A functor has an underlying refl prefunctor.-/ +def Functor.toReflPrefunctor {C D} [Category C] [Category D] (F : C ⥤ D) : C ⥤rq D := { F with } + +@[simp] +theorem Functor.toReflPrefunctor_toPrefunctor {C D : Cat} (F : C ⥤ D) : + (Functor.toReflPrefunctor F).toPrefunctor = F.toPrefunctor := rfl + +namespace ReflQuiver +open Opposite + +/-- `Vᵒᵖ` reverses the direction of all arrows of `V`. -/ +instance opposite {V} [ReflQuiver V] : ReflQuiver Vᵒᵖ where + id X := op (𝟙rq X.unop) + +instance discreteReflQuiver (V : Type u) : ReflQuiver.{u+1} (Discrete V) := + { discreteCategory V with } + +end ReflQuiver + +end CategoryTheory