Concrete categories

A concrete category is a category C where the objects and morphisms correspond with types and (bundled) functions between these types. We define concrete categories using class ConcreteCategory. To convert an object to a type, write ToHom. To convert a morphism to a (bundled) function, write hom.

Each concrete category C comes with a canonical faithful functor forget C : C ⥤ Type*, see class HasForget. In particular, we impose no restrictions on the category C, so Type has the identity forgetful functor.

We say that a concrete category C admits a forgetful functor to a concrete category D, if it has a functor forget₂ C D : C ⥤ D such that (forget₂ C D) ⋙ (forget D) = forget C, see class HasForget₂. Due to Faithful.div_comp, it suffices to verify that forget₂.obj and forget₂.map agree with the equality above; then forget₂ will satisfy the functor laws automatically, see HasForget₂.mk'.

Two classes helping construct concrete categories in the two most common cases are provided in the files BundledHom and UnbundledHom, see their documentation for details.

Implementation notes

We are currently switching over from HasForget to a new class ConcreteCategory, see Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign

Previously, ConcreteCategory had the same definition as now HasForget; the coercion of objects/morphisms to types/functions was defined as (forget C).obj and (forget C).map respectively. This leads to defeq issues since existing CoeFun and FunLike instances provide their own casts. We replace this with a less bundled ConcreteCategory that does not directly use these coercions.

We do not use CoeSort to convert objects in a concrete category to types, since this would lead to elaboration mismatches between results taking a [ConcreteCategory C] instance and specific types C that hold a ConcreteCategory C instance: the first gets a literal CoeSort.coe and the second gets unfolded to the actual coe field.

ToType and ToHom are abbrevs so that we do not need to copy over instances such as Ring or RingHomClass respectively.

Since X → Y is not a FunLike, the category of types is not a ConcreteCategory, but it does have a HasForget instance.

References

See Ahrens and Lumsdaine, Displayed Categories for related work.

class CategoryTheory.HasForget (C : Type u) [Category.{v, u} C] : Type (max (max u v) (w + 1))

A concrete category is a category C with a fixed faithful functor Forget : C ⥤ Type.

Note that HasForget potentially depends on three independent universe levels,

• the universe level w appearing in Forget : C ⥤ Type w
• the universe level v of the morphisms (i.e. we have a Category.{v} C)
• the universe level u of the objects (i.e C : Type u) They are specified that order, to avoid unnecessary universe annotations.

• forget : Functor C (Type w)

  We have a functor to Type

• forget_faithful : HasForget.forget.Faithful

  That functor is faithful

@[reducible, inline]

abbrev CategoryTheory.forget (C : Type u) [Category.{v, u} C] [HasForget C] : Functor C (Type w)

The forgetful functor from a concrete category to Type u.

Equations

• CategoryTheory.forget C = CategoryTheory.HasForget.forget

@[reducible, inline]

instance CategoryTheory.HasForget.types : HasForget (Type u)

Equations

• CategoryTheory.HasForget.types = CategoryTheory.HasForget.mk (CategoryTheory.Functor.id (Type ?u.5))

def CategoryTheory.HasForget.hasCoeToSort (C : Type u) [Category.{v, u} C] [HasForget C] : CoeSort C (Type w)

Provide a coercion to Type u for a concrete category. This is not marked as an instance as it could potentially apply to every type, and so is too expensive in typeclass search.

You can use it on particular examples as:

instance : HasCoeToSort X := HasForget.hasCoeToSort X

Equations

• CategoryTheory.HasForget.hasCoeToSort C = { coe := fun (X : C) => (CategoryTheory.forget C).obj X }

@[reducible, inline]

abbrev CategoryTheory.HasForget.instFunLike {C : Type u} [Category.{v, u} C] [HasForget C] {X Y : C} : FunLike (X ⟶ Y) ((forget C).obj X) ((forget C).obj Y)

In any concrete category, (forget C).map is injective.

Equations

• CategoryTheory.HasForget.instFunLike = { coe := fun (f : X ⟶ Y) => (CategoryTheory.forget C).map f, coe_injective' := ⋯ }

theorem CategoryTheory.ConcreteCategory.hom_ext {C : Type u} [Category.{v, u} C] [HasForget C] {X Y : C} (f g : X ⟶ Y) (w : ∀ (x : (forget C).obj X), f x = g x) : f = g

In any concrete category, we can test equality of morphisms by pointwise evaluations.

theorem CategoryTheory.forget_map_eq_coe {C : Type u} [Category.{v, u} C] [HasForget C] {X Y : C} (f : X ⟶ Y) : (forget C).map f = ⇑f

theorem CategoryTheory.congr_hom {C : Type u} [Category.{v, u} C] [HasForget C] {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : (forget C).obj X) : f x = g x

Analogue of congr_fun h x, when h : f = g is an equality between morphisms in a concrete category.

theorem CategoryTheory.coe_id {C : Type u} [Category.{v, u} C] [HasForget C] {X : C} : ⇑(CategoryStruct.id X) = id

theorem CategoryTheory.coe_comp {C : Type u} [Category.{v, u} C] [HasForget C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryStruct.comp f g) = ⇑g ∘ ⇑f

@[simp]

theorem CategoryTheory.id_apply {C : Type u} [Category.{v, u} C] [HasForget C] {X : C} (x : (forget C).obj X) : (CategoryStruct.id X) x = x

@[simp]

theorem CategoryTheory.comp_apply {C : Type u} [Category.{v, u} C] [HasForget C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget C).obj X) : (CategoryStruct.comp f g) x = g (f x)

theorem CategoryTheory.comp_apply' {C : Type u} [Category.{v, u} C] [HasForget C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget C).obj X) : (forget C).map (CategoryStruct.comp f g) x = (forget C).map g ((forget C).map f x)

Variation of ConcreteCategory.comp_apply that uses forget instead.

theorem CategoryTheory.ConcreteCategory.congr_hom {C : Type u} [Category.{v, u} C] [HasForget C] {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : (forget C).obj X) : f x = g x

theorem CategoryTheory.ConcreteCategory.congr_arg {C : Type u} [Category.{v, u} C] [HasForget C] {X Y : C} (f : X ⟶ Y) {x x' : (forget C).obj X} (h : x = x') : f x = f x'

@[simp]

theorem CategoryTheory.ConcreteCategory.hasCoeToFun_Type {X Y : Type u} (f : X ⟶ Y) : CoeFun.coe f = f

class CategoryTheory.HasForget₂ (C : Type u) (D : Type u') [Category.{v, u} C] [HasForget C] [Category.{v', u'} D] [HasForget D] : Type (max (max (max u u') v) v')

HasForget₂ C D, where C and D are both concrete categories, provides a functor forget₂ C D : C ⥤ D and a proof that forget₂ ⋙ (forget D) = forget C.

• forget₂ : Functor C D

  A functor from C to D

• forget_comp : forget₂.comp (forget D) = forget C

  It covers the HasForget.forget for C and D

@[reducible, inline]

abbrev CategoryTheory.forget₂ (C : Type u) (D : Type u') [Category.{v, u} C] [HasForget C] [Category.{v', u'} D] [HasForget D] [HasForget₂ C D] : Functor C D

The forgetful functor C ⥤ D between concrete categories for which we have an instance HasForget₂ C.

Equations

• CategoryTheory.forget₂ C D = CategoryTheory.HasForget₂.forget₂

theorem CategoryTheory.forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v, u} C] [HasForget C] [Category.{v', u'} D] [HasForget D] [HasForget₂ C D] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget D).obj ((forget₂ C D).obj X)) : ((forget₂ C D).map (CategoryStruct.comp f g)) x = ((forget₂ C D).map g) (((forget₂ C D).map f) x)

instance CategoryTheory.forget₂_faithful (C : Type u) (D : Type u') [Category.{v, u} C] [HasForget C] [Category.{v', u'} D] [HasForget D] [HasForget₂ C D] : (forget₂ C D).Faithful

instance CategoryTheory.InducedCategory.hasForget {C : Type u} {D : Type u'} [Category.{v', u'} D] [HasForget D] (f : C → D) : HasForget (InducedCategory D f)

Equations

• CategoryTheory.InducedCategory.hasForget f = CategoryTheory.HasForget.mk ((CategoryTheory.inducedFunctor f).comp (CategoryTheory.forget D))

instance CategoryTheory.InducedCategory.hasForget₂ {C : Type u} {D : Type u'} [Category.{v, u'} D] [HasForget D] (f : C → D) : HasForget₂ (InducedCategory D f) D

Equations

• CategoryTheory.InducedCategory.hasForget₂ f = { forget₂ := CategoryTheory.inducedFunctor f, forget_comp := ⋯ }

instance CategoryTheory.FullSubcategory.hasForget {C : Type u} [Category.{v, u} C] [HasForget C] (Z : C → Prop) : HasForget (FullSubcategory Z)

Equations

• CategoryTheory.FullSubcategory.hasForget Z = CategoryTheory.HasForget.mk ((CategoryTheory.fullSubcategoryInclusion Z).comp (CategoryTheory.forget C))

instance CategoryTheory.FullSubcategory.hasForget₂ {C : Type u} [Category.{v, u} C] [HasForget C] (Z : C → Prop) : HasForget₂ (FullSubcategory Z) C

Equations

• CategoryTheory.FullSubcategory.hasForget₂ Z = { forget₂ := CategoryTheory.fullSubcategoryInclusion Z, forget_comp := ⋯ }

def CategoryTheory.HasForget₂.mk' {C : Type u} {D : Type u'} [Category.{v, u} C] [HasForget C] [Category.{v', u'} D] [HasForget D] (obj : C → D) (h_obj : ∀ (X : C), (forget D).obj (obj X) = (forget C).obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ((forget D).map (map f)) ((forget C).map f)) : HasForget₂ C D

In order to construct a “partially forgetting” functor, we do not need to verify functor laws; it suffices to ensure that compositions agree with forget₂ C D ⋙ forget D = forget C.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def CategoryTheory.HasForget₂.trans (C : Type u) [Category.{v, u} C] [HasForget C] (D : Type u') [Category.{v', u'} D] [HasForget D] (E : Type u'') [Category.{v'', u''} E] [HasForget E] [HasForget₂ C D] [HasForget₂ D E] : HasForget₂ C E

Composition of HasForget₂ instances.

Equations

• CategoryTheory.HasForget₂.trans C D E = { forget₂ := (CategoryTheory.forget₂ C D).comp (CategoryTheory.forget₂ D E), forget_comp := ⋯ }

def CategoryTheory.hasForgetToType (C : Type u) [Category.{v, u} C] [HasForget C] : HasForget₂ C (Type w)

Every forgetful functor factors through the identity functor. This is not a global instance as it is prone to creating type class resolution loops.

Equations

• CategoryTheory.hasForgetToType C = { forget₂ := CategoryTheory.forget C, forget_comp := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.naturality_apply {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasForget D] {F G : Functor C D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : (forget D).obj (F.obj X)) : (φ.app Y) ((F.map f) x) = (G.map f) ((φ.app X) x)

class CategoryTheory.ConcreteCategory (C : Type u) [Category.{v, u} C] (FC : outParam (C → C → Type u_1)) {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] : Type (max (max u u_1) v)

A concrete category is a category C where objects correspond to types and morphisms to (bundled) functions between those types.

In other words, it has a fixed faithful functor forget : C ⥤ Type.

Note that ConcreteCategory potentially depends on three independent universe levels,

• the universe level w appearing in forget : C ⥤ Type w
• the universe level v of the morphisms (i.e. we have a Category.{v} C)
• the universe level u of the objects (i.e C : Type u) They are specified that order, to avoid unnecessary universe annotations.

• hom {X Y : C} : (X ⟶ Y) → FC X Y

  Convert a morphism of C to a bundled function.

• ofHom {X Y : C} : FC X Y → (X ⟶ Y)

  Convert a bundled function to a morphism of C.

• hom_ofHom {X Y : C} (f : FC X Y) : hom (ofHom f) = f
• ofHom_hom {X Y : C} (f : X ⟶ Y) : ofHom (hom f) = f
• id_apply {X : C} (x : CC X) : (hom (CategoryStruct.id X)) x = x
• comp_apply {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X) : (hom (CategoryStruct.comp f g)) x = (hom g) ((hom f) x)

@[reducible, inline]

abbrev CategoryTheory.ToType {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : C → Type w

ToType X converts the object X of the concrete category C to a type.

This is an abbrev so that instances on X (e.g. Ring) do not need to be redeclared.

Equations

• CategoryTheory.ToType = CC

@[reducible, inline]

abbrev CategoryTheory.ToHom {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : C → C → Type u_1

ToHom X Y is the type of (bundled) functions between objects X Y : C.

This is an abbrev so that instances (e.g. RingHomClass) do not need to be redeclared.

Equations

• CategoryTheory.ToHom = FC

instance CategoryTheory.ConcreteCategory.instCoeFunHomForallToType {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ToType X → ToType Y

We can apply morphisms of concrete categories by first casting them down to the base functions.

Equations

• CategoryTheory.ConcreteCategory.instCoeFunHomForallToType = { coe := fun (f : X ⟶ Y) => ⇑(CategoryTheory.ConcreteCategory.hom f) }

def CategoryTheory.ConcreteCategory.homEquiv {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} : (X ⟶ Y) ≃ ToHom X Y

ConcreteCategory.hom bundled as an Equiv.

Equations

• CategoryTheory.ConcreteCategory.homEquiv = { toFun := CategoryTheory.ConcreteCategory.hom, invFun := CategoryTheory.ConcreteCategory.ofHom, left_inv := ⋯, right_inv := ⋯ }

theorem CategoryTheory.ConcreteCategory.hom_bijective {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} : Function.Bijective hom

theorem CategoryTheory.ConcreteCategory.hom_injective {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} : Function.Injective hom

theorem CategoryTheory.ConcreteCategory.ext {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g

In any concrete category, we can test equality of morphisms by pointwise evaluations.

theorem CategoryTheory.ConcreteCategory.coe_ext {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} {f g : X ⟶ Y} (h : ⇑(hom f) = ⇑(hom g)) : f = g

theorem CategoryTheory.ConcreteCategory.ext_apply {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} {f g : X ⟶ Y} (h : ∀ (x : CC X), (hom f) x = (hom g) x) : f = g

instance CategoryTheory.ConcreteCategory.toHasForget {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : HasForget C

A concrete category comes with a forgetful functor to Type.

Warning: because of the way that ConcreteCategory and HasForget are set up, we can't make forget Type reducibly defeq to the identity functor.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.forget_obj {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] (X : C) : (forget C).obj X = ToType X

@[simp]

theorem CategoryTheory.ConcreteCategory.forget_map_eq_coe {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) : (forget C).map f = ⇑(hom f)

theorem CategoryTheory.congr_fun {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : ToType X) : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Analogue of congr_fun h x, when h : f = g is an equality between morphisms in a concrete category.

theorem CategoryTheory.congr_arg {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) {x x' : ToType X} (h : x = x') : (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x'

Analogue of congr_arg f h, when h : x = x' is an equality between elements of objects in a concrete category.

theorem CategoryTheory.hom_id {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X : C} : ⇑(ConcreteCategory.hom (CategoryStruct.id X)) = id

theorem CategoryTheory.hom_comp {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(ConcreteCategory.hom (CategoryStruct.comp f g)) = ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)

theorem CategoryTheory.coe_toHasForget_instFunLike {C : Type u_2} [Category.{u_5, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4} [inst : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) : ⇑f = ⇑(ConcreteCategory.hom f)

Using the FunLike coercion of HasForget does the same as the original coercion.

@[reducible, inline]

abbrev CategoryTheory.HasForget.toFunLike (C : Type u) [Category.{v, u} C] [HasForget C] (X Y : C) : FunLike (X ⟶ Y) ((forget C).obj X) ((forget C).obj Y)

Build a coercion to functions out of HasForget.

The intended usecase is to provide a FunLike instance in HasForget.toConcreteCategory. See that definition for the considerations in making this an instance.

See note [reducible non-instances].

Equations

• CategoryTheory.HasForget.toFunLike C X Y = { coe := (CategoryTheory.forget C).map, coe_injective' := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.HasForget.toConcreteCategory (C : Type u) [Category.{v, u} C] [HasForget C] : ConcreteCategory C fun (x1 x2 : C) => x1 ⟶ x2

Build a concrete category out of HasForget.

The intended usecase is to prove theorems referencing only (forget C) and not (forget C).obj X nor (forget C).map f: those should be written as ToType X and ConcreteCategory.hom f respectively.

See note [reducible non-instances].

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.forget_eq_ConcreteCategory_hom (C : Type u) [Category.{v, u} C] [HasForget C] {X Y : C} (f : X ⟶ Y) : (forget C).map f = ⇑(ConcreteCategory.hom f)

Note that the ConcreteCategory and HasForget instances here differ from forget_map_eq_coe.

@[reducible, inline]

abbrev CategoryTheory.Types.instFunLike (X Y : Type u) : FunLike (X ⟶ Y) X Y

A FunLike instance on plain functions, in order to instantiate a ConcreteCategory structure on the category of types.

This is not an instance (yet) because that would require a lot of downstream fixes.

See note [reducible non-instances].

Equations

• CategoryTheory.Types.instFunLike = CategoryTheory.HasForget.toFunLike (Type ?u.13)

@[reducible, inline]

abbrev CategoryTheory.Types.instConcreteCategory : ConcreteCategory (Type u) fun (X Y : Type u) => X ⟶ Y

The category of types is concrete, using the identity functor.

This is not an instance (yet) because that would require a lot of downstream fixes.

See note [reducible non-instances].

Equations

• One or more equations did not get rendered due to their size.