mathlib documentation

category_theory.concrete_category.unbundled_hom

Category instances for structures that use unbundled homs

This file provides basic infrastructure to define concrete categories using unbundled homs (see class unbundled_hom), and define forgetful functors between them (see unbundled_hom.mk_has_forget₂).

@[class]
structure category_theory.unbundled_hom {c : Type uType u} :
(Π {α β : Type u}, c αc β(α → β) → Prop) → Type
  • hom_id : ∀ {α : Type ?} (ia : c α), hom ia ia id
  • hom_comp : ∀ {α β γ : Type ?} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β → γ} {f : α → β}, hom Iβ ghom Iα fhom Iα (g f)

A class for unbundled homs used to define a category. hom must take two types α, β and instances of the corresponding structures, and return a predicate on α → β.

Instances
@[instance]
def category_theory.unbundled_hom.bundled_hom (c : Type uType u) (hom : Π ⦃α β : Type u⦄, c αc β(α → β) → Prop) [𝒞 : category_theory.unbundled_hom hom] :
category_theory.bundled_hom (λ (α β : Type u) (Iα : c α) (Iβ : c β), subtype (hom Iα Iβ))

Equations
def category_theory.unbundled_hom.mk_has_forget₂ {c : Type uType u} {hom : Π ⦃α β : Type u⦄, c αc β(α → β) → Prop} [𝒞 : category_theory.unbundled_hom hom] {c' : Type uType u} {hom' : Π ⦃α β : Type u⦄, c' αc' β(α → β) → Prop} [𝒞' : category_theory.unbundled_hom hom'] (obj : Π ⦃α : Type u⦄, c αc' α) :
(∀ ⦃α β : Type u⦄ ⦃Iα : c α⦄ ⦃Iβ : c β⦄ ⦃f : α → β⦄, hom Iα fhom' (obj Iα) (obj Iβ) f)category_theory.has_forget₂ (category_theory.bundled c) (category_theory.bundled c')

A custom constructor for forgetful functor between concrete categories defined using unbundled_hom.

Equations