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} → (Iα : c α) → (Iβ : c β) → hom Iα Iβ → α → β

  the underlying map of a bundled morphism

• id : {α : Type u} → (I : c α) → hom I I

  the identity as a bundled morphism

• comp : {α β γ : Type u} → (Iα : c α) → (Iβ : c β) → (Iγ : c γ) → hom Iβ Iγ → hom Iα Iβ → hom Iα Iγ

  composition of bundled morphisms

• hom_ext : ∀ {α β : Type u} (Iα : c α) (Iβ : c β), Function.Injective (self.toFun Iα Iβ)

  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} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ), self.toFun Iα Iγ (self.comp Iα Iβ Iγ g f) = self.toFun Iβ Iγ g ∘ self.toFun Iα Iβ f

  compatibility with the composition

theorem CategoryTheory.BundledHom.hom_ext {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → Type u} (self : CategoryTheory.BundledHom hom) {α : Type u} {β : Type u} (Iα : c α) (Iβ : c β) : Function.Injective (self.toFun Iα Iβ)

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 : CategoryTheory.BundledHom hom) {α : 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 : CategoryTheory.BundledHom hom) {α : Type u} {β : Type u} {γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ) : self.toFun Iα Iγ (self.comp Iα Iβ Iγ g f) = self.toFun Iβ Iγ g ∘ self.toFun Iα Iβ f

compatibility with the composition

instance CategoryTheory.BundledHom.category {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] : CategoryTheory.Category.{u, u + 1} (CategoryTheory.Bundled c)

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

• CategoryTheory.BundledHom.category hom = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CategoryTheory.BundledHom.concreteCategory {c : Type u → Type u} (hom : ⦃α β : Type u⦄ → c α → c β → Type u) [𝒞 : CategoryTheory.BundledHom hom] : CategoryTheory.ConcreteCategory (CategoryTheory.Bundled c)

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} [𝒞 : 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 f) = ⇑f) : CategoryTheory.HasForget₂ (CategoryTheory.Bundled c) (CategoryTheory.Bundled d)

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

Equations

• CategoryTheory.BundledHom.mkHasForget₂ obj map h_map = CategoryTheory.HasForget₂.mk' (CategoryTheory.Bundled.map obj) ⋯ (fun {X Y : CategoryTheory.Bundled c} => map) ⋯

@[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

• CategoryTheory.BundledHom.MapHom hom F iα iβ = hom (F iα) (F iβ)

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 α) : CategoryTheory.BundledHom (CategoryTheory.BundledHom.MapHom hom F)

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.

class CategoryTheory.BundledHom.ParentProjection {c : Type u → Type u} {d : Type u → Type u} (F : {α : Type u} → d α → c α) : Prop

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) := ⟨⟩

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] : CategoryTheory.BundledHom (CategoryTheory.BundledHom.MapHom hom F)

Equations

• CategoryTheory.BundledHom.bundledHomOfParentProjection hom F = CategoryTheory.BundledHom.map hom 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] : CategoryTheory.HasForget₂ (CategoryTheory.Bundled d) (CategoryTheory.Bundled 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) [𝒞 : CategoryTheory.BundledHom hom] {d : Type u → Type u} (F : {α : Type u} → d α → c α) [CategoryTheory.BundledHom.ParentProjection F] : (CategoryTheory.forget₂ (CategoryTheory.Bundled d) (CategoryTheory.Bundled c)).Full

Equations

• ⋯ = ⋯