Concrete categories

A concrete category is a category C with a fixed faithful functor forget : C ⥤ Type*. We define concrete categories using class ConcreteCategory. In particular, we impose no restrictions on the carrier type C, so Type is a concrete category with the identity forgetful functor.

Each concrete category C comes with a canonical faithful functor forget C : C ⥤ Type*. 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.

References

See [Ahrens and Lumsdaine, Displayed Categories][ahrens2017] for related work.

class CategoryTheory.ConcreteCategory (C : Type u) [CategoryTheory.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 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.

• forget : CategoryTheory.Functor C (Type w)

  We have a functor to Type

• forget_faithful : CategoryTheory.Functor.Faithful CategoryTheory.ConcreteCategory.forget

  That functor is faithful

@[reducible]

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

The forgetful functor from a concrete category to Type u.

Equations

• CategoryTheory.forget C = CategoryTheory.ConcreteCategory.forget

@[reducible]

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

Equations

• CategoryTheory.ConcreteCategory.types = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.id (Type u))

def CategoryTheory.ConcreteCategory.hasCoeToSort (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory 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 := ConcreteCategory.hasCoeToSort X

Equations

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

@[reducible]

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

Equations

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

theorem CategoryTheory.ConcreteCategory.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) (w : ∀ (x : (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.forget C).map f = ⇑f

theorem CategoryTheory.congr_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (x : (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} : ⇑(CategoryTheory.CategoryStruct.id X) = id

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

@[simp]

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

@[simp]

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

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

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

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

theorem CategoryTheory.ConcreteCategory.mono_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) (i : Function.Injective ⇑f) : CategoryTheory.Mono f

In any concrete category, injective morphisms are monomorphisms.

theorem CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)] : Function.Injective ⇑f

theorem CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)] : CategoryTheory.Mono f ↔ Function.Injective ⇑f

theorem CategoryTheory.ConcreteCategory.epi_of_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) (s : Function.Surjective ⇑f) : CategoryTheory.Epi f

In any concrete category, surjective morphisms are epimorphisms.

theorem CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)] : Function.Surjective ⇑f

theorem CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)] : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

theorem CategoryTheory.ConcreteCategory.bijective_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : Function.Bijective ((CategoryTheory.forget C).map f)

theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Functor.ReflectsIsomorphisms (CategoryTheory.forget C)] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ Function.Bijective ((CategoryTheory.forget C).map f)

If the forgetful functor of a concrete category reflects isomorphisms, being an isomorphism is equivalent to being bijective.

@[simp]

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

class CategoryTheory.HasForget₂ (C : Type u) (D : Type u') [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory 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₂ : CategoryTheory.Functor C D

  A functor from C to D

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

  It covers the ConcreteCategory.forget for C and D

@[reducible]

def CategoryTheory.forget₂ (C : Type u) (D : Type u') [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.HasForget₂ C D] : CategoryTheory.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'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.HasForget₂ C D] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : (CategoryTheory.forget D).obj ((CategoryTheory.forget₂ C D).obj X)) : ((CategoryTheory.forget₂ C D).map (CategoryTheory.CategoryStruct.comp f g)) x = ((CategoryTheory.forget₂ C D).map g) (((CategoryTheory.forget₂ C D).map f) x)

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.InducedCategory.concreteCategory f = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.comp (CategoryTheory.inducedFunctor f) (CategoryTheory.forget D))

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

Equations

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

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

Equations

• CategoryTheory.FullSubcategory.concreteCategory Z = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.comp (CategoryTheory.fullSubcategoryInclusion Z) (CategoryTheory.forget C))

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

Equations

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

def CategoryTheory.HasForget₂.mk' {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] (obj : C → D) (h_obj : ∀ (X : C), (CategoryTheory.forget D).obj (obj X) = (CategoryTheory.forget C).obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ((CategoryTheory.forget D).map (map f)) ((CategoryTheory.forget C).map f)) : CategoryTheory.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.

def CategoryTheory.hasForgetToType (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.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 := ⋯ }