covariant hom functor

Stream: Is there code for X?

[Luca Happel]

I would like to define an object property to check if an object of a category is a connected object. Currently, I have this code:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.ObjectProperty.Basic
import Mathlib.CategoryTheory.Limits.Preserves.Basic
import Mathlib.CategoryTheory.Functor.Hom
import Mathlib.CategoryTheory.Functor.Currying
import Mathlib.CategoryTheory.Extensive
import Mathlib.Data.Opposite

open CategoryTheory

universe u

variable {C : Type*}
  [Category C]
  [FinitaryExtensive C]

def hom_functor (X: C) : C ⥤ Type* :=
  let hom' := curryObj $ CategoryTheory.Functor.hom C
  hom'.obj (Opposite.op X)

/-- Predicate to check if an object $X$ is a Z-Object as described by
    Rudolf E. Hoffmann:
    $$
    \Hom[\mathsf{C}]{X}{\cdot} \text{ preserves colimits}
    $$
-/
def is_zobj : CategoryTheory.ObjectProperty C := λ X ↦
  Limits.PreservesColimits (hom_functor  X)

I have based this code on this definition: https://ncatlab.org/nlab/show/connected+object

I am unsure if this is the correct way to define the covariant Hom functor, or if I should do it some other way. I would suppose that mathlib would already have the covariant Hom functor defined somewhere, but I could only find the Hom bifunctor in Mathlib.CategoryTheory.Functor.Hom.
Sorry if this is a stupid question. This is my first post here.

[Robin Carlier]

This is docs#CategoryTheory.coyoneda.

[Robin Carlier]

Also, note that your definition of "Z-object" is incorrect (currently it states that the hom-functor preserves all small colimits, edit:  I think these are called atomic objects), we apparently don’t have a general PreservesCoproducts typeclass, but you can see how it’s stated in file#Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products. it’s something like ∀ {J : Type u} (f : J → C), PreservesColimit (Discrete.functor f) (coyoneda.obj (op X))

[Luca Happel]

If I were to use your suggestion:

universe u

variable {C : Type u}
  [Category C]
  [FinitaryExtensive C]

def is_zobj : ObjectProperty C := λ X ↦
  ∀ {J : Type} (f : J → C),
  Limits.PreservesColimit
    (Discrete.functor f)
    (coyoneda.obj (Opposite.op X))

Wouldn't that mean I would only consider small colimits, because Type = Type 0? If I were to use this:

def is_zobj : ObjectProperty C := λ X ↦
  ∀ {J : Type u} (f : J → C),
  Limits.PreservesColimit
    (Discrete.functor f)
    (coyoneda.obj (Opposite.op X))

where I have changed J to be of Type Type u, would that mean I also allow large colimits?

[Robin Carlier]

The former states that you preserve all "0-small" coproducts, the second that you preserve all u-small coproducts, objects of Type u are never u-large. I think the definition you want to go for really depends on C. Currently when you write [Category C], you do not specify any universe level in which the morphisms of C live, this is why the pattern you usually see in Mathlib is either

variable {C : Type*} [Category C]

in which case nothing is said about universes,
or

universe v u
variable {C : Type u} [Category.{v} C]

in which you specify the size of the type of objects of C to be u-small and the type of morphisms between two objects to be v-small

I’ve never thought about the right size constraints for connected objects in the case where the two universe levels are different, but when C is u-small (i.e {C : Type u} [Category.{u} C], which has an abbrev {C : Type u} [SmallCategory C]), you probably want u-small coproducts. In this situation when people say "small coproducts" they usually mean coproduct of size not exceeding the size of C, so u-small coproducts really.

[Robin Carlier]

Wait no, I’m confused, and probably meant that when C is locally u-small, you want u-small coproducts (even though when C itself is u-small, the preservation of coproduct hyp will simply be empty for coproducts that don’t exist in C, but I’m not sure it’s what you want). Sorry for this... In any case I think for statement involving preservation of colimits like this you want to specify universe levels for C and its hom-types.