Documentation

Mathlib.CategoryTheory.ConcreteCategory.BundledHom

Category instances for algebraic structures that use bundled homs. #

Many algebraic structures in Lean initially used unbundled homs (e.g. a bare function between types, along with an IsMonoidHom typeclass), but the general trend is towards using bundled homs.

This file provides a basic infrastructure to define concrete categories using bundled homs, and define forgetful functors between them.

source
class CategoryTheory.BundledHom {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) :
Type (u + 1)

Class for bundled homs. Note that the arguments order follows that of lemmas for MonoidHom. This way we can use ⟨@MonoidHom.toFun, @MonoidHom.id ...⟩ in an instance.

  • toFun : {α β : Type u} → (Iα : c α) → (Iβ : c β) → hom Iα Iβ → α → β

    the underlying map of a bundled morphism

  • id : {α : Type u} → (I : c α) → hom I I

    the identity as a bundled morphism

  • comp : {α β γ : Type u} → (Iα : c α) → (Iβ : c β) → (Iγ : c γ) → hom Iβ Iγ → hom Iα Iβ → hom Iα Iγ

    composition of bundled morphisms

  • hom_ext : ∀ {α β : Type u} (Iα : c α) (Iβ : c β), Function.Injective (self.toFun Iα Iβ)

    a bundled morphism is determined by the underlying map

  • id_toFun : ∀ {α : Type u} (I : c α), self.toFun I I (self.id I) = id

    compatibility with identities

  • comp_toFun : ∀ {α β γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ), self.toFun Iα Iγ (self.comp Iα Iβ Iγ g f) = self.toFun Iβ Iγ g ∘ self.toFun Iα Iβ f

    compatibility with the composition

Instances
source
instance CategoryTheory.BundledHom.category {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] :
CategoryTheory.Category.{u, u + 1} (CategoryTheory.Bundled c)

Every @BundledHom c _ defines a category with objects in Bundled c.

This instance generates the type-class problem BundledHom ?m. Currently that is not a problem, as there are almost no instances of BundledHom.

Equations
source
instance CategoryTheory.BundledHom.concreteCategory {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] :
CategoryTheory.ConcreteCategory (CategoryTheory.Bundled c)

A category given by BundledHom is a concrete category.

Equations
  • One or more equations did not get rendered due to their size.
source
def CategoryTheory.BundledHom.mkHasForget₂ {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → Type u} [𝒞 : CategoryTheory.BundledHom hom] {d : Type u → Type u} {hom_d : ⦃α β : Type u⦄ → d α → d β → Type u} [CategoryTheory.BundledHom hom_d] (obj : ⦃α : Type u⦄ → c α → d α) (map : {X Y : CategoryTheory.Bundled c} → (X ⟶ Y) → (CategoryTheory.Bundled.map obj X ⟶ CategoryTheory.Bundled.map obj Y)) (h_map : ∀ {X Y : CategoryTheory.Bundled c} (f : X ⟶ Y), ⇑(map f) = ⇑f) :
CategoryTheory.HasForget₂ (CategoryTheory.Bundled c) (CategoryTheory.Bundled d)

A version of HasForget₂.mk' for categories defined using @BundledHom.

Equations
source
@[reducible]
def CategoryTheory.BundledHom.MapHom {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) {d : Type u → Type u} (F : {α : Type u} → d α → c α) ⦃α : Type u⦄ ⦃β : Type u⦄ :
d α → d β → Type u

The hom corresponding to first forgetting along F, then taking the hom associated to c.

For typical usage, see the construction of CommMonCat from MonCat.

Equations
Instances For
source
def CategoryTheory.BundledHom.map {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] {d : Type u → Type u} (F : {α : Type u} → d α → c α) :
CategoryTheory.BundledHom (CategoryTheory.BundledHom.MapHom hom F)

Construct the CategoryTheory.BundledHom induced by a map between type classes. This is useful for building categories such as CommMonCat from MonCat.

Equations
  • One or more equations did not get rendered due to their size.
source
class CategoryTheory.BundledHom.ParentProjection {c : Type u → Type u} {d : Type u → Type u} (F : {α : Type u} → d α → c α) :
Prop

We use the empty ParentProjection class to label functions like CommMonoid.toMonoid, which we would like to use to automatically construct BundledHom instances from.

Once we've set up MonCat as the category of bundled monoids, this allows us to set up CommMonCat by defining an instance instance : ParentProjection (CommMonoid.toMonoid) := ⟨⟩

    Instances
    source
    instance CategoryTheory.BundledHom.bundledHomOfParentProjection {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] {d : Type u → Type u} (F : {α : Type u} → d α → c α) [CategoryTheory.BundledHom.ParentProjection F] :
    CategoryTheory.BundledHom (CategoryTheory.BundledHom.MapHom hom F)
    Equations
    source
    instance CategoryTheory.BundledHom.forget₂ {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] {d : Type u → Type u} (F : {α : Type u} → d α → c α) [CategoryTheory.BundledHom.ParentProjection F] :
    CategoryTheory.HasForget₂ (CategoryTheory.Bundled d) (CategoryTheory.Bundled c)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.BundledHom.forget₂Full {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] {d : Type u → Type u} (F : {α : Type u} → d α → c α) [CategoryTheory.BundledHom.ParentProjection F] :
    CategoryTheory.Full (CategoryTheory.forget₂ (CategoryTheory.Bundled d) (CategoryTheory.Bundled c))
    Equations
    • One or more equations did not get rendered due to their size.