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.

Instances
    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.

    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.

    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 X Y f) = f) :

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

    Instances For
      @[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.

      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.

        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.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] :
              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] :
              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] :