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.

source
@[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α Iβ → α → β
  • id : Π {α : Type ?} (I : c α), hom I I
  • comp : Π {α β γ : Type ?} (Iα : c α) (Iβ : c β) (Iγ : c γ), hom Iβ Iγ → hom Iα Iβ → hom Iα Iγ
  • hom_ext : (∀ {α β : Type ?} (Iα : c α) (Iβ : c β), function.injective (self.to_fun Iα 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 Iα Iγ (self.comp Iα Iβ Iγ g f) = self.to_fun Iβ Iγ g ∘ self.to_fun Iα Iβ 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
source
@[protected, nolint, instance]
def category_theory.bundled_hom.category {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] :
category_theory.category (category_theory.bundled c)

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
source
@[protected, nolint, instance]
def category_theory.bundled_hom.concrete_category {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄, c α → c β → Type u) [𝒞 : category_theory.bundled_hom hom] :
category_theory.concrete_category (category_theory.bundled c)

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
source
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) :
category_theory.has_forget₂ (category_theory.bundled c) (category_theory.bundled d)

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

Equations
source
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 β) :
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
source
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 α) :
category_theory.bundled_hom (category_theory.bundled_hom.map_hom hom F)

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

Equations
source
@[class]
inductive category_theory.bundled_hom.parent_projection {c d : Type u → Type u} (F : Π {α : Type u}, d α → c α) :
Type

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
source
@[protected, nolint, instance]
def category_theory.bundled_hom.bundled_hom_of_parent_projection {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 α) [category_theory.bundled_hom.parent_projection F] :
category_theory.bundled_hom (category_theory.bundled_hom.map_hom hom F)
Equations
source
@[protected, instance]
def category_theory.bundled_hom.forget₂ {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 α) [category_theory.bundled_hom.parent_projection F] :
category_theory.has_forget₂ (category_theory.bundled d) (category_theory.bundled c)
Equations
source
@[protected, instance]
def category_theory.bundled_hom.forget₂_full {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 α) [category_theory.bundled_hom.parent_projection F] :
category_theory.full (category_theory.forget₂ (category_theory.bundled d) (category_theory.bundled c))
Equations