mathlib documentation

category_theory.over

Over and under categories

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

Tags

comma, slice, coslice, over, under

def category_theory.over {T : Type u₁} [category_theory.category T] :
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
@[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} :
f.left = g.leftf = g

@[simp]

@[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) :
(f g).left = f.left g.left

@[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

@[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') :
f.left B.hom f' = A.hom f'

@[simp]

@[simp]
theorem category_theory.over.mk_hom {T : Type u₁} [category_theory.category T] {X Y : T} (f : Y X) :

@[simp]
theorem category_theory.over.mk_left {T : Type u₁} [category_theory.category T] {X Y : T} (f : Y X) :

def category_theory.over.mk {T : Type u₁} [category_theory.category T] {X Y : T} :

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

Equations

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) :
f.hom = f

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) :
(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₁} [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.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 = id (λ {X : T} {U V : category_theory.over X} (f : U.left V.left) (w : f V.hom = U.hom), category_theory.over.hom_mk._proof_1.mpr {down := category_theory.over.hom_mk._proof_2.mpr {down := _}}) f w

@[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") :

@[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") :

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) :
(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

The forgetful functor mapping an arrow to its domain.

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

Equations
@[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} :

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} :

@[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} :

Mapping by the identity morphism is just the identity functor.

Equations

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

Equations

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

Equations
@[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₂) :
((category_theory.over.post F).map f).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

@[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]

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

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

Equations
def category_theory.under {T : Type u₁} [category_theory.category T] :
T → Type (max u₁ v₁)

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

Equations
@[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} :
f.right = g.rightf = g

@[simp]

@[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

@[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

@[simp]
theorem category_theory.under.mk_hom {T : Type u₁} [category_theory.category T] {X Y : T} (f : X Y) :

@[simp]
theorem category_theory.under.mk_right {T : Type u₁} [category_theory.category T] {X Y : T} (f : X Y) :

@[simp]

def category_theory.under.mk {T : Type u₁} [category_theory.category T] {X Y : T} :

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₁} [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 = id (λ {X : T} {U V : category_theory.under X} (f : U.right V.right) (w : U.hom f = V.hom), category_theory.under.hom_mk._proof_1.mpr {down := category_theory.under.hom_mk._proof_2.mpr {down := _}}) f w

@[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") :

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) :
(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₁} [category_theory.category T] {X : T} {f g : category_theory.under X} (hr : f.right g.right) :
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₁} [category_theory.category T] {X : T} {f g : category_theory.under X} (hr : f.right g.right) (hw : f.hom hr.hom = g.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) :

The forgetful functor mapping an arrow to its domain.

Equations
@[simp]

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

Equations
@[simp]

@[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} :

Mapping by the identity morphism is just the identity functor.

Equations

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

Equations

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_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₂) :
((category_theory.under.post F).map f).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