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

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
@[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 = {as := punit.star}
@[simp]
@[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} (f' : (category_theory.functor.from_punit X).obj B.right X') :
f.left B.hom f' = A.hom f'
@[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} (f : Y X) :

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) (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₁} [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 = category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1
@[simp]
@[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
@[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) (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

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

Equations

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

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.

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]

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.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₂) :

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] (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
@[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 = {as := punit.star}
@[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_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'
@[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]

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 = category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1
@[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) (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₁} [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
@[simp]
@[simp]

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

Equations

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

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

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.

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]

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.

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₁} [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₂) :