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.
Equations
Instances For
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
Instances For
To give a morphism in the over category, it suffices to give an arrow fitting in a commutative triangle.
Equations
Instances For
This is useful when homMk (· ≫ ·)
appears under Functor.map
or a natural equivalence.
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 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.
Equations
Instances For
If f
is an isomorphism, map f
is an equivalence of categories.
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
If f = g
, then map f
is naturally isomorphic to map g
.
Equations
- CategoryTheory.Over.mapCongr f g h = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Over X) => CategoryTheory.eqToIso ⋯) ⋯
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
The identity over X
is terminal.
Instances For
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
.
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
post (F ⋙ G)
is isomorphic (actually equal) to post F ⋙ post G
.
Equations
- CategoryTheory.Over.postComp F G = CategoryTheory.NatIso.ofComponents (fun (X_1 : CategoryTheory.Over X) => CategoryTheory.Iso.refl ((CategoryTheory.Over.post (F.comp G)).obj X_1)) ⋯
Instances For
A natural transformation F ⟶ G
induces a natural transformation on
Over X
up to Under.map
.
Equations
- CategoryTheory.Over.postMap e = { app := fun (Y : CategoryTheory.Over X) => CategoryTheory.Over.homMk (e.app Y.left) ⋯, naturality := ⋯ }
Instances For
If F
and G
are naturally isomorphic, then Over.post F
and Over.post G
are also naturally
isomorphic up to Over.map
Equations
- CategoryTheory.Over.postCongr e = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Over X) => CategoryTheory.Over.isoMk (e.app A.left) ⋯) ⋯
Instances For
If F
is fully faithful, then so is Over.post F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An equivalence of categories induces an equivalence on over categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If X : T
is terminal, then the over category of X
is equivalent to T
.
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
An equivalence F
induces an equivalence CostructuredArrow F X ≌ Over X
.
The under category has as objects arrows with domain X
and as morphisms commutative
triangles.
Equations
Instances For
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
This is useful when homMk (· ≫ ·)
appears under Functor.map
or a natural equivalence.
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
If f
is an isomorphism, map f
is an equivalence of categories.
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
If f = g
, then map f
is naturally isomorphic to map g
.
Equations
- CategoryTheory.Under.mapCongr f g h = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Under Y) => CategoryTheory.eqToIso ⋯) ⋯
Instances For
The functor defined by the under categories
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity under X
is initial.
Instances For
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
.
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
post (F ⋙ G)
is isomorphic (actually equal) to post F ⋙ post G
.
Equations
- CategoryTheory.Under.postComp F G = CategoryTheory.NatIso.ofComponents (fun (X_1 : CategoryTheory.Under X) => CategoryTheory.Iso.refl ((CategoryTheory.Under.post (F.comp G)).obj X_1)) ⋯
Instances For
A natural transformation F ⟶ G
induces a natural transformation on
Under X
up to Under.map
.
Equations
- CategoryTheory.Under.postMap e = { app := fun (Y : CategoryTheory.Under X) => CategoryTheory.Under.homMk (e.app Y.right) ⋯, naturality := ⋯ }
Instances For
If F
and G
are naturally isomorphic, then Under.post F
and Under.post G
are also
naturally isomorphic up to Under.map
Equations
- CategoryTheory.Under.postCongr e = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Under X) => CategoryTheory.Under.isoMk (e.app A.right) ⋯) ⋯
Instances For
If F
is fully faithful, then so is Under.post F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An equivalence of categories induces an equivalence on under categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If X : T
is initial, then the under category of X
is equivalent to T
.
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
An equivalence F
induces an equivalence StructuredArrow X F ≌ Under X
.
The essential image of Over.post F
where F
is full is the same as the essential image of
F
.
The essential image of Under.post F
where F
is full is the same as the essential image of
F
.
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 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
The functor used to define the equivalence ofCommaSndEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor used to define the equivalence ofCommaSndEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
There is a canonical equivalence between the structured arrow category with domain c
on
the functor Comma.fst F G : Comma F G ⥤ F
and the comma category over
Under.forget c ⋙ F : Under c ⥤ T
and G
.
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 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.
Instances For
The functor used to define the equivalence ofCommaFstEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor used to define the equivalence ofCommaFstEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
There is a canonical equivalence between the costructured arrow category with codomain c
on
the functor Comma.fst F G : Comma F G ⥤ F
and the comma category over
Over.forget c ⋙ F : Over c ⥤ T
and G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical equivalence between over and under categories by reversing structure arrows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical equivalence between under and over categories by reversing structure arrows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical functor by reversing structure arrows.
Instances For
The canonical functor by reversing structure arrows.
Instances For
The canonical functor by reversing structure arrows.
Instances For
The canonical functor by reversing structure arrows.