Functors between precategories
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.
Created on 2022-03-11.
Last modified on 2023-09-27.
module category-theory.functors-precategories where
Imports
open import category-theory.isomorphisms-in-precategories open import category-theory.maps-precategories open import category-theory.precategories open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.subtypes open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels
Idea
A functor from a precategory C
to a
precategory D
consists of:
- a map
F₀ : C → D
on objects, - a map
F₁ : hom x y → hom (F₀ x) (F₀ y)
on morphisms, such that the following identities hold: F₁ id_x = id_(F₀ x)
,F₁ (g ∘ f) = F₁ g ∘ F₁ f
.
Definition
The predicate of being a functor on maps between precategories
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F : map-Precategory C D) where preserves-comp-hom-map-Precategory : UU (l1 ⊔ l2 ⊔ l4) preserves-comp-hom-map-Precategory = {x y z : obj-Precategory C} (g : hom-Precategory C y z) (f : hom-Precategory C x y) → ( hom-map-Precategory C D F (comp-hom-Precategory C g f)) = ( comp-hom-Precategory D ( hom-map-Precategory C D F g) ( hom-map-Precategory C D F f)) preserves-id-hom-map-Precategory : UU (l1 ⊔ l4) preserves-id-hom-map-Precategory = (x : obj-Precategory C) → ( hom-map-Precategory C D F (id-hom-Precategory C {x})) = ( id-hom-Precategory D {obj-map-Precategory C D F x}) is-functor-map-Precategory : UU (l1 ⊔ l2 ⊔ l4) is-functor-map-Precategory = preserves-comp-hom-map-Precategory × preserves-id-hom-map-Precategory preserves-comp-is-functor-map-Precategory : is-functor-map-Precategory → preserves-comp-hom-map-Precategory preserves-comp-is-functor-map-Precategory = pr1 preserves-id-is-functor-map-Precategory : is-functor-map-Precategory → preserves-id-hom-map-Precategory preserves-id-is-functor-map-Precategory = pr2
functors between precategories
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where functor-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) functor-Precategory = Σ ( obj-Precategory C → obj-Precategory D) ( λ F₀ → Σ ( {x y : obj-Precategory C} (f : hom-Precategory C x y) → hom-Precategory D (F₀ x) (F₀ y)) ( λ F₁ → is-functor-map-Precategory C D (F₀ , F₁))) obj-functor-Precategory : functor-Precategory → obj-Precategory C → obj-Precategory D obj-functor-Precategory = pr1 hom-functor-Precategory : (F : functor-Precategory) → {x y : obj-Precategory C} → (f : hom-Precategory C x y) → hom-Precategory D ( obj-functor-Precategory F x) ( obj-functor-Precategory F y) hom-functor-Precategory F = pr1 (pr2 F) map-functor-Precategory : functor-Precategory → map-Precategory C D pr1 (map-functor-Precategory F) = obj-functor-Precategory F pr2 (map-functor-Precategory F) = hom-functor-Precategory F is-functor-functor-Precategory : (F : functor-Precategory) → is-functor-map-Precategory C D (map-functor-Precategory F) is-functor-functor-Precategory = pr2 ∘ pr2 preserves-comp-functor-Precategory : (F : functor-Precategory) {x y z : obj-Precategory C} (g : hom-Precategory C y z) (f : hom-Precategory C x y) → ( hom-functor-Precategory F (comp-hom-Precategory C g f)) = ( comp-hom-Precategory D ( hom-functor-Precategory F g) ( hom-functor-Precategory F f)) preserves-comp-functor-Precategory F = preserves-comp-is-functor-map-Precategory C D ( map-functor-Precategory F) ( is-functor-functor-Precategory F) preserves-id-functor-Precategory : (F : functor-Precategory) (x : obj-Precategory C) → ( hom-functor-Precategory F (id-hom-Precategory C {x})) = ( id-hom-Precategory D {obj-functor-Precategory F x}) preserves-id-functor-Precategory F = preserves-id-is-functor-map-Precategory C D ( map-functor-Precategory F) ( is-functor-functor-Precategory F)
Examples
The identity functor
There is an identity functor on any precategory.
id-functor-Precategory : {l1 l2 : Level} (C : Precategory l1 l2) → functor-Precategory C C pr1 (id-functor-Precategory C) = id pr1 (pr2 (id-functor-Precategory C)) = id pr1 (pr2 (pr2 (id-functor-Precategory C))) g f = refl pr2 (pr2 (pr2 (id-functor-Precategory C))) x = refl
Composition of functors
Any two compatible functors can be composed to a new functor.
comp-functor-Precategory : {l1 l2 l3 l4 l5 l6 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (E : Precategory l5 l6) → functor-Precategory D E → functor-Precategory C D → functor-Precategory C E pr1 (comp-functor-Precategory C D E G F) = obj-functor-Precategory D E G ∘ obj-functor-Precategory C D F pr1 (pr2 (comp-functor-Precategory C D E G F)) = hom-functor-Precategory D E G ∘ hom-functor-Precategory C D F pr1 (pr2 (pr2 (comp-functor-Precategory C D E G F))) g f = ( ap ( hom-functor-Precategory D E G) ( preserves-comp-functor-Precategory C D F g f)) ∙ ( preserves-comp-functor-Precategory D E G ( hom-functor-Precategory C D F g) ( hom-functor-Precategory C D F f)) pr2 (pr2 (pr2 (comp-functor-Precategory C D E G F))) x = ( ap ( hom-functor-Precategory D E G) ( preserves-id-functor-Precategory C D F x)) ∙ ( preserves-id-functor-Precategory D E G ( obj-functor-Precategory C D F x))
Properties
Respecting identities and compositions are propositions
This follows from the fact that the hom-types are sets.
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F : map-Precategory C D) where is-prop-preserves-comp-hom-map-Precategory : is-prop (preserves-comp-hom-map-Precategory C D F) is-prop-preserves-comp-hom-map-Precategory = is-prop-Π' ( λ x → is-prop-Π' ( λ y → is-prop-Π' ( λ z → is-prop-Π² ( λ g f → is-set-hom-Precategory D ( obj-map-Precategory C D F x) ( obj-map-Precategory C D F z) ( hom-map-Precategory C D F ( comp-hom-Precategory C g f)) ( comp-hom-Precategory D ( hom-map-Precategory C D F g) ( hom-map-Precategory C D F f)))))) preserves-comp-hom-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4) pr1 preserves-comp-hom-prop-map-Precategory = preserves-comp-hom-map-Precategory C D F pr2 preserves-comp-hom-prop-map-Precategory = is-prop-preserves-comp-hom-map-Precategory is-prop-preserves-id-hom-map-Precategory : is-prop (preserves-id-hom-map-Precategory C D F) is-prop-preserves-id-hom-map-Precategory = is-prop-Π ( λ x → is-set-hom-Precategory D ( obj-map-Precategory C D F x) ( obj-map-Precategory C D F x) ( hom-map-Precategory C D F (id-hom-Precategory C {x})) ( id-hom-Precategory D {obj-map-Precategory C D F x})) preserves-id-hom-prop-map-Precategory : Prop (l1 ⊔ l4) pr1 preserves-id-hom-prop-map-Precategory = preserves-id-hom-map-Precategory C D F pr2 preserves-id-hom-prop-map-Precategory = is-prop-preserves-id-hom-map-Precategory is-prop-is-functor-map-Precategory : is-prop (is-functor-map-Precategory C D F) is-prop-is-functor-map-Precategory = is-prop-prod ( is-prop-preserves-comp-hom-map-Precategory) ( is-prop-preserves-id-hom-map-Precategory) is-functor-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4) pr1 is-functor-prop-map-Precategory = is-functor-map-Precategory C D F pr2 is-functor-prop-map-Precategory = is-prop-is-functor-map-Precategory
Extensionality of functors between precategories
Equality of functors is equality of underlying maps
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where equiv-eq-map-eq-functor-Precategory : (F = G) ≃ (map-functor-Precategory C D F = map-functor-Precategory C D G) equiv-eq-map-eq-functor-Precategory = equiv-ap-emb ( comp-emb ( emb-subtype (is-functor-prop-map-Precategory C D)) ( emb-equiv ( inv-associative-Σ ( obj-Precategory C → obj-Precategory D) ( λ F₀ → { x y : obj-Precategory C} → hom-Precategory C x y → hom-Precategory D (F₀ x) (F₀ y)) ( pr1 ∘ is-functor-prop-map-Precategory C D)))) eq-map-eq-functor-Precategory : (F = G) → (map-functor-Precategory C D F = map-functor-Precategory C D G) eq-map-eq-functor-Precategory = map-equiv equiv-eq-map-eq-functor-Precategory eq-eq-map-functor-Precategory : (map-functor-Precategory C D F = map-functor-Precategory C D G) → (F = G) eq-eq-map-functor-Precategory = map-inv-equiv equiv-eq-map-eq-functor-Precategory is-section-eq-eq-map-functor-Precategory : eq-map-eq-functor-Precategory ∘ eq-eq-map-functor-Precategory ~ id is-section-eq-eq-map-functor-Precategory = is-section-map-inv-equiv equiv-eq-map-eq-functor-Precategory is-retraction-eq-eq-map-functor-Precategory : eq-eq-map-functor-Precategory ∘ eq-map-eq-functor-Precategory ~ id is-retraction-eq-eq-map-functor-Precategory = is-retraction-map-inv-equiv equiv-eq-map-eq-functor-Precategory
Equality of functors is homotopy of underlying maps
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where htpy-functor-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-functor-Precategory = htpy-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) equiv-htpy-eq-functor-Precategory : (F = G) ≃ htpy-functor-Precategory equiv-htpy-eq-functor-Precategory = ( equiv-htpy-eq-map-Precategory C D) ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) ∘e ( equiv-eq-map-eq-functor-Precategory C D F G) htpy-eq-functor-Precategory : F = G → htpy-functor-Precategory htpy-eq-functor-Precategory = map-equiv equiv-htpy-eq-functor-Precategory eq-htpy-functor-Precategory : htpy-functor-Precategory → F = G eq-htpy-functor-Precategory = map-inv-equiv equiv-htpy-eq-functor-Precategory is-section-eq-htpy-functor-Precategory : htpy-eq-functor-Precategory ∘ eq-htpy-functor-Precategory ~ id is-section-eq-htpy-functor-Precategory = is-section-map-inv-equiv equiv-htpy-eq-functor-Precategory is-retraction-eq-htpy-functor-Precategory : eq-htpy-functor-Precategory ∘ htpy-eq-functor-Precategory ~ id is-retraction-eq-htpy-functor-Precategory = is-retraction-map-inv-equiv equiv-htpy-eq-functor-Precategory
Functors preserve isomorphisms
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F : functor-Precategory C D) {x y : obj-Precategory C} where preserves-is-iso-functor-Precategory : (f : hom-Precategory C x y) → is-iso-Precategory C f → is-iso-Precategory D (hom-functor-Precategory C D F f) pr1 (preserves-is-iso-functor-Precategory f is-iso-f) = hom-functor-Precategory C D F (hom-inv-is-iso-Precategory C is-iso-f) pr1 (pr2 (preserves-is-iso-functor-Precategory f is-iso-f)) = ( inv ( preserves-comp-functor-Precategory C D F ( f) ( hom-inv-is-iso-Precategory C is-iso-f))) ∙ ( ap ( hom-functor-Precategory C D F) ( is-section-hom-inv-is-iso-Precategory C is-iso-f)) ∙ ( preserves-id-functor-Precategory C D F y) pr2 (pr2 (preserves-is-iso-functor-Precategory f is-iso-f)) = ( inv ( preserves-comp-functor-Precategory C D F ( hom-inv-is-iso-Precategory C is-iso-f) ( f))) ∙ ( ap ( hom-functor-Precategory C D F) ( is-retraction-hom-inv-is-iso-Precategory C is-iso-f)) ∙ ( preserves-id-functor-Precategory C D F x) preserves-iso-functor-Precategory : iso-Precategory C x y → iso-Precategory D ( obj-functor-Precategory C D F x) ( obj-functor-Precategory C D F y) pr1 (preserves-iso-functor-Precategory f) = hom-functor-Precategory C D F (hom-iso-Precategory C f) pr2 (preserves-iso-functor-Precategory f) = preserves-is-iso-functor-Precategory ( hom-iso-Precategory C f) ( is-iso-iso-Precategory C f)
See also
Recent changes
- 2023-09-27. Fredrik Bakke. Presheaf categories (#801).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).