Documentation

Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom

Category instances for structures that use unbundled homs #

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

class CategoryTheory.UnbundledHom {c : Type u → Type u} (hom : α β : Type u⦄ → c αc β(αβ)Prop) :

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 α → β.

  • hom_id : ∀ {α : Type u} (ia : c α), hom ia ia id
  • hom_comp : ∀ {α β γ : Type u} { : c α} { : c β} { : c γ} {g : βγ} {f : αβ}, hom ghom fhom (g f)
Instances
    theorem CategoryTheory.UnbundledHom.hom_id {c : Type u → Type u} {hom : α β : Type u⦄ → c αc β(αβ)Prop} [self : CategoryTheory.UnbundledHom hom] {α : Type u} (ia : c α) :
    hom ia ia id
    theorem CategoryTheory.UnbundledHom.hom_comp {c : Type u → Type u} {hom : α β : Type u⦄ → c αc β(αβ)Prop} [self : CategoryTheory.UnbundledHom hom] {α : Type u} {β : Type u} {γ : Type u} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : βγ} {f : αβ} :
    hom ghom fhom (g f)
    instance CategoryTheory.UnbundledHom.bundledHom (c : Type u → Type u) (hom : α β : Type u⦄ → c αc β(αβ)Prop) [𝒞 : CategoryTheory.UnbundledHom hom] :
    CategoryTheory.BundledHom fun (α β : Type u) ( : c α) ( : c β) => Subtype (hom )
    Equations
    • One or more equations did not get rendered due to their size.
    def CategoryTheory.UnbundledHom.mkHasForget₂ {c : Type u → Type u} {hom : α β : Type u⦄ → c αc β(αβ)Prop} [𝒞 : CategoryTheory.UnbundledHom hom] {c' : Type u → Type u} {hom' : α β : Type u⦄ → c' αc' β(αβ)Prop} [𝒞' : CategoryTheory.UnbundledHom hom'] (obj : α : Type u⦄ → c αc' α) (map : ∀ ⦃α β : Type u⦄ ⦃ : c α⦄ ⦃ : c β⦄ ⦃f : αβ⦄, hom fhom' (obj ) (obj ) f) :

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

    Equations
    Instances For