Concrete categories
A concrete category is a category C with a fixed faithful functor
forget : C ⥤ Type*. We define concrete categories using class
concrete_category. 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 has_forget₂. 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
has_forget₂.mk'.
Two classes helping construct concrete categories in the two most
common cases are provided in the files bundled_hom and
unbundled_hom, see their documentation for details.
References
See [Ahrens and Lumsdaine, Displayed Categories][ahrens2017] for related work.
- forget : C ⥤ Type ?
- forget_faithful : category_theory.faithful (category_theory.concrete_category.forget C)
A concrete category is a category C with a fixed faithful functor forget : C ⥤ Type.
Instances
- category_theory.concrete_category.types
- category_theory.induced_category.concrete_category
- category_theory.bundled_hom.category_theory.concrete_category
- Mon.concrete_category
- AddMon.concrete_category
- CommMon.concrete_category
- AddCommMon.concrete_category
- Group.concrete_category
- AddGroup.concrete_category
- CommGroup.concrete_category
- AddCommGroup.concrete_category
- SemiRing.concrete_category
- Ring.concrete_category
- CommSemiRing.concrete_category
- CommRing.concrete_category
- Module.category_theory.concrete_category
- Algebra.category_theory.concrete_category
- category_theory.graded_object.category_theory.concrete_category
- category_theory.differential_object.concrete_category_of_differential_objects
- Top.concrete_category
- Meas.concrete_category
- Preorder.concrete_category
- PartialOrder.concrete_category
- LinearOrder.concrete_category
- NonemptyFinLinOrd.concrete_category
- TopCommRing.category_theory.concrete_category
- UniformSpace.concrete_category
- CpltSepUniformSpace.concrete_category
The forgetful functor from a concrete category to Type u.
Equations
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 : has_coe_to_sort X := concrete_category.has_coe_to_sort X
Equations
- category_theory.concrete_category.has_coe_to_sort C = {S := Type u, coe := (category_theory.concrete_category.forget C).obj}
Usually a bundled hom structure already has a coercion to function that works with different universes. So we don't use this as a global instance.
In any concrete category, we can test equality of morphisms by pointwise evaluations.
In any concrete category, injective morphisms are monomorphisms.
In any concrete category, surjective morphisms are epimorphisms.
Equations
- forget₂ : C ⥤ D
- forget_comp : category_theory.has_forget₂.forget₂ ⋙ category_theory.forget D = category_theory.forget C . "obviously"
has_forget₂ 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.
Instances
- category_theory.induced_category.has_forget₂
- category_theory.has_forget_to_Type
- category_theory.bundled_hom.forget₂
- CommMon.has_forget_to_Mon
- AddCommMon.has_forget_to_AddMon
- Group.has_forget_to_Mon
- AddGroup.has_forget_to_AddMon
- CommGroup.has_forget_to_Group
- AddCommGroup.has_forget_to_AddGroup
- CommGroup.has_forget_to_CommMon
- AddCommGroup.has_forget_to_AddCommMon
- SemiRing.has_forget_to_Mon
- SemiRing.has_forget_to_AddCommMon
- Ring.has_forget_to_SemiRing
- Ring.has_forget_to_AddCommGroup
- CommSemiRing.has_forget_to_SemiRing
- CommSemiRing.has_forget_to_CommMon
- CommRing.has_forget_to_Ring
- CommRing.has_forget_to_CommSemiRing
- Module.has_forget_to_AddCommGroup
- Algebra.has_forget_to_Ring
- Algebra.has_forget_to_Module
- category_theory.graded_object.category_theory.has_forget₂
- category_theory.differential_object.category_theory.has_forget₂
- Top.has_forget_to_Meas
- TopCommRing.has_forget_to_CommRing
- TopCommRing.has_forget_to_Top
- UniformSpace.has_forget_to_Top
- CpltSepUniformSpace.has_forget_to_UniformSpace
The forgetful functor C ⥤ D between concrete categories for which we have an instance
has_forget₂ C.
Equations
Equations
- _ = _
Equations
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
- category_theory.has_forget₂.mk' obj h_obj map h_map = {forget₂ := category_theory.faithful.div (category_theory.forget C) (category_theory.forget D) (λ (X : C), obj X) h_obj (λ (X Y : C) (f : X ⟶ Y), map f) h_map, forget_comp := _}
Equations
- category_theory.has_forget_to_Type C = {forget₂ := category_theory.forget C _inst_2, forget_comp := _}