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 u Type u} (hom : Π ⦃α β : 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 (self.to_fun Iβ)) . "obviously"
  • id_to_fun : ( {α : Type ?} (I : c α), self.to_fun I I (self.id I) = id) . "obviously"
  • comp_to_fun : ( {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ), self.to_fun (self.comp g f) = self.to_fun g self.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 of this typeclass
Instances of other typeclasses for category_theory.bundled_hom
  • category_theory.bundled_hom.has_sizeof_inst
@[protected, nolint, instance]

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
@[protected, nolint, instance]

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 u Type u} {hom : Π ⦃α β : Type u⦄, c α c β Type u} [𝒞 : category_theory.bundled_hom hom] {d : Type u Type 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)) (h_map : {X Y : category_theory.bundled c} (f : X Y), (map f) = f) :

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

Equations
@[reducible]
def category_theory.bundled_hom.map_hom {c : Type u Type u} (hom : Π ⦃α β : Type u⦄, c α c β Type u) {d : Type u Type u} (F : Π {α : Type u}, d α c α) ⦃α β : Type u⦄ (Iα : d α) (Iβ : d β) :

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 u Type u} (hom : Π ⦃α β : Type u⦄, c α c β Type u) [𝒞 : category_theory.bundled_hom hom] {d : Type u Type 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
@[class]
structure category_theory.bundled_hom.parent_projection {c d : Type u Type u} (F : Π {α : Type u}, d α c α) :

We use the empty parent_projection class to label functions like comm_monoid.to_monoid, which we would like to use to automatically construct bundled_hom instances from.

Once we've set up Mon as the category of bundled monoids, this allows us to set up CommMon by defining an instance instance : parent_projection (comm_monoid.to_monoid) := ⟨⟩

Instances of this typeclass
Instances of other typeclasses for category_theory.bundled_hom.parent_projection
  • category_theory.bundled_hom.parent_projection.has_sizeof_inst
@[protected, instance]
Equations