Pointed endofunctors

Content created by Egbert Rijke.

Created on 2024-02-08.
Last modified on 2024-02-08.

module category-theory.pointed-endofunctors-precategories where
Imports 
open import category-theory.functors-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

Idea

An endofunctor F : C → C on a precategory C is said to be pointed if it comes equipped with a natural transformation id ⇒ F from the identity functor to F.

More explicitly, a pointing of an endofunctor F : C → C consists of a family of morphisms η X : X → F X such that for each morphism f : X → Y in C the diagram

       η X
    X -----> F X
    |         |
  f |         | F f
    ∨         ∨
    Y -----> F Y
       η Y

commutes.

Definitions

The structure of a pointing on an endofunctor on a precategory

module _
  {l1 l2 : Level} (C : Precategory l1 l2) (T : functor-Precategory C C)
  where

  pointing-endofunctor-Precategory : UU (l1 ⊔ l2)
  pointing-endofunctor-Precategory =
    natural-transformation-Precategory C C (id-functor-Precategory C) T

Pointed endofunctors on a precategory

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  where

  pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
  pointed-endofunctor-Precategory =
    Σ (functor-Precategory C C) (pointing-endofunctor-Precategory C)

  module _
    (F : pointed-endofunctor-Precategory)
    where

    functor-pointed-endofunctor-Precategory :
      functor-Precategory C C
    functor-pointed-endofunctor-Precategory =
      pr1 F

    obj-pointed-endofunctor-Precategory : obj-Precategory C → obj-Precategory C
    obj-pointed-endofunctor-Precategory =
      obj-functor-Precategory C C functor-pointed-endofunctor-Precategory

    hom-pointed-endofunctor-Precategory :
      {X Y : obj-Precategory C} →
      hom-Precategory C X Y →
      hom-Precategory C
        ( obj-pointed-endofunctor-Precategory X)
        ( obj-pointed-endofunctor-Precategory Y)
    hom-pointed-endofunctor-Precategory =
      hom-functor-Precategory C C functor-pointed-endofunctor-Precategory

    preserves-id-pointed-endofunctor-Precategory :
      (X : obj-Precategory C) →
      hom-pointed-endofunctor-Precategory (id-hom-Precategory C {X}) ＝
      id-hom-Precategory C
    preserves-id-pointed-endofunctor-Precategory =
      preserves-id-functor-Precategory C C
        ( functor-pointed-endofunctor-Precategory)

    preserves-comp-pointed-endofunctor-Precategory :
      {X Y Z : obj-Precategory C}
      (g : hom-Precategory C Y Z) (f : hom-Precategory C X Y) →
      hom-pointed-endofunctor-Precategory
        ( comp-hom-Precategory C g f) ＝
      comp-hom-Precategory C
        ( hom-pointed-endofunctor-Precategory g)
        ( hom-pointed-endofunctor-Precategory f)
    preserves-comp-pointed-endofunctor-Precategory =
      preserves-comp-functor-Precategory C C
        ( functor-pointed-endofunctor-Precategory)

    pointing-pointed-endofunctor-Precategory :
      natural-transformation-Precategory C C
        ( id-functor-Precategory C)
        ( functor-pointed-endofunctor-Precategory)
    pointing-pointed-endofunctor-Precategory = pr2 F

    hom-family-pointing-pointed-endofunctor-Precategory :
      hom-family-functor-Precategory C C
        ( id-functor-Precategory C)
        ( functor-pointed-endofunctor-Precategory)
    hom-family-pointing-pointed-endofunctor-Precategory =
      hom-family-natural-transformation-Precategory C C
        ( id-functor-Precategory C)
        ( functor-pointed-endofunctor-Precategory)
        ( pointing-pointed-endofunctor-Precategory)

    naturality-pointing-pointed-endofunctor-Precategory :
      is-natural-transformation-Precategory C C
        ( id-functor-Precategory C)
        ( functor-pointed-endofunctor-Precategory)
        ( hom-family-pointing-pointed-endofunctor-Precategory)
    naturality-pointing-pointed-endofunctor-Precategory =
      naturality-natural-transformation-Precategory C C
        ( id-functor-Precategory C)
        ( functor-pointed-endofunctor-Precategory)
        ( pointing-pointed-endofunctor-Precategory)

Recent changes