Rigid objects in a precategory

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2023-11-09.

module category-theory.rigid-objects-precategories where
Imports 
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

Idea

A rigid object in a precategory is an object whose automorphism group is trivial.

Definitions

The predicate of being rigid

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

  is-rigid-obj-prop-Precategory : Prop l2
  is-rigid-obj-prop-Precategory = is-contr-Prop (iso-Precategory C x x)

  is-rigid-obj-Precategory : UU l2
  is-rigid-obj-Precategory = type-Prop is-rigid-obj-prop-Precategory

  is-prop-is-rigid-obj-Precategory : is-prop is-rigid-obj-Precategory
  is-prop-is-rigid-obj-Precategory =
    is-prop-type-Prop is-rigid-obj-prop-Precategory

The type of rigid objects in a precategory

rigid-obj-Precategory : {l1 l2 : Level} (C : Precategory l1 l2) → UU (l1 ⊔ l2)
rigid-obj-Precategory C = Σ (obj-Precategory C) (is-rigid-obj-Precategory C)

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

  obj-rigid-obj-Precategory : rigid-obj-Precategory C → obj-Precategory C
  obj-rigid-obj-Precategory = pr1

  is-rigid-rigid-obj-Precategory :
    (x : rigid-obj-Precategory C) →
    is-rigid-obj-Precategory C (obj-rigid-obj-Precategory x)
  is-rigid-rigid-obj-Precategory = pr2

Recent changes