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 ToType. 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 the file Mathlib.CategoryTheory.ConcreteCategory.Forget
Implementation notes #
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.
References #
See Ahrens and Lumsdaine, Displayed Categories for related work.
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
wappearing inforget : C ⥤ Type w - the universe level
vof the morphisms (i.e. we have aCategory.{v} C) - the universe level
uof the objects (i.eC : 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
Cto a bundled function. - ofHom {X Y : C} : FC X Y → (X ⟶ Y)
Convert a bundled function to a morphism of
C.
Instances
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
Instances For
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
Instances For
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) }
A non-instance FunLike instance on X ⟶ Y.
Equations
- CategoryTheory.HasForget.instFunLike = { coe := fun (f : X ⟶ Y) => ⇑(CategoryTheory.ConcreteCategory.hom f), coe_injective' := ⋯ }
Instances For
ConcreteCategory.hom bundled as an Equiv.
Equations
- CategoryTheory.ConcreteCategory.homEquiv = { toFun := CategoryTheory.ConcreteCategory.hom, invFun := CategoryTheory.ConcreteCategory.ofHom, left_inv := ⋯, right_inv := ⋯ }
Instances For
In any concrete category, we can test equality of morphisms by pointwise evaluations.
In any concrete category, we can test equality of morphisms by pointwise evaluations.
Analogue of congr_fun h x,
when h : f = g is an equality between morphisms in a concrete category.
Alias of CategoryTheory.comp_apply.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.