# mathlib3documentation

category_theory.over

# Over and under categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def category_theory.over.category {T : Type u₁} (X : T) :
def category_theory.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 category_theory.over
@[protected, instance]
Equations
@[ext]
theorem category_theory.over.over_morphism.ext {T : Type u₁} {X : T} {U V : category_theory.over X} {f g : U V} (h : f.left = g.left) :
f = g
@[simp]
theorem category_theory.over.over_right {T : Type u₁} {X : T} (U : category_theory.over X) :
U.right = {as := punit.star}
@[simp]
theorem category_theory.over.id_left {T : Type u₁} {X : T} (U : category_theory.over X) :
@[simp]
theorem category_theory.over.comp_left {T : Type u₁} {X : T} (a b c : category_theory.over X) (f : a b) (g : b c) :
(f g).left = f.left g.left
@[simp]
theorem category_theory.over.w {T : Type u₁} {X : T} {A B : category_theory.over X} (f : A B) :
f.left B.hom = A.hom
@[simp]
theorem category_theory.over.w_assoc {T : Type u₁} {X : T} {A B : category_theory.over X} (f : A B) {X' : T} (f' : X') :
f.left B.hom f' = A.hom f'
@[simp]
theorem category_theory.over.mk_hom {T : Type u₁} {X Y : T} (f : Y X) :
@[simp]
theorem category_theory.over.mk_left {T : Type u₁} {X Y : T} (f : Y X) :
def category_theory.over.mk {T : Type u₁} {X Y : T} (f : Y X) :

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

Equations
def category_theory.over.coe_from_hom {T : Type u₁} {X Y : T} :
has_coe (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
@[simp]
theorem category_theory.over.coe_hom {T : Type u₁} {X Y : T} (f : Y X) :
f.hom = f
def category_theory.over.hom_mk {T : Type u₁} {X : T} {U V : category_theory.over X} (f : U.left V.left) (w : f V.hom = U.hom . "obviously") :
U V

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

Equations
@[simp]
theorem category_theory.over.hom_mk_left {T : Type u₁} {X : T} {U V : category_theory.over X} (f : U.left V.left) (w : f V.hom = U.hom . "obviously") :
= f
@[simp]
theorem category_theory.over.hom_mk_right {T : Type u₁} {X : T} {U V : category_theory.over X} (f : U.left V.left) (w : f V.hom = U.hom . "obviously") :
= category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1
@[simp]
theorem category_theory.over.iso_mk_inv_right {T : Type u₁} {X : T} {f g : category_theory.over X} (hl : f.left g.left) (hw : hl.hom g.hom = f.hom . "obviously") :
@[simp]
theorem category_theory.over.iso_mk_hom_right {T : Type u₁} {X : T} {f g : category_theory.over X} (hl : f.left g.left) (hw : hl.hom g.hom = f.hom . "obviously") :
hw).hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[simp]
theorem category_theory.over.iso_mk_hom_left {T : Type u₁} {X : T} {f g : category_theory.over X} (hl : f.left g.left) (hw : hl.hom g.hom = f.hom . "obviously") :
hw).hom.left = hl.hom
@[simp]
theorem category_theory.over.iso_mk_inv_left {T : Type u₁} {X : T} {f g : category_theory.over X} (hl : f.left g.left) (hw : hl.hom g.hom = f.hom . "obviously") :
hw).inv.left = hl.inv
def category_theory.over.iso_mk {T : Type u₁} {X : T} {f g : category_theory.over X} (hl : f.left g.left) (hw : hl.hom g.hom = f.hom . "obviously") :
f g

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

Equations
def category_theory.over.forget {T : Type u₁} (X : T) :

The forgetful functor mapping an arrow to its domain.

Equations
Instances for category_theory.over.forget
@[simp]
theorem category_theory.over.forget_obj {T : Type u₁} {X : T} {U : category_theory.over X} :
= U.left
@[simp]
theorem category_theory.over.forget_map {T : Type u₁} {X : T} {U V : category_theory.over X} {f : U V} :
= f.left
@[simp]
theorem category_theory.over.forget_cocone_ι_app {T : Type u₁} (X : T) (self : ) :
self = self.hom
@[simp]
theorem category_theory.over.forget_cocone_X {T : Type u₁} (X : T) :

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

Equations
def category_theory.over.map {T : Type u₁} {X Y : T} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.over.map_obj_left {T : Type u₁} {X Y : T} {f : X Y} {U : category_theory.over X} :
U).left = U.left
@[simp]
theorem category_theory.over.map_obj_hom {T : Type u₁} {X Y : T} {f : X Y} {U : category_theory.over X} :
U).hom = U.hom f
@[simp]
theorem category_theory.over.map_map_left {T : Type u₁} {X Y : T} {f : X Y} {U V : category_theory.over X} {g : U V} :
g).left = g.left
def category_theory.over.map_id {T : Type u₁} {Y : T} :

Mapping by the identity morphism is just the identity functor.

Equations
def category_theory.over.map_comp {T : Type u₁} {X Y 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.

Equations
@[protected, instance]
@[protected, instance]
def category_theory.over.forget_faithful {T : Type u₁} {X : T} :
theorem category_theory.over.epi_of_epi_left {T : Type u₁} {X : T} {f g : category_theory.over X} (k : f g) [hk : category_theory.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 category_theory.over.epi_left_of_epi.

theorem category_theory.over.mono_of_mono_left {T : Type u₁} {X : T} {f g : category_theory.over X} (k : f g) [hk : category_theory.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 category_theory.over.mono_left_of_mono.

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

@[protected, instance]
def category_theory.over.mono_left_of_mono {T : Type u₁} {X : T} {f g : category_theory.over X} (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 category_theory.over.mono_of_mono_left.

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

Equations
@[simp]
theorem category_theory.over.iterated_slice_forward_map {T : Type u₁} {X : T} (f : category_theory.over X) (α β : category_theory.over f) (κ : α β) :
@[simp]
theorem category_theory.over.iterated_slice_backward_map {T : Type u₁} {X : T} (f : category_theory.over X) (g h : category_theory.over f.left) (α : g h) :

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

Equations

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

Equations
@[simp]
theorem category_theory.over.post_map {T : Type u₁} {X : T} {D : Type u₂} (F : T D) (Y₁ Y₂ : category_theory.over X) (f : Y₁ Y₂) :
= _
@[simp]
theorem category_theory.over.post_obj {T : Type u₁} {X : T} {D : Type u₂} (F : T D) (Y : category_theory.over X) :
=
def category_theory.over.post {T : Type u₁} {X : T} {D : Type u₂} (F : T D) :

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

Equations
@[protected, instance]
def category_theory.under.category {T : Type u₁} (X : T) :
def category_theory.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 category_theory.under
@[protected, instance]
Equations
@[ext]
theorem category_theory.under.under_morphism.ext {T : Type u₁} {X : T} {U V : category_theory.under X} {f g : U V} (h : f.right = g.right) :
f = g
@[simp]
theorem category_theory.under.under_left {T : Type u₁} {X : T} (U : category_theory.under X) :
U.left = {as := punit.star}
@[simp]
theorem category_theory.under.id_right {T : Type u₁} {X : T} (U : category_theory.under X) :
@[simp]
theorem category_theory.under.comp_right {T : Type u₁} {X : T} (a b c : category_theory.under X) (f : a b) (g : b c) :
(f g).right = f.right g.right
@[simp]
theorem category_theory.under.w_assoc {T : Type u₁} {X : T} {A B : category_theory.under X} (f : A B) {X' : T} (f' : B.right X') :
A.hom f.right f' = B.hom f'
@[simp]
theorem category_theory.under.w {T : Type u₁} {X : T} {A B : category_theory.under X} (f : A B) :
A.hom f.right = B.hom
@[simp]
theorem category_theory.under.mk_hom {T : Type u₁} {X Y : T} (f : X Y) :
@[simp]
theorem category_theory.under.mk_right {T : Type u₁} {X Y : T} (f : X Y) :
def category_theory.under.mk {T : Type u₁} {X Y : T} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.under.hom_mk_left {T : Type u₁} {X : T} {U V : category_theory.under X} (f : U.right V.right) (w : U.hom f = V.hom . "obviously") :
= category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1
@[simp]
theorem category_theory.under.hom_mk_right {T : Type u₁} {X : T} {U V : category_theory.under X} (f : U.right V.right) (w : U.hom f = V.hom . "obviously") :
def category_theory.under.hom_mk {T : Type u₁} {X : T} {U V : category_theory.under X} (f : U.right V.right) (w : U.hom f = V.hom . "obviously") :
U V

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

Equations
def category_theory.under.iso_mk {T : Type u₁} {X : T} {f g : category_theory.under X} (hr : f.right g.right) (hw : f.hom hr.hom = g.hom) :
f g

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

Equations
@[simp]
theorem category_theory.under.iso_mk_hom_right {T : Type u₁} {X : T} {f g : category_theory.under X} (hr : f.right g.right) (hw : f.hom hr.hom = g.hom) :
hw).hom.right = hr.hom
@[simp]
theorem category_theory.under.iso_mk_inv_right {T : Type u₁} {X : T} {f g : category_theory.under X} (hr : f.right g.right) (hw : f.hom hr.hom = g.hom) :
hw).inv.right = hr.inv
def category_theory.under.forget {T : Type u₁} (X : T) :

The forgetful functor mapping an arrow to its domain.

Equations
Instances for category_theory.under.forget
@[simp]
theorem category_theory.under.forget_obj {T : Type u₁} {X : T} {U : category_theory.under X} :
@[simp]
theorem category_theory.under.forget_map {T : Type u₁} {X : T} {U V : category_theory.under X} {f : U V} :
@[simp]
theorem category_theory.under.forget_cone_π_app {T : Type u₁} (X : T) (self : (𝟭 T)) :
self = self.hom
def category_theory.under.forget_cone {T : Type u₁} (X : T) :

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

Equations
@[simp]
theorem category_theory.under.forget_cone_X {T : Type u₁} (X : T) :
def category_theory.under.map {T : Type u₁} {X Y : T} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.under.map_obj_right {T : Type u₁} {X Y : T} {f : X Y} {U : category_theory.under Y} :
U).right = U.right
@[simp]
theorem category_theory.under.map_obj_hom {T : Type u₁} {X Y : T} {f : X Y} {U : category_theory.under Y} :
U).hom = f U.hom
@[simp]
theorem category_theory.under.map_map_right {T : Type u₁} {X Y : T} {f : X Y} {U V : category_theory.under Y} {g : U V} :
g).right = g.right
def category_theory.under.map_id {T : Type u₁} {Y : T} :

Mapping by the identity morphism is just the identity functor.

Equations
def category_theory.under.map_comp {T : Type u₁} {X Y 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.

Equations
@[protected, instance]
@[protected, instance]
theorem category_theory.under.mono_of_mono_right {T : Type u₁} {X : T} {f g : category_theory.under X} (k : f g) [hk : category_theory.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 category_theory.under.mono_right_of_mono.

theorem category_theory.under.epi_of_epi_right {T : Type u₁} {X : T} {f g : category_theory.under X} (k : f g) [hk : category_theory.epi k.right] :

If k.right is a epimorphism, then k is a epimorphism. In other words, under.forget X reflects epimorphisms. The converse of category_theory.under.epi_right_of_epi.

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

@[protected, instance]
def category_theory.under.epi_right_of_epi {T : Type u₁} {X : T} {f g : category_theory.under X} (k : f g)  :

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

def category_theory.under.post {T : Type u₁} {D : Type u₂} {X : T} (F : T D) :

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

Equations
@[simp]
theorem category_theory.under.post_map {T : Type u₁} {D : Type u₂} {X : T} (F : T D) (Y₁ Y₂ : category_theory.under X) (f : Y₁ Y₂) :
= _
@[simp]
theorem category_theory.under.post_obj {T : Type u₁} {D : Type u₂} {X : T} (F : T D) (Y : category_theory.under X) :
=