The category of "structured arrows" #
For T : C ⥤ D
, a T
-structured arrow with source S : D
is just a morphism S ⟶ T.obj Y
, for some Y : C
.
These form a category with morphisms g : Y ⟶ Y'
making the obvious diagram commute.
We prove that 𝟙 (T.obj Y)
is the initial object in T
-structured objects with source T.obj Y
.
The category of T
-structured arrows with domain S : D
(here T : C ⥤ D
),
has as its objects D
-morphisms of the form S ⟶ T Y
, for some Y : C
,
and morphisms C
-morphisms Y ⟶ Y'
making the obvious triangle commute.
Equations
Instances For
Equations
- CategoryTheory.instCategoryStructuredArrow S T = CategoryTheory.commaCategory
The obvious projection functor from structured arrows.
Equations
Instances For
Construct a structured arrow from a morphism.
Equations
- CategoryTheory.StructuredArrow.mk f = { left := { as := PUnit.unit }, right := Y, hom := f }
Instances For
To construct a morphism of structured arrows, we need a morphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- CategoryTheory.StructuredArrow.homMk g w = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }
Instances For
Given a structured arrow X ⟶ T(Y)
, and an arrow Y ⟶ Y'
, we can construct a morphism of
structured arrows given by (X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y'))
.
Equations
- f.homMk' g = { left := CategoryTheory.CategoryStruct.id f.left, right := g, w := ⋯ }
Instances For
Variant of homMk'
where both objects are applications of mk
.
Equations
- CategoryTheory.StructuredArrow.mkPostcomp f g = { left := CategoryTheory.CategoryStruct.id (CategoryTheory.StructuredArrow.mk f).left, right := g, w := ⋯ }
Instances For
To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes.
Equations
Instances For
Equations
- ⋯ = ⋯
The converse of this is true with additional assumptions, see mono_iff_mono_right
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Eta rule for structured arrows. Prefer StructuredArrow.eta
for rewriting, since equality of
objects tends to cause problems.
Eta rule for structured arrows.
Equations
- f.eta = CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl f.right) ⋯
Instances For
A morphism between source objects S ⟶ S'
contravariantly induces a functor between structured arrows,
StructuredArrow S' T ⥤ StructuredArrow S T
.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat
.
Equations
Instances For
An isomorphism S ≅ S'
induces an equivalence StructuredArrow S T ≌ StructuredArrow S' T
.
Equations
Instances For
A natural isomorphism T ≅ T'
induces an equivalence
StructuredArrow S T ≌ StructuredArrow S T'
.
Equations
Instances For
Equations
- ⋯ = ⋯
The identity structured arrow is initial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor (S, F ⋙ G) ⥤ (S, G)
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If F
is an equivalence, then so is the functor (S, F ⋙ G) ⥤ (S, G)
.
Equations
- ⋯ = ⋯
The functor (S, F) ⥤ (G(S), F ⋙ G)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If G
is fully faithful, then post S F G : (S, F) ⥤ (G(S), F ⋙ G)
is an equivalence.
Equations
- ⋯ = ⋯
The functor StructuredArrow L R ⥤ StructuredArrow L' R'
that is deduced from
a natural transformation R ⋙ G ⟶ F ⋙ R'
and a morphism L' ⟶ G.obj L.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A structured arrow is called universal if it is initial.
Equations
- f.IsUniversal = CategoryTheory.Limits.IsInitial f
Instances For
The family of morphisms out of a universal arrow.
Equations
- h.desc g = (CategoryTheory.Limits.IsInitial.to h g).right
Instances For
Any structured arrow factors through a universal arrow.
Two morphisms out of a universal T
-structured arrow are equal if their image under T
are
equal after precomposing the universal arrow.
The category of S
-costructured arrows with target T : D
(here S : C ⥤ D
),
has as its objects D
-morphisms of the form S Y ⟶ T
, for some Y : C
,
and morphisms C
-morphisms Y ⟶ Y'
making the obvious triangle commute.
Equations
Instances For
Equations
- CategoryTheory.instCategoryCostructuredArrow S T = CategoryTheory.commaCategory
The obvious projection functor from costructured arrows.
Equations
Instances For
Construct a costructured arrow from a morphism.
Equations
- CategoryTheory.CostructuredArrow.mk f = { left := Y, right := { as := PUnit.unit }, hom := f }
Instances For
To construct a morphism of costructured arrows, we need a morphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- CategoryTheory.CostructuredArrow.homMk g w = { left := g, right := CategoryTheory.CategoryStruct.id f.right, w := ⋯ }
Instances For
Given a costructured arrow S(Y) ⟶ X
, and an arrow Y' ⟶ Y'
, we can construct a morphism of
costructured arrows given by (S(Y) ⟶ X) ⟶ (S(Y') ⟶ S(Y) ⟶ X)
.
Equations
- f.homMk' g = { left := g, right := CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right, w := ⋯ }
Instances For
Variant of homMk'
where both objects are applications of mk
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, and to check that the triangle commutes.
Equations
Instances For
Equations
- ⋯ = ⋯
The converse of this is true with additional assumptions, see epi_iff_epi_left
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Eta rule for costructured arrows. Prefer CostructuredArrow.eta
for rewriting, as equality of
objects tends to cause problems.
Eta rule for costructured arrows.
Equations
- f.eta = CategoryTheory.CostructuredArrow.isoMk (CategoryTheory.Iso.refl f.left) ⋯
Instances For
A morphism between target objects T ⟶ T'
covariantly induces a functor between costructured arrows,
CostructuredArrow S T ⥤ CostructuredArrow S T'
.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat
.
Equations
Instances For
An isomorphism T ≅ T'
induces an equivalence
CostructuredArrow S T ≌ CostructuredArrow S T'
.
Equations
Instances For
A natural isomorphism S ≅ S'
induces an equivalence
CostrucutredArrow S T ≌ CostructuredArrow S' T
.
Equations
Instances For
Equations
- ⋯ = ⋯
The identity costructured arrow is terminal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor (F ⋙ G, S) ⥤ (G, S)
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If F
is an equivalence, then so is the functor (F ⋙ G, S) ⥤ (G, S)
.
Equations
- ⋯ = ⋯
The functor (F, S) ⥤ (F ⋙ G, G(S))
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If G
is fully faithful, then post F G S : (F, S) ⥤ (F ⋙ G, G(S))
is an equivalence.
Equations
- ⋯ = ⋯
The functor CostructuredArrow S T ⥤ CostructuredArrow U V
that is deduced from
a natural transformation F ⋙ U ⟶ S ⋙ G
and a morphism G.obj T ⟶ V
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A costructured arrow is called universal if it is terminal.
Equations
- f.IsUniversal = CategoryTheory.Limits.IsTerminal f
Instances For
The family of morphisms into a universal arrow.
Equations
- h.lift g = (CategoryTheory.Limits.IsTerminal.from h g).left
Instances For
Any costructured arrow factors through a universal arrow.
Two morphisms into a universal S
-costructured arrow are equal if their image under S
are
equal after postcomposing the universal arrow.
Given X : D
and F : C ⥤ D
, to upgrade a functor G : E ⥤ C
to a functor
E ⥤ StructuredArrow X F
, it suffices to provide maps X ⟶ F.obj (G.obj Y)
for all Y
making
the obvious triangles involving all F.map (G.map g)
commute.
This is of course the same as providing a cone over F ⋙ G
with cone point X
, see
Functor.toStructuredArrowIsoToStructuredArrow
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Upgrading a functor E ⥤ C
to a functor E ⥤ StructuredArrow X F
and composing with the
forgetful functor StructuredArrow X F ⥤ C
recovers the original functor.
Equations
- G.toStructuredArrowCompProj X F f h = CategoryTheory.Iso.refl ((G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F))
Instances For
Given F : C ⥤ D
and X : D
, to upgrade a functor G : E ⥤ C
to a functor
E ⥤ CostructuredArrow F X
, it suffices to provide maps F.obj (G.obj Y) ⟶ X
for all Y
making the obvious triangles involving all F.map (G.map g)
commute.
This is of course the same as providing a cocone over F ⋙ G
with cocone point X
, see
Functor.toCostructuredArrowIsoToCostructuredArrow
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Upgrading a functor E ⥤ C
to a functor E ⥤ CostructuredArrow F X
and composing with the
forgetful functor CostructuredArrow F X ⥤ C
recovers the original functor.
Equations
- G.toCostructuredArrowCompProj F X f h = CategoryTheory.Iso.refl ((G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X))
Instances For
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of structured arrows d ⟶ F.obj c
to the category of costructured arrows
F.op.obj c ⟶ (op d)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of structured arrows op d ⟶ F.op.obj c
to the category of costructured arrows
F.obj c ⟶ d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of costructured arrows F.obj c ⟶ d
to the category of structured arrows
op d ⟶ F.op.obj c
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor F : C ⥤ D
and an object d : D
, we obtain a contravariant functor from the
category of costructured arrows F.op.obj c ⟶ op d
to the category of structured arrows
d ⟶ F.obj c
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor F : C ⥤ D
and an object d : D
, the category of structured arrows d ⟶ F.obj c
is contravariantly equivalent to the category of costructured arrows F.op.obj c ⟶ op d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a functor F : C ⥤ D
and an object d : D
, the category of costructured arrows
F.obj c ⟶ d
is contravariantly equivalent to the category of structured arrows
op d ⟶ F.op.obj c
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor establishing the equivalence StructuredArrow.preEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse functor establishing the equivalence StructuredArrow.preEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A structured arrow category on a StructuredArrow.pre e F G
functor is equivalent to the
structured arrow category on F
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor establishing the equivalence CostructuredArrow.preEquivalence
.
Equations
- One or more equations did not get rendered due to their size.