# 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.

Equations
Instances For
instance CategoryTheory.instCategoryOver {T : Type u₁} [] (X : T) :
Equations
• = CategoryTheory.commaCategory
Equations
theorem CategoryTheory.Over.OverMorphism.ext_iff {T : Type u₁} [] {X : T} {U : } {V : } {f : U V} {g : U V} :
f = g f.left = g.left
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_hom {T : Type u₁} [] {X : T} {Y : T} (f : Y X) :
.hom = f
@[simp]
theorem CategoryTheory.Over.mk_left {T : Type u₁} [] {X : T} {Y : T} (f : Y X) :
.left = Y
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.

Equations
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.

Equations
• CategoryTheory.Over.coeFromHom = { coe := CategoryTheory.Over.mk }
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✝) :
=
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.

Equations
Instances For
@[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
@[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✝) :
=
@[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_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✝) :
=
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.

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

The forgetful functor mapping an arrow to its domain.

Equations
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.

Equations
• = { pt := X, ι := { app := CategoryTheory.Comma.hom, naturality := } }
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.

Equations
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

This section proves various equalities between functors that demonstrate, for instance, that over categories assemble into a functor mapFunctor : T ⥤ Cat.

These equalities between functors are then converted to natural isomorphisms using eqToIso. Such natural isomorphisms could be obtained directly using Iso.refl but this method will have better computational properties, when used, for instance, in developing the theory of Beck-Chevalley transformations.

theorem CategoryTheory.Over.mapId_eq {T : Type u₁} [] (Y : T) :

Mapping by the identity morphism is just the identity functor.

The natural isomorphism arising from mapForget_eq.

Equations
Instances For
theorem CategoryTheory.Over.mapForget_eq {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :

Mapping by f and then forgetting is the same as forgetting.

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

The natural isomorphism arising from mapForget_eq.

Equations
Instances For
@[simp]
theorem CategoryTheory.Over.eqToHom_left {T : Type u₁} [] {X : T} {U : } {V : } (e : U = V) :
theorem CategoryTheory.Over.mapComp_eq {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.

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

The natural isomorphism arising from mapComp_eq.

Equations
Instances For
@[simp]
theorem CategoryTheory.Over.mapFunctor_obj (T : Type u₁) [] (X : T) :
@[simp]
theorem CategoryTheory.Over.mapFunctor_map (T : Type u₁) [] :
∀ {X Y : T} (f : X Y),

The functor defined by the over categories.

Equations
• = { obj := fun (X : T) => , map := fun {X Y : T} => CategoryTheory.Over.map, map_id := , map_comp := }
Instances For
instance CategoryTheory.Over.forget_reflects_iso {T : Type u₁} [] {X : T} :
.ReflectsIsomorphisms
Equations
• =
noncomputable def CategoryTheory.Over.mkIdTerminal {T : Type u₁} [] {X : T} :

The identity over X is terminal.

Equations
• CategoryTheory.Over.mkIdTerminal = CategoryTheory.CostructuredArrow.mkIdTerminal
Instances For
instance CategoryTheory.Over.forget_faithful {T : Type u₁} [] {X : T} :
.Faithful
Equations
• =
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.

Equations
• =
@[simp]
theorem CategoryTheory.Over.iteratedSliceForward_map {T : Type u₁} [] {X : T} (f : ) :
∀ {X_1 Y : } (κ : X_1 Y), f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk κ.left.left
@[simp]
theorem CategoryTheory.Over.iteratedSliceForward_obj {T : Type u₁} [] {X : T} (f : ) (α : ) :
f.iteratedSliceForward.obj α = CategoryTheory.Over.mk α.hom.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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Over.iteratedSliceBackward_map {T : Type u₁} [] {X : T} (f : ) :
∀ {X_1 Y : CategoryTheory.Over f.left} (α : X_1 Y), f.iteratedSliceBackward.map α =
@[simp]
theorem CategoryTheory.Over.iteratedSliceBackward_obj {T : Type u₁} [] {X : T} (f : ) (g : CategoryTheory.Over f.left) :
f.iteratedSliceBackward.obj g =
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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Over.iteratedSliceEquiv_unitIso {T : Type u₁} [] {X : T} (f : ) :
f.iteratedSliceEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (g : ) => CategoryTheory.Over.isoMk (CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (.obj g).left.left) ) )
@[simp]
theorem CategoryTheory.Over.iteratedSliceEquiv_functor {T : Type u₁} [] {X : T} (f : ) :
f.iteratedSliceEquiv.functor = f.iteratedSliceForward
@[simp]
theorem CategoryTheory.Over.iteratedSliceEquiv_counitIso {T : Type u₁} [] {X : T} (f : ) :
f.iteratedSliceEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (g : CategoryTheory.Over f.left) => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((f.iteratedSliceBackward.comp f.iteratedSliceForward).obj g).left) )
@[simp]
theorem CategoryTheory.Over.iteratedSliceEquiv_inverse {T : Type u₁} [] {X : T} (f : ) :
f.iteratedSliceEquiv.inverse = f.iteratedSliceBackward
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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Over.iteratedSliceForward_forget {T : Type u₁} [] {X : T} (f : ) :
f.iteratedSliceForward.comp (CategoryTheory.Over.forget f.left) = .comp
theorem CategoryTheory.Over.iteratedSliceBackward_forget_forget {T : Type u₁} [] {X : T} (f : ) :
f.iteratedSliceBackward.comp (.comp ) =
@[simp]
theorem CategoryTheory.Over.post_map {T : Type u₁} [] {D : Type u₂} [] {X : T} (F : ) :
∀ {X_1 Y : } (f : X_1 Y), .map f = CategoryTheory.Over.homMk (F.map f.left)
@[simp]
theorem CategoryTheory.Over.post_obj {T : Type u₁} [] {D : Type u₂} [] {X : T} (F : ) (Y : ) :
.obj Y = CategoryTheory.Over.mk (F.map Y.hom)
def CategoryTheory.Over.post {T : Type u₁} [] {D : Type u₂} [] {X : T} (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_obj_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) (X : ) :
(.obj X).left = F.obj X.left
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_map_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
∀ {X_1 Y : } (f : X_1 Y), (.map f).right = CategoryTheory.CategoryStruct.id X_1.right
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_obj_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) (X : ) :
(.obj X).hom = X.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_map_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) :
∀ {X_1 Y : } (f : X_1 Y), (.map f).left = F.map f.left
@[simp]
theorem CategoryTheory.CostructuredArrow.toOver_obj_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) (X : ) :
(.obj X).right = X.right
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.

Equations
Instances For
instance CategoryTheory.CostructuredArrow.instFaithfulOverToOver {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) [F.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.CostructuredArrow.instFullOverToOver {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) [F.Full] :
.Full
Equations
• =
instance CategoryTheory.CostructuredArrow.instEssSurjOverToOver {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) [F.EssSurj] :
.EssSurj
Equations
• =
instance CategoryTheory.CostructuredArrow.isEquivalence_toOver {T : Type u₁} [] {D : Type u₂} [] (F : ) (X : T) [F.IsEquivalence] :
.IsEquivalence

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

Equations
• =
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.

Equations
Instances For
instance CategoryTheory.instCategoryUnder {T : Type u₁} [] (X : T) :
Equations
• = CategoryTheory.commaCategory
Equations
• One or more equations did not get rendered due to their size.
theorem CategoryTheory.Under.UnderMorphism.ext_iff {T : Type u₁} [] {X : T} {U : } {V : } {f : U V} {g : U V} :
f = g f.right = g.right
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_hom {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :
.hom = f
@[simp]
theorem CategoryTheory.Under.mk_right {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :
.right = Y
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.

Equations
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✝) :
=
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.

Equations
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.

Equations
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.

Equations
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.

Equations
• = { pt := X, π := { app := CategoryTheory.Comma.hom, naturality := } }
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.

Equations
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

This section proves various equalities between functors that demonstrate, for instance, that under categories assemble into a functor mapFunctor : Tᵒᵖ ⥤ Cat.

theorem CategoryTheory.Under.mapId_eq {T : Type u₁} [] (Y : T) :

Mapping by the identity morphism is just the identity functor.

Mapping by the identity morphism is just the identity functor.

Equations
Instances For
theorem CategoryTheory.Under.mapForget_eq {T : Type u₁} [] {X : T} {Y : T} (f : X Y) :

Mapping by f and then forgetting is the same as forgetting.

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

The natural isomorphism arising from mapForget_eq.

Equations
Instances For
@[simp]
theorem CategoryTheory.Under.eqToHom_right {T : Type u₁} [] {X : T} {U : } {V : } (e : U = V) :
.right =
theorem CategoryTheory.Under.mapComp_eq {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.

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

The natural isomorphism arising from mapComp_eq.

Equations
Instances For
@[simp]
theorem CategoryTheory.Under.mapFunctor_obj (T : Type u₁) [] (X : Tᵒᵖ) :
@[simp]
theorem CategoryTheory.Under.mapFunctor_map (T : Type u₁) [] :
∀ {X Y : Tᵒᵖ} (f : X Y), .map f = CategoryTheory.Under.map f.unop

The functor defined by the under categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Under.forget_reflects_iso {T : Type u₁} [] {X : T} :
.ReflectsIsomorphisms
Equations
• =
noncomputable def CategoryTheory.Under.mkIdInitial {T : Type u₁} [] {X : T} :

The identity under X is initial.

Equations
• CategoryTheory.Under.mkIdInitial = CategoryTheory.StructuredArrow.mkIdInitial
Instances For
instance CategoryTheory.Under.forget_faithful {T : Type u₁} [] {X : T} :
.Faithful
Equations
• =
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.

Equations
• =
@[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_1 Y : } (f : X_1 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_obj_hom {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) (X : ) :
(.obj X).hom = X.hom
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_map_left {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
∀ {X_1 Y : } (f : X_1 Y), (.map f).left = CategoryTheory.CategoryStruct.id X_1.left
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_obj_left {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) (X : ) :
(.obj X).left = X.left
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_map_right {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) :
∀ {X_1 Y : } (f : X_1 Y), (.map f).right = F.map f.right
@[simp]
theorem CategoryTheory.StructuredArrow.toUnder_obj_right {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) (X : ) :
(.obj X).right = F.obj X.right
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.

Equations
Instances For
instance CategoryTheory.StructuredArrow.instFaithfulUnderToUnder {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) [F.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.StructuredArrow.instFullUnderToUnder {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) [F.Full] :
.Full
Equations
• =
instance CategoryTheory.StructuredArrow.instEssSurjUnderToUnder {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) [F.EssSurj] :
.EssSurj
Equations
• =
instance CategoryTheory.StructuredArrow.isEquivalence_toUnder {T : Type u₁} [] {D : Type u₂} [] (X : T) (F : ) [F.IsEquivalence] :
.IsEquivalence

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

Equations
• =
@[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) :
((F.toOver X f h).obj Y).left = F.obj Y
@[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_1 Y : S} (g : X_1 Y), ((F.toOver X f h).map g).left = F.map g
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.

Equations
• F.toOver X f h = F.toCostructuredArrow X f
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) :
(F.toOver X f ).comp F

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

Equations
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) :
(F.toOver X f ).comp = F
@[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_1 Y : S} (g : X_1 Y), ((F.toUnder X f h).map g).right = F.map g
@[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) :
((F.toUnder X f h).obj Y).right = F.obj Y
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.

Equations
• F.toUnder X f h = F.toStructuredArrow X f
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) :
(F.toUnder X f ).comp F

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

Equations
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) :
(F.toUnder X f ).comp = F
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_left_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), .right.right = g.right.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_left_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
.left.as = PUnit.unit
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
.right.left.as = PUnit.unit
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
.right.hom = Y.hom
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
.right.right = Y.right.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
.hom = Y.right.hom
def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :

A functor from the structured arrow category on the projection functor for any structured arrow category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) (Y : CategoryTheory.StructuredArrow Y✝ (.comp F)) :
.right.left.as = PUnit.unit
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) (Y : CategoryTheory.StructuredArrow Y✝ (.comp F)) :
.hom = Y.right.hom
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) (Y : CategoryTheory.StructuredArrow Y✝ (.comp F)) :
.right.hom = Y.hom
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), .right.right = g.right.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) (Y : CategoryTheory.StructuredArrow Y✝ (.comp F)) :
.right.right = Y.right.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_left_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) (Y : CategoryTheory.StructuredArrow Y✝ (.comp F)) :
.left.as = PUnit.unit
@[simp]
theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_left_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :

The inverse functor of ofStructuredArrowProjEquivalence.functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : T) (X : D) :

Characterization of the structured arrow category on the projection functor of any structured arrow category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_left_down_down {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), =
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_right {T : Type u₁} [] (X : T × T) :
.right.right = Y.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_right {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), .right.right = g.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_left_down_down {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), =
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_hom {T : Type u₁} [] (X : T × T) :
.hom = Y.hom.2
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_hom {T : Type u₁} [] (X : T × T) :
.right.hom = Y.hom.1

The canonical functor from the structured arrow category on the diagonal functor T ⥤ T × T to the the structured arrow category on Under.forget.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_left_down_down {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), =
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_right {T : Type u₁} [] (X : T × T) (Y : ) :
.right = Y.right.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_right {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), .right = g.right.right
@[simp]
theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_hom {T : Type u₁} [] (X : T × T) (Y : ) :
.hom = (Y.right.hom, Y.hom)
@[simp]

The inverse functor of ofDiagEquivalence.functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Characterization of the structured arrow category on the diagonal functor T ⥤ T × T.

Equations
• One or more equations did not get rendered due to their size.
Instances For

A version of StructuredArrow.ofDiagEquivalence with the roles of the first and second projection swapped.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_left_right_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
.left.left = Y.left.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
.left.hom = Y.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_right_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
.left.right.as = PUnit.unit
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
.hom = Y.left.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_right_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
.right.as = PUnit.unit
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_left_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), .left.left = g.left.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_right_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :

A functor from the costructured arrow category on the projection functor for any costructured arrow category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_right_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) (Y : CategoryTheory.CostructuredArrow (.comp F) Y✝) :
.left.hom = Y.hom
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) (Y : CategoryTheory.CostructuredArrow (.comp F) Y✝) :
.left.left = Y.left.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_right_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) (Y : CategoryTheory.CostructuredArrow (.comp F) Y✝) :
.left.right.as = PUnit.unit
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_right_as {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) (Y : CategoryTheory.CostructuredArrow (.comp F) Y✝) :
.right.as = PUnit.unit
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_right_down_down {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), =
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_left {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :
∀ {X_1 Y_1 : } (g : X_1 Y_1), .left.left = g.left.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_hom {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) (Y : CategoryTheory.CostructuredArrow (.comp F) Y✝) :
.hom = Y.left.hom
def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :

The inverse functor of ofCostructuredArrowProjEquivalence.functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence {T : Type u₁} [] {D : Type u₂} [] (F : ) (Y : D) (X : T) :

Characterization of the costructured arrow category on the projection functor of any costructured arrow category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_left_left {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), .left.left = g.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_hom {T : Type u₁} [] (X : T × T) :
.left.hom = Y.hom.1
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_hom {T : Type u₁} [] (X : T × T) :
.hom = Y.hom.2
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_left_right_down_down {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), =
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_left {T : Type u₁} [] (X : T × T) :
.left.left = Y.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_right_down_down {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), =

The canonical functor from the costructured arrow category on the diagonal functor T ⥤ T × T to the the costructured arrow category on Under.forget.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_map_left {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), .left = g.left.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_left {T : Type u₁} [] (X : T × T) (Y : ) :
.left = Y.left.left
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_map_right_down_down {T : Type u₁} [] (X : T × T) :
∀ {X_1 Y : } (g : X_1 Y), =
@[simp]
theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_hom {T : Type u₁} [] (X : T × T) (Y : ) :
.hom = (Y.left.hom, Y.hom)

The inverse functor of ofDiagEquivalence.functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Characterization of the costructured arrow category on the diagonal functor T ⥤ T × T.

Equations
• One or more equations did not get rendered due to their size.
Instances For

A version of CostructuredArrow.ofDiagEquivalence with the roles of the first and second projection swapped.

Equations
• One or more equations did not get rendered due to their size.
Instances For