Forgetful functors

A concrete category is a category C where the objects and morphisms correspond with types and (bundled) functions between these types, see the file Mathlib.CategoryTheory.ConcreteCategory.Basic

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

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'.

References

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

def CategoryTheory.forget (C : Type u_1) [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] : Functor C (Type w)

The forgetful functor from a concrete category to the category of types.

instance CategoryTheory.instFaithfulForget (C : Type u_1) [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] : (forget C).Faithful

@[simp]

theorem CategoryTheory.ConcreteCategory.forget_map_eq_coe {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((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.forget_obj {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] (X : C) : (forget C).obj X = ToType X

theorem CategoryTheory.congr_fun {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((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_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((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.

class CategoryTheory.HasForget₂ (C : Type u_1) [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] (D : Type u_3) [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] : Type (max (max (max u_1 u_3) v_1) v_2)

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 forget for C and D

@[reducible, inline]

abbrev CategoryTheory.forget₂ (C : Type u_1) [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] (D : Type u_3) [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] [HasForget₂ C D] : Functor C D

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

theorem CategoryTheory.forget₂_comp_apply {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] {D : Type u_3} [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] [HasForget₂ C D] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ToType ((forget₂ C D).obj X)) : (ConcreteCategory.hom ((forget₂ C D).map (CategoryStruct.comp f g))) x = (ConcreteCategory.hom ((forget₂ C D).map g)) ((ConcreteCategory.hom ((forget₂ C D).map f)) x)

instance CategoryTheory.forget₂_faithful {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] {D : Type u_3} [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] [HasForget₂ C D] : (forget₂ C D).Faithful

instance CategoryTheory.InducedCategory.hasForget₂ {C : Type u_1} {D : Type u_3} [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] (f : C → D) : HasForget₂ (InducedCategory D f) D

instance CategoryTheory.FullSubcategory.hasForget₂ {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] (P : ObjectProperty C) : HasForget₂ P.FullSubcategory C

def CategoryTheory.HasForget₂.mk' {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] {D : Type u_3} [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] (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}, (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.

@[reducible]

def CategoryTheory.HasForget₂.trans (C : Type u_1) [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] (D : Type u_3) [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] (E : Type u_5) [Category.{v_3, u_5} E] {FE : outParam (E → E → Type u_6)} {CE : outParam (E → Type w)} [outParam ((X Y : E) → FunLike (FE X Y) (CE X) (CE Y))] [ConcreteCategory E FE] [HasForget₂ C D] [HasForget₂ D E] : HasForget₂ C E

Composition of HasForget₂ instances.

theorem CategoryTheory.ConcreteCategory.forget₂_comp_apply {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] {D : Type u_3} [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] [HasForget₂ C D] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ToType ((forget₂ C D).obj X)) : (hom ((forget₂ C D).map (CategoryStruct.comp f g))) x = (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x)

instance CategoryTheory.hom_isIso {C : Type u_1} [Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso ⇑(ConcreteCategory.hom f)

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

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

@[simp]

theorem CategoryTheory.Types.hom_eq_coe {X Y : Type u} (f : X ⟶ Y) : ConcreteCategory.hom f = f

@[simp]

theorem CategoryTheory.NatTrans.naturality_apply {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_3} [Category.{v_2, u_3} D] {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)} [outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [ConcreteCategory D FD] {F G : Functor C D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : ToType (F.obj X)) : (ConcreteCategory.hom (φ.app Y)) ((ConcreteCategory.hom (F.map f)) x) = (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app X)) x)