# Documentation

Mathlib.CategoryTheory.Over

# Over and under categories #

Over (and under) categories are special cases of comma categories.

• If L is the identity functor and R is a constant functor, then Comma L R is the "slice" or "over" category over the object R maps to.
• Conversely, if L is a constant functor and R is the identity functor, then Comma L R is the "coslice" or "under" category under the object L maps to.

## Tags #

Comma, Slice, Coslice, Over, Under

def CategoryTheory.Over {T : Type u₁} [] (X : T) :
Type (max u₁ v₁)

The over category has as objects arrows in T with codomain X and as morphisms commutative triangles.

Instances For
instance CategoryTheory.instCategoryOver {T : Type u₁} [] (X : T) :
theorem CategoryTheory.Over.OverMorphism.ext {T : Type u₁} [] {X : T} {U : } {V : } {f : U V} {g : U V} (h : f.left = g.left) :
f = g
theorem CategoryTheory.Over.over_right {T : Type u₁} [] {X : T} (U : ) :
U.right = { as := PUnit.unit }
@[simp]
theorem CategoryTheory.Over.id_left {T : Type u₁} [] {X : T} (U : ) :
@[simp]
theorem CategoryTheory.Over.comp_left {T : Type u₁} [] {X : T} (a : ) (b : ) (c : ) (f : a b) (g : b c) :
@[simp]
theorem CategoryTheory.Over.w_assoc {T : Type u₁} [] {X : T} {A : } {B : } (f : A B) {Z : T} (h : ().obj B.right Z) :
=
@[simp]
theorem CategoryTheory.Over.w {T : Type u₁} [] {X : T} {A : } {B : } (f : A B) :
@[simp]
theorem CategoryTheory.Over.mk_left {T : Type u₁} [] {X : T} {Y : T} (f : Y X) :
().left = Y
@[simp]
theorem CategoryTheory.Over.mk_hom {T : Type u₁} [] {X : T} {Y : T} (f : Y X) :
().hom = f
def CategoryTheory.Over.mk {T : Type u₁} [] {X : T} {Y : T} (f : Y X) :

To give an object in the over category, it suffices to give a morphism with codomain X.

Instances For
def CategoryTheory.Over.coeFromHom {T : Type u₁} [] {X : T} {Y : T} :
CoeOut (Y X) ()

We can set up a coercion from arrows with codomain X to over X. This most likely should not be a global instance, but it is sometimes useful.

Instances For
@[simp]
theorem CategoryTheory.Over.coe_hom {T : Type u₁} [] {X : T} {Y : T} (f : Y X) :
().hom = f
@[simp]
theorem CategoryTheory.Over.homMk_left {T : Type u₁} [] {X : T} {U : } {V : } (f : U.left V.left) (w : autoParam ( = U.hom) _auto✝) :
().left = f
@[simp]
theorem CategoryTheory.Over.homMk_right_down_down {T : Type u₁} [] {X : T} {U : } {V : } (f : U.left V.left) (w : autoParam ( = U.hom) _auto✝) :
(_ : V.right.as = V.right.as) = (_ : V.right.as = V.right.as)
def CategoryTheory.Over.homMk {T : Type u₁} [] {X : T} {U : } {V : } (f : U.left V.left) (w : autoParam ( = U.hom) _auto✝) :
U V

To give a morphism in the over category, it suffices to give an arrow fitting in a commutative triangle.

Instances For
@[simp]
theorem CategoryTheory.Over.isoMk_hom_right_down_down {T : Type u₁} [] {X : T} {f : } {g : } (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
(_ : g.right.as = g.right.as) = (_ : g.right.as = g.right.as)
@[simp]
theorem CategoryTheory.Over.isoMk_inv_right_down_down {T : Type u₁} [] {X : T} {f : } {g : } (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
(_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)
@[simp]
theorem CategoryTheory.Over.isoMk_inv_left {T : Type u₁} [] {X : T} {f : } {g : } (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
().inv.left = hl.inv
@[simp]
theorem CategoryTheory.Over.isoMk_hom_left {T : Type u₁} [] {X : T} {f : } {g : } (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
().hom.left = hl.hom
def CategoryTheory.Over.isoMk {T : Type u₁} [] {X : T} {f : } {g : } (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
f g

Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

Instances For
def CategoryTheory.Over.forget {T : Type u₁} [] (X : T) :

The forgetful functor mapping an arrow to its domain.

Instances For
@[simp]
theorem CategoryTheory.Over.forget_obj {T : Type u₁} [] {X : T} {U : } :
().obj U = U.left
@[simp]
theorem CategoryTheory.Over.forget_map {T : Type u₁} [] {X : T} {U : } {V : } {f : U V} :
().map f = f.left
@[simp]
theorem CategoryTheory.Over.forgetCocone_ι_app {T : Type u₁} [] (X : T) :
.app self = self.hom
@[simp]
theorem CategoryTheory.Over.forgetCocone_pt {T : Type u₁} [] (X : T) :
def CategoryTheory.Over.forgetCocone {T : Type u₁} [] (X : T) :

The natural cocone over the forgetful functor Over X ⥤ T with cocone point X.

Instances For
def CategoryTheory.Over.map {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :

A morphism f : X ⟶ Y induces a functor Over X ⥤ Over Y in the obvious way.

Instances For
@[simp]
theorem CategoryTheory.Over.map_obj_left {T : Type u₁} [] {X : T} {Y : T} {f : X Y} {U : } :
(().obj U).left = U.left
@[simp]
theorem CategoryTheory.Over.map_obj_hom {T : Type u₁} [] {X : T} {Y : T} {f : X Y} {U : } :
(().obj U).hom =
@[simp]
theorem CategoryTheory.Over.map_map_left {T : Type u₁} [] {X : T} {Y : T} {f : X Y} {U : } {V : } {g : U V} :
(().map g).left = g.left

Mapping by the identity morphism is just the identity functor.

Instances For
def CategoryTheory.Over.mapComp {T : Type u₁} [] {X : T} {Y : T} {Z : T} (f : X Y) (g : Y Z) :

Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

Instances For
instance CategoryTheory.Over.forget_reflects_iso {T : Type u₁} [] {X : T} :

The identity over X is terminal.

Instances For
instance CategoryTheory.Over.forget_faithful {T : Type u₁} [] {X : T} :
theorem CategoryTheory.Over.epi_of_epi_left {T : Type u₁} [] {X : T} {f : } {g : } (k : f g) [hk : CategoryTheory.Epi k.left] :

If k.left is an epimorphism, then k is an epimorphism. In other words, Over.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Over.epi_left_of_epi.

theorem CategoryTheory.Over.mono_of_mono_left {T : Type u₁} [] {X : T} {f : } {g : } (k : f g) [hk : CategoryTheory.Mono k.left] :

If k.left is a monomorphism, then k is a monomorphism. In other words, Over.forget X reflects monomorphisms. The converse of CategoryTheory.Over.mono_left_of_mono.

This lemma is not an instance, to avoid loops in type class inference.

instance CategoryTheory.Over.mono_left_of_mono {T : Type u₁} [] {X : T} {f : } {g : } (k : f g) :

If k is a monomorphism, then k.left is a monomorphism. In other words, Over.forget X preserves monomorphisms. The converse of CategoryTheory.Over.mono_of_mono_left.

@[simp]
theorem CategoryTheory.Over.iteratedSliceForward_obj {T : Type u₁} [] {X : T} (f : ) (α : ) :
@[simp]
theorem CategoryTheory.Over.iteratedSliceForward_map {T : Type u₁} [] {X : T} (f : ) :
∀ {X Y : } (κ : X Y), = CategoryTheory.Over.homMk κ.left.left
def CategoryTheory.Over.iteratedSliceForward {T : Type u₁} [] {X : T} (f : ) :

Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y

Instances For
@[simp]
theorem CategoryTheory.Over.iteratedSliceBackward_obj {T : Type u₁} [] {X : T} (f : ) (g : CategoryTheory.Over f.left) :
@[simp]
theorem CategoryTheory.Over.iteratedSliceBackward_map {T : Type u₁} [] {X : T} (f : ) :
∀ {X Y : CategoryTheory.Over f.left} (α : X Y),
def CategoryTheory.Over.iteratedSliceBackward {T : Type u₁} [] {X : T} (f : ) :

Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f

Instances For
@[simp]
theorem CategoryTheory.Over.iteratedSliceEquiv_functor {T : Type u₁} [] {X : T} (f : ) :
@[simp]
theorem CategoryTheory.Over.iteratedSliceEquiv_inverse {T : Type u₁} [] {X : T} (f : ) :
def CategoryTheory.Over.iteratedSliceEquiv {T : Type u₁} [] {X : T} (f : ) :

Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y

Instances For
theorem CategoryTheory.Over.iteratedSliceForward_forget {T : Type u₁} [] {X : T} (f : ) :
@[simp]
theorem CategoryTheory.Over.post_obj {T : Type u₁} [] {X : T} {D : Type u₂} [] (F : ) (Y : ) :
().obj Y = CategoryTheory.Over.mk (F.map Y.hom)
@[simp]
theorem CategoryTheory.Over.post_map {T : Type u₁} [] {X : T} {D : Type u₂} [] (F : ) :
∀ {X Y : } (f : X Y), ().map f = CategoryTheory.Over.homMk (F.map f.left)
def CategoryTheory.Over.post {T : Type u₁} [] {X : T} {D : Type u₂} [] (F : ) :

A functor F : T ⥤ D induces a functor Over X ⥤ Over (F.obj X) in the obvious way.

Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_obj_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
(().obj X).right = X.right
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_obj_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
(().obj X).hom = X.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_map_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
∀ {X Y : } (f : X Y), (().map f).right =
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_map_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
∀ {X Y : } (f : X Y), (().map f).left = F.map f.left
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_obj_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
(().obj X).left = F.obj X.left
def CategoryTheory.CostructuredArrow.toOver {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :

Reinterpreting an F-costructured arrow F.obj d ⟶ X as an arrow over X induces a functor CostructuredArrow F X ⥤ Over X.

Instances For
noncomputable def CategoryTheory.CostructuredArrow.isEquivalenceToOver {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :

An equivalence F induces an equivalence CostructuredArrow F X ≌ Over X.

Instances For
def CategoryTheory.Under {T : Type u₁} [] (X : T) :
Type (max u₁ v₁)

The under category has as objects arrows with domain X and as morphisms commutative triangles.

Instances For
instance CategoryTheory.instCategoryUnder {T : Type u₁} [] (X : T) :
theorem CategoryTheory.Under.UnderMorphism.ext {T : Type u₁} [] {X : T} {U : } {V : } {f : U V} {g : U V} (h : f.right = g.right) :
f = g
theorem CategoryTheory.Under.under_left {T : Type u₁} [] {X : T} (U : ) :
U.left = { as := PUnit.unit }
@[simp]
theorem CategoryTheory.Under.id_right {T : Type u₁} [] {X : T} (U : ) :
().right =
@[simp]
theorem CategoryTheory.Under.comp_right {T : Type u₁} [] {X : T} (a : ) (b : ) (c : ) (f : a b) (g : b c) :
().right = CategoryTheory.CategoryStruct.comp f.right g.right
@[simp]
theorem CategoryTheory.Under.w_assoc {T : Type u₁} [] {X : T} {A : } {B : } (f : A B) {Z : T} (h : B.right Z) :
@[simp]
theorem CategoryTheory.Under.w {T : Type u₁} [] {X : T} {A : } {B : } (f : A B) :
@[simp]
theorem CategoryTheory.Under.mk_right {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :
().right = Y
@[simp]
theorem CategoryTheory.Under.mk_hom {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :
().hom = f
def CategoryTheory.Under.mk {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :

To give an object in the under category, it suffices to give an arrow with domain X.

Instances For
@[simp]
theorem CategoryTheory.Under.homMk_right {T : Type u₁} [] {X : T} {U : } {V : } (f : U.right V.right) (w : autoParam ( = V.hom) _auto✝) :
().right = f
@[simp]
theorem CategoryTheory.Under.homMk_left_down_down {T : Type u₁} [] {X : T} {U : } {V : } (f : U.right V.right) (w : autoParam ( = V.hom) _auto✝) :
(_ : V.left.as = V.left.as) = (_ : V.left.as = V.left.as)
def CategoryTheory.Under.homMk {T : Type u₁} [] {X : T} {U : } {V : } (f : U.right V.right) (w : autoParam ( = V.hom) _auto✝) :
U V

To give a morphism in the under category, it suffices to give a morphism fitting in a commutative triangle.

Instances For
def CategoryTheory.Under.isoMk {T : Type u₁} [] {X : T} {f : } {g : } (hr : f.right g.right) (hw : autoParam (CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) _auto✝) :
f g

Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

Instances For
@[simp]
theorem CategoryTheory.Under.isoMk_hom_right {T : Type u₁} [] {X : T} {f : } {g : } (hr : f.right g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) :
().hom.right = hr.hom
@[simp]
theorem CategoryTheory.Under.isoMk_inv_right {T : Type u₁} [] {X : T} {f : } {g : } (hr : f.right g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) :
().inv.right = hr.inv
def CategoryTheory.Under.forget {T : Type u₁} [] (X : T) :

The forgetful functor mapping an arrow to its domain.

Instances For
@[simp]
theorem CategoryTheory.Under.forget_obj {T : Type u₁} [] {X : T} {U : } :
().obj U = U.right
@[simp]
theorem CategoryTheory.Under.forget_map {T : Type u₁} [] {X : T} {U : } {V : } {f : U V} :
().map f = f.right
@[simp]
theorem CategoryTheory.Under.forgetCone_pt {T : Type u₁} [] (X : T) :
= X
@[simp]
theorem CategoryTheory.Under.forgetCone_π_app {T : Type u₁} [] (X : T) :
.app self = self.hom
def CategoryTheory.Under.forgetCone {T : Type u₁} [] (X : T) :

The natural cone over the forgetful functor Under X ⥤ T with cone point X.

Instances For
def CategoryTheory.Under.map {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :

A morphism X ⟶ Y induces a functor Under Y ⥤ Under X in the obvious way.

Instances For
@[simp]
theorem CategoryTheory.Under.map_obj_right {T : Type u₁} [] {X : T} {Y : T} {f : X Y} {U : } :
(().obj U).right = U.right
@[simp]
theorem CategoryTheory.Under.map_obj_hom {T : Type u₁} [] {X : T} {Y : T} {f : X Y} {U : } :
(().obj U).hom =
@[simp]
theorem CategoryTheory.Under.map_map_right {T : Type u₁} [] {X : T} {Y : T} {f : X Y} {U : } {V : } {g : U V} :
(().map g).right = g.right

Mapping by the identity morphism is just the identity functor.

Instances For
def CategoryTheory.Under.mapComp {T : Type u₁} [] {X : T} {Y : T} {Z : T} (f : X Y) (g : Y Z) :

Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

Instances For
instance CategoryTheory.Under.forget_reflects_iso {T : Type u₁} [] {X : T} :

The identity under X is initial.

Instances For
instance CategoryTheory.Under.forget_faithful {T : Type u₁} [] {X : T} :
theorem CategoryTheory.Under.mono_of_mono_right {T : Type u₁} [] {X : T} {f : } {g : } (k : f g) [hk : CategoryTheory.Mono k.right] :

If k.right is a monomorphism, then k is a monomorphism. In other words, Under.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Under.mono_right_of_mono.

theorem CategoryTheory.Under.epi_of_epi_right {T : Type u₁} [] {X : T} {f : } {g : } (k : f g) [hk : CategoryTheory.Epi k.right] :

If k.right is an epimorphism, then k is an epimorphism. In other words, Under.forget X reflects epimorphisms. The converse of CategoryTheory.Under.epi_right_of_epi.

This lemma is not an instance, to avoid loops in type class inference.

instance CategoryTheory.Under.epi_right_of_epi {T : Type u₁} [] {X : T} {f : } {g : } (k : f g) :

If k is an epimorphism, then k.right is an epimorphism. In other words, Under.forget X preserves epimorphisms. The converse of CategoryTheory.under.epi_of_epi_right.

@[simp]
theorem CategoryTheory.Under.post_obj {T : Type u₁} [] {D : Type u₂} [] {X : T} (F : ) (Y : ) :
().obj Y = CategoryTheory.Under.mk (F.map Y.hom)
@[simp]
theorem CategoryTheory.Under.post_map {T : Type u₁} [] {D : Type u₂} [] {X : T} (F : ) :
∀ {X Y : } (f : X Y), ().map f = CategoryTheory.Under.homMk (F.map f.right)
def CategoryTheory.Under.post {T : Type u₁} [] {D : Type u₂} [] {X : T} (F : ) :

A functor F : T ⥤ D induces a functor Under X ⥤ Under (F.obj X) in the obvious way.

Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_map_left {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
∀ {X Y : } (f : X Y), (().map f).left =
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_obj_left {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
(().obj X).left = X.left
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_map_right {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
∀ {X Y : } (f : X Y), (().map f).right = F.map f.right
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_obj_right {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
(().obj X).right = F.obj X.right
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_obj_hom {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
(().obj X).hom = X.hom
def CategoryTheory.StructuredArrow.toUnder {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :

Reinterpreting an F-structured arrow X ⟶ F.obj d as an arrow under X induces a functor StructuredArrow X F ⥤ Under X.

Instances For
noncomputable def CategoryTheory.StructuredArrow.isEquivalenceToUnder {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :

An equivalence F induces an equivalence StructuredArrow X F ≌ Under X.

Instances For
@[simp]
theorem CategoryTheory.Functor.toOver_map_left {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :
∀ {X Y : S} (g : X Y), (().map g).left = F.map g
@[simp]
theorem CategoryTheory.Functor.toOver_obj_left {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) (Y : S) :
(().obj Y).left = F.obj Y
def CategoryTheory.Functor.toOver {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

Given X : T, to upgrade a functor F : S ⥤ T to a functor S ⥤ Over X, it suffices to provide maps F.obj Y ⟶ X for all Y making the obvious triangles involving all F.map g commute.

Instances For
def CategoryTheory.Functor.toOverCompForget {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

Upgrading a functor S ⥤ T to a functor S ⥤ Over X and composing with the forgetful functor Over X ⥤ T recovers the original functor.

Instances For
@[simp]
theorem CategoryTheory.Functor.toOver_comp_forget {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :
@[simp]
theorem CategoryTheory.Functor.toUnder_obj_right {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) (Y : S) :
(().obj Y).right = F.obj Y
@[simp]
theorem CategoryTheory.Functor.toUnder_map_right {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :
∀ {X Y : S} (g : X Y), (().map g).right = F.map g
def CategoryTheory.Functor.toUnder {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :

Given X : T, to upgrade a functor F : S ⥤ T to a functor S ⥤ Under X, it suffices to provide maps X ⟶ F.obj Y for all Y making the obvious triangles involving all F.map g commute.

Instances For
def CategoryTheory.Functor.toUnderCompForget {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :

Upgrading a functor S ⥤ T to a functor S ⥤ Under X and composing with the forgetful functor Under X ⥤ T recovers the original functor.

Instances For
@[simp]
theorem CategoryTheory.Functor.toUnder_comp_forget {T : Type u₁} [] {S : Type u₂} [] (F : ) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :