Over and under categories
Over (and under) categories are special cases of comma categories.
- If
Lis the identity functor andRis a constant functor, thencomma L Ris the "slice" or "over" category over the objectRmaps to. - Conversely, if
Lis a constant functor andRis the identity functor, thencomma L Ris the "coslice" or "under" category under the objectLmaps to.
Tags
comma, slice, coslice, over, under
@[instance]
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
@[instance]
@[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
@[simp]
theorem
category_theory.over.over_right
{T : Type u₁}
[category_theory.category T]
{X : T}
(U : category_theory.over X) :
U.right = punit.star
@[simp]
theorem
category_theory.over.id_left
{T : Type u₁}
[category_theory.category T]
{X : T}
(U : category_theory.over X) :
@[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) :
@[simp]
theorem
category_theory.over.w
{T : Type u₁}
[category_theory.category T]
{X : T}
{A B : category_theory.over X}
(f : A ⟶ B) :
@[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 . "obviously"}
(f' : (category_theory.functor.from_punit X).obj B.right ⟶ X') :
@[simp]
theorem
category_theory.over.mk_right
{T : Type u₁}
[category_theory.category T]
{X Y : T}
(f : Y ⟶ X) :
@[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
@[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
To give an object in the over category, it suffices to give a morphism with codomain X.
Equations
- category_theory.over.mk f = {left := Y, right := punit.star, hom := f}
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
@[simp]
theorem
category_theory.over.coe_hom
{T : Type u₁}
[category_theory.category T]
{X Y : T}
(f : Y ⟶ X) :
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.
@[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
@[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") :
@[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_iso category_theory.over.iso_mk._proof_1).inv
@[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_iso category_theory.over.iso_mk._proof_1).hom
@[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
@[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
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
- category_theory.over.iso_mk hl hw = category_theory.comma.iso_mk hl (category_theory.eq_to_iso category_theory.over.iso_mk._proof_1) _
The forgetful functor mapping an arrow to its domain.
See https://stacks.math.columbia.edu/tag/001G.
Equations
@[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
@[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
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
@[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
@[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} :
@[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
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
- category_theory.over.map_id = category_theory.nat_iso.of_components (λ (X : category_theory.over Y), category_theory.over.iso_mk (category_theory.iso.refl ((category_theory.over.map (𝟙 Y)).obj X).left) _) category_theory.over.map_id._proof_2
def
category_theory.over.map_comp
{T : Type u₁}
[category_theory.category T]
{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
- category_theory.over.map_comp f g = category_theory.nat_iso.of_components (λ (X_1 : category_theory.over X), category_theory.over.iso_mk (category_theory.iso.refl ((category_theory.over.map (f ≫ g)).obj X_1).left) _) _
@[instance]
Equations
- category_theory.over.forget_reflects_iso = {reflects := λ (Y Z : category_theory.over X) (f : Y ⟶ Z) (t : category_theory.is_iso ((category_theory.over.forget X).map f)), {inv := category_theory.over.hom_mk (category_theory.is_iso.inv ((category_theory.over.forget X).map f)) _, hom_inv_id' := _, inv_hom_id' := _}}
@[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) :
def
category_theory.over.iterated_slice_forward
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y
Equations
- f.iterated_slice_forward = {obj := λ (α : category_theory.over f), category_theory.over.mk α.hom.left, map := λ (α β : category_theory.over f) (κ : α ⟶ β), category_theory.over.hom_mk κ.left.left _, map_id' := _, map_comp' := _}
@[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)
(κ : α ⟶ β) :
@[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) :
@[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) :
def
category_theory.over.iterated_slice_backward
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f
Equations
- f.iterated_slice_backward = {obj := λ (g : category_theory.over f.left), category_theory.over.mk (category_theory.over.hom_mk g.hom _), map := λ (g h : category_theory.over f.left) (α : g ⟶ h), category_theory.over.hom_mk (category_theory.over.hom_mk α.left _) _, map_id' := _, map_comp' := _}
def
category_theory.over.iterated_slice_equiv
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y
Equations
- f.iterated_slice_equiv = {functor := f.iterated_slice_forward, inverse := f.iterated_slice_backward, 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) _) _) _, 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) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.over.iterated_slice_equiv_inverse
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
@[simp]
theorem
category_theory.over.iterated_slice_equiv_unit_iso
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
@[simp]
theorem
category_theory.over.iterated_slice_equiv_counit_iso
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
@[simp]
theorem
category_theory.over.iterated_slice_equiv_functor
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
theorem
category_theory.over.iterated_slice_forward_forget
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
theorem
category_theory.over.iterated_slice_backward_forget_forget
{T : Type u₁}
[category_theory.category T]
{X : T}
(f : category_theory.over X) :
@[simp]
theorem
category_theory.over.post_map_right
{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₂) :
@[simp]
theorem
category_theory.over.post_map_left
{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₂) :
@[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)
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
- category_theory.over.post F = {obj := λ (Y : category_theory.over X), category_theory.over.mk (F.map Y.hom), map := λ (Y₁ Y₂ : category_theory.over X) (f : Y₁ ⟶ Y₂), {left := F.map f.left, right := id (λ (F : T ⥤ D) (Y₁ Y₂ : category_theory.over X) (f : Y₁ ⟶ Y₂), {down := category_theory.over.post._proof_1.mpr {down := _}}) F Y₁ Y₂ f, w' := _}, map_id' := _, map_comp' := _}
@[instance]
The under category has as objects arrows with domain X and as morphisms commutative
triangles.
Equations
@[instance]
Equations
- category_theory.under.inhabited = {default := {left := punit.star, right := default T _inst_2, hom := 𝟙 ((category_theory.functor.from_punit (default T)).obj punit.star)}}
@[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
@[simp]
theorem
category_theory.under.under_left
{T : Type u₁}
[category_theory.category T]
{X : T}
(U : category_theory.under X) :
U.left = punit.star
@[simp]
theorem
category_theory.under.id_right
{T : Type u₁}
[category_theory.category T]
{X : T}
(U : category_theory.under X) :
@[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) :
@[simp]
theorem
category_theory.under.w
{T : Type u₁}
[category_theory.category T]
{X : T}
{A B : category_theory.under X}
(f : A ⟶ B) :
@[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
@[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
@[simp]
theorem
category_theory.under.mk_left
{T : Type u₁}
[category_theory.category T]
{X Y : T}
(f : X ⟶ Y) :
To give an object in the under category, it suffices to give an arrow with domain X.
Equations
- category_theory.under.mk f = {left := punit.star, right := Y, hom := f}
@[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") :
@[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
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.
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
- category_theory.under.iso_mk hr hw = category_theory.comma.iso_mk (category_theory.eq_to_iso category_theory.under.iso_mk._proof_1) hr _
@[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
@[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
The forgetful functor mapping an arrow to its domain.
Equations
@[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
@[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
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₁}
[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
@[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} :
@[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
Mapping by the identity morphism is just the identity functor.
Equations
- category_theory.under.map_id = category_theory.nat_iso.of_components (λ (X : category_theory.under Y), category_theory.under.iso_mk (category_theory.iso.refl ((category_theory.under.map (𝟙 Y)).obj X).right) _) category_theory.under.map_id._proof_2
def
category_theory.under.map_comp
{T : Type u₁}
[category_theory.category T]
{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
- category_theory.under.map_comp f g = category_theory.nat_iso.of_components (λ (X_1 : category_theory.under Z), category_theory.under.iso_mk (category_theory.iso.refl ((category_theory.under.map (f ≫ g)).obj X_1).right) _) _
def
category_theory.under.post
{T : Type u₁}
[category_theory.category T]
{D : Type u₂}
[category_theory.category D]
{X : T}
(F : T ⥤ D) :
A functor F : T ⥤ D induces a functor under X ⥤ under (F.obj X) in the obvious way.
Equations
- category_theory.under.post F = {obj := λ (Y : category_theory.under X), category_theory.under.mk (F.map Y.hom), map := λ (Y₁ Y₂ : category_theory.under X) (f : Y₁ ⟶ Y₂), {left := id (λ {X : T} (F : T ⥤ D) (Y₁ Y₂ : category_theory.under X) (f : Y₁ ⟶ Y₂), {down := category_theory.under.post._proof_1.mpr {down := _}}) F Y₁ Y₂ f, right := F.map f.right, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.under.post_map_right
{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₂) :
@[simp]
theorem
category_theory.under.post_map_left
{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₂) :
@[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)