mathlib documentation

category_theory.subobject.comma

Subobjects in the category of structured arrows #

We compute the subobjects of an object A in the category structured_arrow S T for T : C ⥤ D and S : D as a subtype of the subobjects of A.right. We deduce that structured_arrow S T is well-powered if C is.

Main declarations #

Implementation notes #

Our computation requires that C has all limits and T preserves all limits. Furthermore, we require that the morphisms of C and D are in the same universe. It is possible that both of these requirements can be relaxed by refining the results about limits in comma categories.

We also provide the dual results. As usual, we use subobject (op A) for the quotient objects of A.

Every subobject of a structured arrow can be projected to a subobject of the underlying object.

Equations
@[simp]

A subobject of the underlying object of a structured arrow can be lifted to a subobject of the structured arrow, provided that there is a morphism making the subobject into a structured arrow.

Equations

If A : S → T.obj B is a structured arrow for S : D and T : C ⥤ D, then we can explicitly describe the subobjects of A as the subobjects P of B in C for which A.hom factors through the image of P under T.

Equations
@[protected, instance]

If C is well-powered and complete and T preserves limits, then structured_arrow S T is well-powered.

@[simp]

A quotient of the underlying object of a costructured arrow can be lifted to a quotient of the costructured arrow, provided that there is a morphism making the quotient into a costructured arrow.

Equations

If A : S.obj B ⟶ T is a costructured arrow for S : C ⥤ D and T : D, then we can explicitly describe the quotients of A as the quotients P of B in C for which A.hom factors through the image of P under S.

Equations
@[protected, instance]

If C is well-copowered and cocomplete and S preserves colimits, then costructured_arrow S T is well-copowered.