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 u Type u} (hom : Π {α β : Type u}, c α c β β) Prop) :
  • hom_id : {α : Type ?} (ia : c α), hom ia ia id
  • hom_comp : {α β γ : Type ?} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β γ} {f : α β}, hom Iβ g hom Iα f hom 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 of this typeclass
Instances of other typeclasses for category_theory.unbundled_hom
  • category_theory.unbundled_hom.has_sizeof_inst
@[protected, instance]
def category_theory.unbundled_hom.bundled_hom (c : Type u Type 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 u Type u} {hom : Π ⦃α β : Type u⦄, c α c β β) Prop} [𝒞 : category_theory.unbundled_hom hom] {c' : Type u Type u} {hom' : Π ⦃α β : Type u⦄, c' α c' β β) Prop} [𝒞' : category_theory.unbundled_hom hom'] (obj : Π ⦃α : Type u⦄, c α c' α) (map : ⦃α β : Type u⦄ ⦃Iα : c α⦄ ⦃Iβ : c β⦄ ⦃f : α β⦄, hom Iα f hom' (obj Iα) (obj Iβ) f) :

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

Equations