Over and under categories #
Over (and under) categories are special cases of comma categories.
- If
L
is the identity functor andR
is a constant functor, thenComma L R
is the "slice" or "over" category over the objectR
maps to. - Conversely, if
L
is a constant functor andR
is the identity functor, thenComma L R
is the "coslice" or "under" category under the objectL
maps to.
Tags #
Comma, Slice, Coslice, Over, Under
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
Equations
- CategoryTheory.instCategoryOver X = CategoryTheory.commaCategory
Equations
- CategoryTheory.Over.inhabited = { default := { left := default, right := default, hom := CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id T).obj default) } }
To give an object in the over category, it suffices to give a morphism with codomain X
.
Equations
Instances For
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
- CategoryTheory.Over.coeFromHom = { coe := CategoryTheory.Over.mk }
Instances For
To give a morphism in the over category, it suffices to give an arrow fitting in a commutative triangle.
Equations
Instances For
Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.
Equations
Instances For
The forgetful functor mapping an arrow to its domain.
See https://stacks.math.columbia.edu/tag/001G.
Equations
Instances For
The natural cocone over the forgetful functor Over X ⥤ T
with cocone point X
.
Equations
- CategoryTheory.Over.forgetCocone X = { pt := X, ι := { app := CategoryTheory.Comma.hom, naturality := ⋯ } }
Instances For
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
Instances For
This section proves various equalities between functors that
demonstrate, for instance, that over categories assemble into a
functor mapFunctor : T ⥤ Cat
.
These equalities between functors are then converted to natural
isomorphisms using eqToIso
. Such natural isomorphisms could be
obtained directly using Iso.refl
but this method will have
better computational properties, when used, for instance, in
developing the theory of Beck-Chevalley transformations.
Mapping by the identity morphism is just the identity functor.
The natural isomorphism arising from mapForget_eq
.
Equations
Instances For
Mapping by f
and then forgetting is the same as forgetting.
The natural isomorphism arising from mapForget_eq
.
Equations
Instances For
Mapping by the composite morphism f ≫ g
is the same as mapping by f
then by g
.
The natural isomorphism arising from mapComp_eq
.
Equations
Instances For
The functor defined by the over categories.
Equations
- CategoryTheory.Over.mapFunctor T = { obj := fun (X : T) => CategoryTheory.Cat.of (CategoryTheory.Over X), map := fun {X Y : T} => CategoryTheory.Over.map, map_id := ⋯, map_comp := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The identity over X
is terminal.
Equations
- CategoryTheory.Over.mkIdTerminal = CategoryTheory.CostructuredArrow.mkIdTerminal
Instances For
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
CategoryTheory.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 CategoryTheory.Over.mono_left_of_mono
.
This lemma is not an instance, to avoid loops in type class inference.
If k
is a monomorphism, then k.left
is a monomorphism. In other words, Over.forget X
preserves
monomorphisms.
The converse of CategoryTheory.Over.mono_of_mono_left
.
Equations
- ⋯ = ⋯
Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor F : T ⥤ D
induces a functor Over X ⥤ Over (F.obj X)
in the obvious way.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reinterpreting an F
-costructured arrow F.obj d ⟶ X
as an arrow over X
induces a functor
CostructuredArrow F X ⥤ Over X
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An equivalence F
induces an equivalence CostructuredArrow F X ≌ Over X
.
Equations
- ⋯ = ⋯
The under category has as objects arrows with domain X
and as morphisms commutative
triangles.
Equations
Instances For
Equations
- CategoryTheory.instCategoryUnder X = CategoryTheory.commaCategory
Equations
- One or more equations did not get rendered due to their size.
To give an object in the under category, it suffices to give an arrow with domain X
.
Equations
Instances For
To give a morphism in the under category, it suffices to give a morphism fitting in a commutative triangle.
Equations
Instances For
Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.
Equations
Instances For
The forgetful functor mapping an arrow to its domain.
Equations
Instances For
The natural cone over the forgetful functor Under X ⥤ T
with cone point X
.
Equations
- CategoryTheory.Under.forgetCone X = { pt := X, π := { app := CategoryTheory.Comma.hom, naturality := ⋯ } }
Instances For
A morphism X ⟶ Y
induces a functor Under Y ⥤ Under X
in the obvious way.
Equations
Instances For
This section proves various equalities between functors that
demonstrate, for instance, that under categories assemble into a
functor mapFunctor : Tᵒᵖ ⥤ Cat
.
Mapping by the identity morphism is just the identity functor.
Mapping by the identity morphism is just the identity functor.
Equations
Instances For
Mapping by f
and then forgetting is the same as forgetting.
The natural isomorphism arising from mapForget_eq
.
Equations
Instances For
Mapping by the composite morphism f ≫ g
is the same as mapping by f
then by g
.
The natural isomorphism arising from mapComp_eq
.
Equations
Instances For
The functor defined by the under categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The identity under X
is initial.
Equations
- CategoryTheory.Under.mkIdInitial = CategoryTheory.StructuredArrow.mkIdInitial
Instances For
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
CategoryTheory.Under.mono_right_of_mono
.
If k.right
is an epimorphism, then k
is an epimorphism. In other words, Under.forget X
reflects epimorphisms.
The converse of CategoryTheory.Under.epi_right_of_epi
.
This lemma is not an instance, to avoid loops in type class inference.
If k
is an epimorphism, then k.right
is an epimorphism. In other words, Under.forget X
preserves epimorphisms.
The converse of CategoryTheory.under.epi_of_epi_right
.
Equations
- ⋯ = ⋯
A functor F : T ⥤ D
induces a functor Under X ⥤ Under (F.obj X)
in the obvious way.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reinterpreting an F
-structured arrow X ⟶ F.obj d
as an arrow under X
induces a functor
StructuredArrow X F ⥤ Under X
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An equivalence F
induces an equivalence StructuredArrow X F ≌ Under X
.
Equations
- ⋯ = ⋯
Given X : T
, to upgrade a functor F : S ⥤ T
to a functor S ⥤ Over X
, it suffices to
provide maps F.obj Y ⟶ X
for all Y
making the obvious triangles involving all F.map g
commute.
Equations
- F.toOver X f h = F.toCostructuredArrow (CategoryTheory.Functor.id T) X f ⋯
Instances For
Upgrading a functor S ⥤ T
to a functor S ⥤ Over X
and composing with the forgetful functor
Over X ⥤ T
recovers the original functor.
Equations
- F.toOverCompForget X f h = CategoryTheory.Iso.refl ((F.toOver X f ⋯).comp (CategoryTheory.Over.forget X))
Instances For
Given X : T
, to upgrade a functor F : S ⥤ T
to a functor S ⥤ Under X
, it suffices to
provide maps X ⟶ F.obj Y
for all Y
making the obvious triangles involving all F.map g
commute.
Equations
- F.toUnder X f h = F.toStructuredArrow X (CategoryTheory.Functor.id T) f ⋯
Instances For
Upgrading a functor S ⥤ T
to a functor S ⥤ Under X
and composing with the forgetful functor
Under X ⥤ T
recovers the original functor.
Equations
- F.toUnderCompForget X f h = CategoryTheory.Iso.refl ((F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X))
Instances For
A functor from the structured arrow category on the projection functor for any structured arrow category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor of ofStructuredArrowProjEquivalence.functor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterization of the structured arrow category on the projection functor of any structured arrow category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical functor from the structured arrow category on the diagonal functor
T ⥤ T × T
to the the structured arrow category on Under.forget
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor of ofDiagEquivalence.functor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterization of the structured arrow category on the diagonal functor T ⥤ T × T
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of StructuredArrow.ofDiagEquivalence
with the roles of the first and second
projection swapped.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor from the costructured arrow category on the projection functor for any costructured arrow category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor of ofCostructuredArrowProjEquivalence.functor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterization of the costructured arrow category on the projection functor of any costructured arrow category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical functor from the costructured arrow category on the diagonal functor
T ⥤ T × T
to the the costructured arrow category on Under.forget
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor of ofDiagEquivalence.functor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterization of the costructured arrow category on the diagonal functor T ⥤ T × T
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of CostructuredArrow.ofDiagEquivalence
with the roles of the first and second
projection swapped.
Equations
- One or more equations did not get rendered due to their size.