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.

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} → ( : c α) → ( : c β) → hom αβ

    the underlying map of a bundled morphism

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

    the identity as a bundled morphism

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

    composition of bundled morphisms

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

    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} ( : c α) ( : c β) ( : c γ) (f : hom ) (g : hom ), self.toFun (self.comp g f) = self.toFun g self.toFun f

    compatibility with the composition

Instances
    theorem CategoryTheory.BundledHom.hom_ext {c : Type u → Type u} {hom : α β : Type u⦄ → c αc βType u} (self : CategoryTheory.BundledHom hom) {α : Type u} {β : Type u} (Iα : c α) (Iβ : c β) :
    Function.Injective (self.toFun )

    a bundled morphism is determined by the underlying map

    @[simp]
    theorem CategoryTheory.BundledHom.id_toFun {c : Type u → Type u} {hom : α β : Type u⦄ → c αc βType u} (self : CategoryTheory.BundledHom hom) {α : Type u} (I : c α) :
    self.toFun I I (self.id I) = id

    compatibility with identities

    @[simp]
    theorem CategoryTheory.BundledHom.comp_toFun {c : Type u → Type u} {hom : α β : Type u⦄ → c αc βType u} (self : CategoryTheory.BundledHom hom) {α : Type u} {β : Type u} {γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom ) (g : hom ) :
    self.toFun (self.comp g f) = self.toFun g self.toFun f

    compatibility with the composition

    instance CategoryTheory.BundledHom.category {c : Type u → Type u} (hom : α β : Type u⦄ → c αc βType u) [𝒞 : CategoryTheory.BundledHom hom] :

    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
    instance CategoryTheory.BundledHom.concreteCategory {c : Type u → Type u} (hom : α β : Type u⦄ → c αc βType u) [𝒞 : CategoryTheory.BundledHom hom] :

    A category given by BundledHom is a concrete category.

    Equations
    • One or more equations did not get rendered due to their size.
    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) :

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

    Equations
    Instances For
      @[reducible, inline]
      abbrev 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
        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 α) :

        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.
        Instances For
          class CategoryTheory.BundledHom.ParentProjection {c : Type u → Type u} {d : Type u → Type u} (F : {α : Type u} → d αc α) :

          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
              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] :
              Equations
              • One or more equations did not get rendered due to their size.
              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] :
              Equations
              • =