3.7. Concrete categories
When doing constructions or stating theorems about concrete categories,
a concrete category C can be introduced by using the following variables:
variable {C : Type*} [Category* C]
{FC : C → C → Type*} {CC : C → Type w}
[∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory.{w} C FC]
This roughly means that a type CC X is attached to any object X : C,
that the types of morphisms X ⟶ Y in the category C can be identified
(up to a bijection) with a type FC X Y and that FC X Y injects into
the type of functions CC X → CC Y.
For example, if R is a ring, the category ModuleCat R is a concrete category,
with CC being the underlying type of a R-module and FC the type of
linear maps:
variable (R : Type*) [Ring R]
#synth ConcreteCategory (ModuleCat R) (· →ₗ[R] ·)
Note that the types of morphisms in ModuleCat R are not defined directly using
types of linear maps (they are defined using a 1-field structure), but for
the concrete category instance, we use · →ₗ[R] ·.
If C is a concrete category, we have a faithful forgetful functor to the category
of types:
example : C ⥤ Type w := forget C
#synth (forget C).Faithful
-- `ToType` is an abbreviation for `CC`,
-- and if `f : X ⟶ Y` and `x : ToType X`,
-- the syntax `f x` allows to evaluate `f` at `x`:
example {X Y : C} (f : X ⟶ Y) (x : ToType X) :
ToType Y := f x
The lemma comp_apply relates the composition of morphisms and
the evaluation:
variable {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z)
example : f ≫ g = h ↔ ∀ x, g (f x) = h x := C:Type u_1inst✝³:Category.{v_1, u_1} CFC:C → C → Type u_2CC:C → Type winst✝²:(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)inst✝¹:ConcreteCategory C FCR:Type u_3inst✝:Ring RX:CY:CZ:Cf:X ⟶ Yg:Y ⟶ Zh:X ⟶ Z⊢ f ≫ g = h ↔ ∀ (x : CC X), (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x) = (ConcreteCategory.hom h) x
All goals completed! 🐙