mathlib documentation

category_theory.concrete_category.bundled_hom

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 is_monoid_hom 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]
structure category_theory.bundled_hom {c : Type uType u} :
(Π ⦃α β : Type u⦄, c αc βType u)Type (u+1)
  • to_fun : Π {α β : Type ?} (Iα : c α) (Iβ : c β), hom Iαα → β
  • id : Π {α : Type ?} (I : c α), hom I I
  • comp : Π {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ), hom Iβhom Iαhom Iα
  • hom_ext : (∀ {α β : Type ?} (Iα : c α) (Iβ : c β), function.injective (c_1.to_fun Iβ)) . "obviously"
  • id_to_fun : (∀ {α : Type ?} (I : c α), c_1.to_fun I I (c_1.id I) = id) . "obviously"
  • comp_to_fun : (∀ {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ), c_1.to_fun (c_1.comp g f) = c_1.to_fun g c_1.to_fun f) . "obviously"

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

Instances
@[nolint, instance]
def category_theory.bundled_hom.category {c : Type uType u} (hom : Π ⦃α β : Type u⦄, c αc βType u) [𝒞 : category_theory.bundled_hom hom] :

Every @bundled_hom c _ defines a category with objects in bundled c.

This instance generates the type-class problem bundled_hom ?m (which is why this is marked as [nolint]). Currently that is not a problem, as there are almost no instances of bundled_hom.

Equations
@[nolint, instance]
def category_theory.bundled_hom.category_theory.concrete_category {c : Type uType u} (hom : Π ⦃α β : Type u⦄, c αc βType u) [𝒞 : category_theory.bundled_hom hom] :

A category given by bundled_hom is a concrete category.

This instance generates the type-class problem bundled_hom ?m (which is why this is marked as [nolint]). Currently that is not a problem, as there are almost no instances of bundled_hom.

Equations
def category_theory.bundled_hom.mk_has_forget₂ {c : Type uType u} {hom : Π ⦃α β : Type u⦄, c αc βType u} [𝒞 : category_theory.bundled_hom hom] {d : Type uType u} {hom_d : Π ⦃α β : Type u⦄, d αd βType u} [category_theory.bundled_hom hom_d] (obj : Π ⦃α : Type u⦄, c αd α) (map : Π {X Y : category_theory.bundled c}, (X Y)(category_theory.bundled.map obj X category_theory.bundled.map obj Y)) :

A version of has_forget₂.mk' for categories defined using @bundled_hom.

Equations
def category_theory.bundled_hom.map_hom {c : Type uType u} (hom : Π ⦃α β : Type u⦄, c αc βType u) {d : Type uType u} (F : Π {α : Type u}, d αc α) ⦃α β : 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 CommMon from Mon.

Equations
def category_theory.bundled_hom.map {c : Type uType u} (hom : Π ⦃α β : Type u⦄, c αc βType u) [𝒞 : category_theory.bundled_hom hom] {d : Type uType u} (F : Π {α : Type u}, d αc α) :

Construct the bundled_hom induced by a map between type classes. This is useful for building categories such as CommMon from Mon.

Equations
@[nolint, instance]
def category_theory.bundled_hom.bundled_hom_of_parent_projection {c : Type uType u} (hom : Π ⦃α β : Type u⦄, c αc βType u) [𝒞 : category_theory.bundled_hom hom] {d : Type uType u} (F : Π {α : Type u}, d αc α) [category_theory.bundled_hom.parent_projection F] :

Equations
@[instance]
def category_theory.bundled_hom.forget₂ {c : Type uType u} (hom : Π ⦃α β : Type u⦄, c αc βType u) [𝒞 : category_theory.bundled_hom hom] {d : Type uType u} (F : Π {α : Type u}, d αc α) [category_theory.bundled_hom.parent_projection F] :

Equations