# 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 : ) {α : 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 : ) {α : 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 : ) {α : 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) [𝒞 : ] :

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) [𝒞 : ] :

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} [𝒞 : ] {d : Type u → Type u} {hom_d : α β : Type u⦄ → d αd βType u} [] (obj : α : Type u⦄ → c αd α) (map : {X Y : } → (X Y)()) (h_map : ∀ {X Y : } (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) [𝒞 : ] {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.bundledHomOfParentProjection {c : Type u → Type u} (hom : α β : Type u⦄ → c αc βType u) [𝒞 : ] {d : Type u → Type u} (F : {α : Type u} → d αc α) :
Equations
instance CategoryTheory.BundledHom.forget₂ {c : Type u → Type u} (hom : α β : Type u⦄ → c αc βType u) [𝒞 : ] {d : Type u → Type u} (F : {α : Type u} → d αc α) :
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) [𝒞 : ] {d : Type u → Type u} (F : {α : Type u} → d αc α) :
.Full
Equations
• =