mathlib3 documentation

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.

Tags #

comma, slice, coslice, over, under

source
@[protected, instance]
def category_theory.over.category {T : Type u₁} [category_theory.category T] (X : T) :
category_theory.category (category_theory.over X)
source
def category_theory.over {T : Type u₁} [category_theory.category T] (X : T) :
Type (max u₁ v₁)

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

See https://stacks.math.columbia.edu/tag/001G.

Equations
Instances for category_theory.over
source
@[protected, instance]
def category_theory.over.inhabited {T : Type u₁} [category_theory.category T] [inhabited T] :
inhabited (category_theory.over inhabited.default)
Equations
source
@[ext]
theorem category_theory.over.over_morphism.ext {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.over X} {f g : U ⟶ V} (h : f.left = g.left) :
f = g
source
@[simp]
theorem category_theory.over.over_right {T : Type u₁} [category_theory.category T] {X : T} (U : category_theory.over X) :
U.right = {as := punit.star}
source
@[simp]
theorem category_theory.over.id_left {T : Type u₁} [category_theory.category T] {X : T} (U : category_theory.over X) :
(𝟙 U).left = 𝟙 U.left
source
@[simp]
theorem category_theory.over.comp_left {T : Type u₁} [category_theory.category T] {X : T} (a b c : category_theory.over X) (f : a ⟶ b) (g : b ⟶ c) :
(f ≫ g).left = f.left ≫ g.left
source
@[simp]
theorem category_theory.over.w {T : Type u₁} [category_theory.category T] {X : T} {A B : category_theory.over X} (f : A ⟶ B) :
f.left ≫ B.hom = A.hom
source
@[simp]
theorem category_theory.over.w_assoc {T : Type u₁} [category_theory.category T] {X : T} {A B : category_theory.over X} (f : A ⟶ B) {X' : T} (f' : (category_theory.functor.from_punit X).obj B.right ⟶ X') :
f.left ≫ B.hom ≫ f' = A.hom ≫ f'
source
@[simp]
theorem category_theory.over.mk_hom {T : Type u₁} [category_theory.category T] {X Y : T} (f : Y ⟶ X) :
(category_theory.over.mk f).hom = f
source
@[simp]
theorem category_theory.over.mk_left {T : Type u₁} [category_theory.category T] {X Y : T} (f : Y ⟶ X) :
(category_theory.over.mk f).left = Y
source
def category_theory.over.mk {T : Type u₁} [category_theory.category T] {X Y : T} (f : Y ⟶ X) :
category_theory.over X

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

Equations
source
def category_theory.over.coe_from_hom {T : Type u₁} [category_theory.category T] {X Y : T} :
has_coe (Y ⟶ X) (category_theory.over 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
source
@[simp]
theorem category_theory.over.coe_hom {T : Type u₁} [category_theory.category T] {X Y : T} (f : Y ⟶ X) :
↑f.hom = f
source
def category_theory.over.hom_mk {T : Type u₁} [category_theory.category T] {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
source
@[simp]
theorem category_theory.over.hom_mk_left {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.over X} (f : U.left ⟶ V.left) (w : f ≫ V.hom = U.hom . "obviously") :
(category_theory.over.hom_mk f w).left = f
source
@[simp]
theorem category_theory.over.hom_mk_right {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.over X} (f : U.left ⟶ V.left) (w : f ≫ V.hom = U.hom . "obviously") :
(category_theory.over.hom_mk f w).right = category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1
source
@[simp]
theorem category_theory.over.iso_mk_inv_right {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (hl : f.left ≅ g.left) (hw : hl.hom ≫ g.hom = f.hom . "obviously") :
(category_theory.over.iso_mk hl hw).inv.right = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.over.iso_mk_hom_right {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (hl : f.left ≅ g.left) (hw : hl.hom ≫ g.hom = f.hom . "obviously") :
(category_theory.over.iso_mk hl hw).hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
source
@[simp]
theorem category_theory.over.iso_mk_hom_left {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (hl : f.left ≅ g.left) (hw : hl.hom ≫ g.hom = f.hom . "obviously") :
(category_theory.over.iso_mk hl hw).hom.left = hl.hom
source
@[simp]
theorem category_theory.over.iso_mk_inv_left {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (hl : f.left ≅ g.left) (hw : hl.hom ≫ g.hom = f.hom . "obviously") :
(category_theory.over.iso_mk hl hw).inv.left = hl.inv
source
def category_theory.over.iso_mk {T : Type u₁} [category_theory.category T] {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
source
def category_theory.over.forget {T : Type u₁} [category_theory.category T] (X : T) :
category_theory.over X ⥤ T

The forgetful functor mapping an arrow to its domain.

See https://stacks.math.columbia.edu/tag/001G.

Equations
Instances for category_theory.over.forget
source
@[simp]
theorem category_theory.over.forget_obj {T : Type u₁} [category_theory.category T] {X : T} {U : category_theory.over X} :
(category_theory.over.forget X).obj U = U.left
source
@[simp]
theorem category_theory.over.forget_map {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.over X} {f : U ⟶ V} :
(category_theory.over.forget X).map f = f.left
source
@[simp]
theorem category_theory.over.forget_cocone_ι_app {T : Type u₁} [category_theory.category T] (X : T) (self : category_theory.comma (𝟭 T) (category_theory.functor.from_punit X)) :
(category_theory.over.forget_cocone X).ι.app self = self.hom
source
@[simp]
theorem category_theory.over.forget_cocone_X {T : Type u₁} [category_theory.category T] (X : T) :
(category_theory.over.forget_cocone X).X = X
source
def category_theory.over.forget_cocone {T : Type u₁} [category_theory.category T] (X : T) :
category_theory.limits.cocone (category_theory.over.forget X)

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

Equations
source
def category_theory.over.map {T : Type u₁} [category_theory.category T] {X Y : T} (f : X ⟶ Y) :
category_theory.over X ⥤ category_theory.over Y

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

See https://stacks.math.columbia.edu/tag/001G.

Equations
source
@[simp]
theorem category_theory.over.map_obj_left {T : Type u₁} [category_theory.category T] {X Y : T} {f : X ⟶ Y} {U : category_theory.over X} :
((category_theory.over.map f).obj U).left = U.left
source
@[simp]
theorem category_theory.over.map_obj_hom {T : Type u₁} [category_theory.category T] {X Y : T} {f : X ⟶ Y} {U : category_theory.over X} :
((category_theory.over.map f).obj U).hom = U.hom ≫ f
source
@[simp]
theorem category_theory.over.map_map_left {T : Type u₁} [category_theory.category T] {X Y : T} {f : X ⟶ Y} {U V : category_theory.over X} {g : U ⟶ V} :
((category_theory.over.map f).map g).left = g.left
source
def category_theory.over.map_id {T : Type u₁} [category_theory.category T] {Y : T} :
category_theory.over.map (𝟙 Y) ≅ 𝟭 (category_theory.over Y)

Mapping by the identity morphism is just the identity functor.

Equations
source
def category_theory.over.map_comp {T : Type u₁} [category_theory.category T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
category_theory.over.map (f ≫ g) ≅ category_theory.over.map f ⋙ category_theory.over.map g

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

Equations
source
@[protected, instance]
def category_theory.over.forget_reflects_iso {T : Type u₁} [category_theory.category T] {X : T} :
category_theory.reflects_isomorphisms (category_theory.over.forget X)
source
@[protected, instance]
def category_theory.over.forget_faithful {T : Type u₁} [category_theory.category T] {X : T} :
category_theory.faithful (category_theory.over.forget X)
source
theorem category_theory.over.epi_of_epi_left {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (k : f ⟶ g) [hk : category_theory.epi k.left] :
category_theory.epi k

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.

source
theorem category_theory.over.mono_of_mono_left {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (k : f ⟶ g) [hk : category_theory.mono k.left] :
category_theory.mono k

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.

source
@[protected, instance]
def category_theory.over.mono_left_of_mono {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.over X} (k : f ⟶ g) [category_theory.mono k] :
category_theory.mono k.left

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.

source
@[simp]
theorem category_theory.over.iterated_slice_forward_obj {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) (α : category_theory.over f) :
f.iterated_slice_forward.obj α = category_theory.over.mk α.hom.left
source
def category_theory.over.iterated_slice_forward {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
category_theory.over f ⥤ category_theory.over f.left

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

Equations
source
@[simp]
theorem category_theory.over.iterated_slice_forward_map {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) (α β : category_theory.over f) (κ : α ⟶ β) :
f.iterated_slice_forward.map κ = category_theory.over.hom_mk κ.left.left _
source
@[simp]
theorem category_theory.over.iterated_slice_backward_map {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) (g h : category_theory.over f.left) (α : g ⟶ h) :
f.iterated_slice_backward.map α = category_theory.over.hom_mk (category_theory.over.hom_mk α.left _) _
source
@[simp]
theorem category_theory.over.iterated_slice_backward_obj {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) (g : category_theory.over f.left) :
f.iterated_slice_backward.obj g = category_theory.over.mk (category_theory.over.hom_mk g.hom _)
source
def category_theory.over.iterated_slice_backward {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
category_theory.over f.left ⥤ category_theory.over f

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

Equations
source
def category_theory.over.iterated_slice_equiv {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
category_theory.over f ≌ category_theory.over f.left

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

Equations
source
@[simp]
theorem category_theory.over.iterated_slice_equiv_inverse {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
f.iterated_slice_equiv.inverse = f.iterated_slice_backward
source
@[simp]
theorem category_theory.over.iterated_slice_equiv_unit_iso {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
f.iterated_slice_equiv.unit_iso = category_theory.nat_iso.of_components (λ (g : category_theory.over f), category_theory.over.iso_mk (category_theory.over.iso_mk (category_theory.iso.refl ((𝟭 (category_theory.over f)).obj g).left.left) _) _) _
source
@[simp]
theorem category_theory.over.iterated_slice_equiv_counit_iso {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
f.iterated_slice_equiv.counit_iso = category_theory.nat_iso.of_components (λ (g : category_theory.over f.left), category_theory.over.iso_mk (category_theory.iso.refl ((f.iterated_slice_backward ⋙ f.iterated_slice_forward).obj g).left) _) _
source
@[simp]
theorem category_theory.over.iterated_slice_equiv_functor {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
f.iterated_slice_equiv.functor = f.iterated_slice_forward
source
theorem category_theory.over.iterated_slice_forward_forget {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
f.iterated_slice_forward ⋙ category_theory.over.forget f.left = category_theory.over.forget f ⋙ category_theory.over.forget X
source
theorem category_theory.over.iterated_slice_backward_forget_forget {T : Type u₁} [category_theory.category T] {X : T} (f : category_theory.over X) :
f.iterated_slice_backward ⋙ category_theory.over.forget f ⋙ category_theory.over.forget X = category_theory.over.forget f.left
source
@[simp]
theorem category_theory.over.post_map {T : Type u₁} [category_theory.category T] {X : T} {D : Type u₂} [category_theory.category D] (F : T ⥤ D) (Y₁ Y₂ : category_theory.over X) (f : Y₁ ⟶ Y₂) :
(category_theory.over.post F).map f = category_theory.over.hom_mk (F.map f.left) _
source
@[simp]
theorem category_theory.over.post_obj {T : Type u₁} [category_theory.category T] {X : T} {D : Type u₂} [category_theory.category D] (F : T ⥤ D) (Y : category_theory.over X) :
(category_theory.over.post F).obj Y = category_theory.over.mk (F.map Y.hom)
source
def category_theory.over.post {T : Type u₁} [category_theory.category T] {X : T} {D : Type u₂} [category_theory.category D] (F : T ⥤ D) :
category_theory.over X ⥤ category_theory.over (F.obj X)

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

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

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

Equations
source
@[simp]
theorem category_theory.under.hom_mk_left {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.under X} (f : U.right ⟶ V.right) (w : U.hom ≫ f = V.hom . "obviously") :
(category_theory.under.hom_mk f w).left = category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1
source
@[simp]
theorem category_theory.under.hom_mk_right {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.under X} (f : U.right ⟶ V.right) (w : U.hom ≫ f = V.hom . "obviously") :
(category_theory.under.hom_mk f w).right = f
source
def category_theory.under.hom_mk {T : Type u₁} [category_theory.category T] {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
source
def category_theory.under.iso_mk {T : Type u₁} [category_theory.category T] {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
source
@[simp]
theorem category_theory.under.iso_mk_hom_right {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) :
(category_theory.under.iso_mk hr hw).hom.right = hr.hom
source
@[simp]
theorem category_theory.under.iso_mk_inv_right {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) :
(category_theory.under.iso_mk hr hw).inv.right = hr.inv
source
def category_theory.under.forget {T : Type u₁} [category_theory.category T] (X : T) :
category_theory.under X ⥤ T

The forgetful functor mapping an arrow to its domain.

Equations
Instances for category_theory.under.forget
source
@[simp]
theorem category_theory.under.forget_obj {T : Type u₁} [category_theory.category T] {X : T} {U : category_theory.under X} :
(category_theory.under.forget X).obj U = U.right
source
@[simp]
theorem category_theory.under.forget_map {T : Type u₁} [category_theory.category T] {X : T} {U V : category_theory.under X} {f : U ⟶ V} :
(category_theory.under.forget X).map f = f.right
source
@[simp]
theorem category_theory.under.forget_cone_π_app {T : Type u₁} [category_theory.category T] (X : T) (self : category_theory.comma (category_theory.functor.from_punit X) (𝟭 T)) :
(category_theory.under.forget_cone X).π.app self = self.hom
source
def category_theory.under.forget_cone {T : Type u₁} [category_theory.category T] (X : T) :
category_theory.limits.cone (category_theory.under.forget X)

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

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

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

Equations
source
@[simp]
theorem category_theory.under.map_obj_right {T : Type u₁} [category_theory.category T] {X Y : T} {f : X ⟶ Y} {U : category_theory.under Y} :
((category_theory.under.map f).obj U).right = U.right
source
@[simp]
theorem category_theory.under.map_obj_hom {T : Type u₁} [category_theory.category T] {X Y : T} {f : X ⟶ Y} {U : category_theory.under Y} :
((category_theory.under.map f).obj U).hom = f ≫ U.hom
source
@[simp]
theorem category_theory.under.map_map_right {T : Type u₁} [category_theory.category T] {X Y : T} {f : X ⟶ Y} {U V : category_theory.under Y} {g : U ⟶ V} :
((category_theory.under.map f).map g).right = g.right
source
def category_theory.under.map_id {T : Type u₁} [category_theory.category T] {Y : T} :
category_theory.under.map (𝟙 Y) ≅ 𝟭 (category_theory.under Y)

Mapping by the identity morphism is just the identity functor.

Equations
source
def category_theory.under.map_comp {T : Type u₁} [category_theory.category T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
category_theory.under.map (f ≫ g) ≅ category_theory.under.map g ⋙ category_theory.under.map f

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

Equations
source
@[protected, instance]
def category_theory.under.forget_reflects_iso {T : Type u₁} [category_theory.category T] {X : T} :
category_theory.reflects_isomorphisms (category_theory.under.forget X)
source
@[protected, instance]
def category_theory.under.forget_faithful {T : Type u₁} [category_theory.category T] {X : T} :
category_theory.faithful (category_theory.under.forget X)
source
theorem category_theory.under.mono_of_mono_right {T : Type u₁} [category_theory.category T] {X : T} {f g : category_theory.under X} (k : f ⟶ g) [hk : category_theory.mono k.right] :
category_theory.mono k

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.

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

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.

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

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.

source
def category_theory.under.post {T : Type u₁} [category_theory.category T] {D : Type u₂} [category_theory.category D] {X : T} (F : T ⥤ D) :
category_theory.under X ⥤ category_theory.under (F.obj X)

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

Equations
source
@[simp]
theorem category_theory.under.post_map {T : Type u₁} [category_theory.category T] {D : Type u₂} [category_theory.category D] {X : T} (F : T ⥤ D) (Y₁ Y₂ : category_theory.under X) (f : Y₁ ⟶ Y₂) :
(category_theory.under.post F).map f = category_theory.under.hom_mk (F.map f.right) _
source
@[simp]
theorem category_theory.under.post_obj {T : Type u₁} [category_theory.category T] {D : Type u₂} [category_theory.category D] {X : T} (F : T ⥤ D) (Y : category_theory.under X) :
(category_theory.under.post F).obj Y = category_theory.under.mk (F.map Y.hom)