mathlib3 documentation

category_theory.concrete_category.basic

Concrete categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 for related work.

@[class]

structure category_theory.concrete_category (C : Type u) [category_theory.category C] :

Type (max u v (w+1))

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.

Note that concrete_category 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.

Instances of this typeclass

Instances of other typeclasses for category_theory.concrete_category

category_theory.concrete_category.has_sizeof_inst

@[reducible]

def category_theory.forget (C : Type u) [category_theory.category C] [category_theory.concrete_category C] :

The forgetful functor from a concrete category to Type u.

Equations

category_theory.forget C = category_theory.concrete_category.forget C

@[protected, instance]

def category_theory.concrete_category.types :

category_theory.concrete_category (Type u)

Equations

category_theory.concrete_category.types = category_theory.concrete_category.mk (𝟭 (Type u))

def category_theory.concrete_category.has_coe_to_sort (C : Type u) [category_theory.category C] [category_theory.concrete_category C] :

has_coe_to_sort 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 : has_coe_to_sort X := concrete_category.has_coe_to_sort X

Equations

category_theory.concrete_category.has_coe_to_sort C = {coe := (category_theory.concrete_category.forget C).obj}

@[simp]

theorem category_theory.forget_obj_eq_coe {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X : C} :

(category_theory.forget C).obj X = ↥X

def category_theory.concrete_category.has_coe_to_fun {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} :

has_coe_to_fun (X ⟶ Y) (λ (f : X ⟶ Y), ↥X → ↥Y)

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.

Equations

category_theory.concrete_category.has_coe_to_fun = {coe := λ (f : X ⟶ Y), (category_theory.forget C).map f}

theorem category_theory.concrete_category.hom_ext {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f g : X ⟶ Y) (w : ∀ (x : ↥X), ⇑f x = ⇑g x) :

f = g

In any concrete category, we can test equality of morphisms by pointwise evaluations.

@[simp]

theorem category_theory.forget_map_eq_coe {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) :

(category_theory.forget C).map f = ⇑f

theorem category_theory.congr_hom {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : ↥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 category_theory.coe_id {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X : C} :

⇑(𝟙 X) = id

theorem category_theory.coe_comp {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :

⇑(f ≫ g) = ⇑g ∘ ⇑f

@[simp]

theorem category_theory.id_apply {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X : C} (x : ↥X) :

⇑(𝟙 X) x = x

@[simp]

theorem category_theory.comp_apply {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) :

⇑(f ≫ g) x = ⇑g (⇑f x)

theorem category_theory.concrete_category.congr_hom {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : ↥X) :

⇑f x = ⇑g x

theorem category_theory.concrete_category.congr_arg {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) {x x' : ↥X} (h : x = x') :

⇑f x = ⇑f x'

theorem category_theory.concrete_category.mono_of_injective {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) (i : function.injective ⇑f) :

category_theory.mono f

In any concrete category, injective morphisms are monomorphisms.

theorem category_theory.concrete_category.injective_of_mono_of_preserves_pullback {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] [category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan (category_theory.forget C)] :

function.injective ⇑f

theorem category_theory.concrete_category.mono_iff_injective_of_preserves_pullback {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan (category_theory.forget C)] :

category_theory.mono f ↔ function.injective ⇑f

theorem category_theory.concrete_category.epi_of_surjective {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) (s : function.surjective ⇑f) :

category_theory.epi f

In any concrete category, surjective morphisms are epimorphisms.

theorem category_theory.concrete_category.surjective_of_epi_of_preserves_pushout {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) [category_theory.epi f] [category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span (category_theory.forget C)] :

function.surjective ⇑f

theorem category_theory.concrete_category.epi_iff_surjective_of_preserves_pushout {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span (category_theory.forget C)] :

category_theory.epi f ↔ function.surjective ⇑f

theorem category_theory.concrete_category.bijective_of_is_iso {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :

function.bijective ((category_theory.forget C).map f)

@[simp]

theorem category_theory.concrete_category.has_coe_to_fun_Type {X Y : Type u} (f : X ⟶ Y) :

⇑f = f

@[class]

structure category_theory.has_forget₂ (C : Type u) (D : Type u') [category_theory.category C] [category_theory.concrete_category C] [category_theory.category D] [category_theory.concrete_category D] :

Type (max u u' v v')

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 of this typeclass

Instances of other typeclasses for category_theory.has_forget₂

category_theory.has_forget₂.has_sizeof_inst

@[reducible]

def category_theory.forget₂ (C : Type u) (D : Type u') [category_theory.category C] [category_theory.concrete_category C] [category_theory.category D] [category_theory.concrete_category D] [category_theory.has_forget₂ C D] :

C ⥤ D

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

Equations

category_theory.forget₂ C D = category_theory.has_forget₂.forget₂

@[protected, instance]

def category_theory.forget₂_faithful (C : Type u) (D : Type u') [category_theory.category C] [category_theory.concrete_category C] [category_theory.category D] [category_theory.concrete_category D] [category_theory.has_forget₂ C D] :

category_theory.faithful (category_theory.forget₂ C D)

@[protected, instance]

def category_theory.forget₂_preserves_monomorphisms (C : Type u) (D : Type u') [category_theory.category C] [category_theory.concrete_category C] [category_theory.category D] [category_theory.concrete_category D] [category_theory.has_forget₂ C D] [(category_theory.forget C).preserves_monomorphisms] :

(category_theory.forget₂ C D).preserves_monomorphisms

@[protected, instance]

def category_theory.forget₂_preserves_epimorphisms (C : Type u) (D : Type u') [category_theory.category C] [category_theory.concrete_category C] [category_theory.category D] [category_theory.concrete_category D] [category_theory.has_forget₂ C D] [(category_theory.forget C).preserves_epimorphisms] :

(category_theory.forget₂ C D).preserves_epimorphisms

@[protected, instance]

def category_theory.induced_category.concrete_category {C : Type u} {D : Type u'} [category_theory.category D] [category_theory.concrete_category D] (f : C → D) :

category_theory.concrete_category (category_theory.induced_category D f)

Equations

category_theory.induced_category.concrete_category f = category_theory.concrete_category.mk (category_theory.induced_functor f ⋙ category_theory.forget D)

@[protected, instance]

def category_theory.induced_category.has_forget₂ {C : Type u} {D : Type u'} [category_theory.category D] [category_theory.concrete_category D] (f : C → D) :

category_theory.has_forget₂ (category_theory.induced_category D f) D

Equations

category_theory.induced_category.has_forget₂ f = {forget₂ := category_theory.induced_functor f, forget_comp := _}

@[protected, instance]

def category_theory.full_subcategory.concrete_category {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (Z : C → Prop) :

category_theory.concrete_category (category_theory.full_subcategory Z)

Equations

category_theory.full_subcategory.concrete_category Z = category_theory.concrete_category.mk (category_theory.full_subcategory_inclusion Z ⋙ category_theory.forget C)

@[protected, instance]

def category_theory.full_subcategory.has_forget₂ {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (Z : C → Prop) :

category_theory.has_forget₂ (category_theory.full_subcategory Z) C

Equations

category_theory.full_subcategory.has_forget₂ Z = {forget₂ := category_theory.full_subcategory_inclusion Z, forget_comp := _}

def category_theory.has_forget₂.mk' {C : Type u} {D : Type u'} [category_theory.category C] [category_theory.concrete_category C] [category_theory.category D] [category_theory.concrete_category D] (obj : C → D) (h_obj : ∀ (X : C), (category_theory.forget D).obj (obj X) = (category_theory.forget C).obj X) (map : Π {X Y : C}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, (category_theory.forget D).map (map f) == (category_theory.forget C).map f) :

category_theory.has_forget₂ 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

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 := _}

def category_theory.has_forget_to_Type (C : Type u) [category_theory.category C] [category_theory.concrete_category C] :

category_theory.has_forget₂ 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

category_theory.has_forget_to_Type C = {forget₂ := category_theory.forget C _inst_2, forget_comp := _}