Mathlib.CategoryTheory.ConcreteCategory.Basic

Module docstring

{"# 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 ToHom. 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 class HasForget. In particular, 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'.

Two classes helping construct concrete categories in the two most common cases are provided in the files BundledHom and UnbundledHom, see their documentation for details.

Implementation notes

We are currently switching over from HasForget to a new class ConcreteCategory, see Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign

Previously, ConcreteCategory had the same definition as now HasForget; the coercion of objects/morphisms to types/functions was defined as (forget C).obj and (forget C).map respectively. This leads to defeq issues since existing CoeFun and FunLike instances provide their own casts. We replace this with a less bundled ConcreteCategory that does not directly use these coercions.

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.

Since X → Y is not a FunLike, the category of types is not a ConcreteCategory, but it does have a HasForget instance.

References

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

CategoryTheory.HasForget structure

(C : Type u) [Category.{v} C]

Full source

/-- A concrete category is a category `C` with a fixed faithful functor `Forget : C ⥤ Type`.

Note that `HasForget` 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.
-/
class HasForget (C : Type u) [Category.{v} C] where
  /-- We have a functor to Type -/
  protected forget : C ⥤ Type w
  /-- That functor is faithful -/
  [forget_faithful : forget.Faithful]

Concrete Category

Informal description

A concrete category is a category $ C $ equipped with a faithful functor $ \text{Forget} : C \to \text{Type} $, which maps objects of $ C $ to types and morphisms of $ C $ to functions between these types. This functor allows us to view the objects and morphisms of $ C $ as types and functions, respectively, while preserving the categorical structure.

CategoryTheory.forget abbrev

(C : Type u) [Category.{v} C] [HasForget.{w} C] : C ⥤ Type w

Full source

/-- The forgetful functor from a concrete category to `Type u`. -/
abbrev forget (C : Type u) [Category.{v} C] [HasForget.{w} C] : C ⥤ Type w :=
  HasForget.forget

Forgetful Functor from Concrete Category to Types

Informal description

The forgetful functor from a concrete category $C$ to the category of types $\mathrm{Type}_w$, denoted $\mathrm{Forget} : C \to \mathrm{Type}_w$, maps objects of $C$ to their underlying types and morphisms of $C$ to their underlying functions.

CategoryTheory.HasForget.types abbrev

: HasForget.{u, u, u + 1} (Type u)

Full source

@[instance] abbrev HasForget.types : HasForget.{u, u, u+1} (Type u) where
  forget := 𝟭 _

Identity Forgetful Functor for the Category of Types

Informal description

The category of types $\mathrm{Type}_u$ in a given universe $u$ has a forgetful functor to itself, which is the identity functor. This means that the forgetful functor maps each type to itself and each function to itself, preserving the categorical structure.

CategoryTheory.HasForget.hasCoeToSort definition

(C : Type u) [Category.{v} C] [HasForget.{w} C] : CoeSort C (Type w)

Full source

/-- 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 : HasCoeToSort X := HasForget.hasCoeToSort X
```
-/
def HasForget.hasCoeToSort (C : Type u) [Category.{v} C] [HasForget.{w} C] :
    CoeSort C (Type w) where
  coe X := (forget C).obj X

Coercion from concrete category objects to types

Informal description

Given a concrete category $ C $ with a forgetful functor to the category of types, this definition provides a coercion from objects of $ C $ to types in the target universe $ w $. Specifically, for any object $ X $ in $ C $, the coercion maps $ X $ to its underlying type as given by the forgetful functor.

CategoryTheory.HasForget.instFunLike abbrev

{X Y : C} : FunLike (X ⟶ Y) X Y

Full source

/-- In any concrete category, `(forget C).map` is injective. -/
abbrev HasForget.instFunLike {X Y : C} : FunLike (X ⟶ Y) X Y where
  coe f := (forget C).map f
  coe_injective' _ _ h := (forget C).map_injective h

Function-Like Structure on Morphisms in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, the hom-set $\mathrm{Hom}(X, Y)$ has a function-like structure, meaning there exists an injective coercion from morphisms $f : X \to Y$ to functions $X \to Y$.

CategoryTheory.ConcreteCategory.hom_ext theorem

{X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x = g x) : f = g

Full source

/-- In any concrete category, we can test equality of morphisms by pointwise evaluations. -/
@[ext low] -- Porting note: lowered priority
theorem ConcreteCategory.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x = g x) : f = g := by
  apply (forget C).map_injective
  dsimp [forget]
  funext x
  exact w x

Extensionality of Morphisms in Concrete Categories

Informal description

Let $C$ be a concrete category, and let $X$ and $Y$ be objects in $C$. For any two morphisms $f, g : X \to Y$, if $f(x) = g(x)$ for all $x \in X$, then $f = g$.

CategoryTheory.forget_map_eq_coe theorem

{X Y : C} (f : X ⟶ Y) : (forget C).map f = f

Full source

theorem forget_map_eq_coe {X Y : C} (f : X ⟶ Y) : (forget C).map f = f := rfl

Forgetful Functor Preserves Morphisms as Functions

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, and for any morphism $f : X \to Y$, the image of $f$ under the forgetful functor $\mathrm{Forget} : C \to \mathrm{Type}$ is equal to $f$ itself when viewed as a function.

CategoryTheory.congr_hom theorem

{X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x

Full source

/-- Analogue of `congr_fun h x`,
when `h : f = g` is an equality between morphisms in a concrete category.
-/
theorem congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
  congrFun (congrArg (fun k : X ⟶ Y => (k : X → Y)) h) x

Morphism Equality Implies Pointwise Equality in Concrete Categories

Informal description

Let $C$ be a concrete category, and let $X$ and $Y$ be objects in $C$. For any two morphisms $f, g : X \to Y$, if $f = g$, then $f(x) = g(x)$ for all $x \in X$.

CategoryTheory.coe_id theorem

{X : C} : (𝟙 X : X → X) = id

Full source

theorem coe_id {X : C} : (𝟙 X : X → X) = id :=
  (forget _).map_id X

Identity Morphism Corresponds to Identity Function in Concrete Categories

Informal description

For any object $X$ in a concrete category $C$, the identity morphism $\mathrm{id}_X : X \to X$ corresponds to the identity function $\mathrm{id} : X \to X$ when viewed through the forgetful functor.

CategoryTheory.coe_comp theorem

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : X → Z) = g ∘ f

Full source

theorem coe_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : X → Z) = g ∘ f :=
  (forget _).map_comp f g

Composition of Morphisms in Concrete Categories Corresponds to Function Composition

Informal description

For any objects $X, Y, Z$ in a concrete category $C$, and for any morphisms $f : X \to Y$ and $g : Y \to Z$, the underlying function of the composition $f \gg g$ is equal to the function composition $g \circ f$.

CategoryTheory.id_apply theorem

{X : C} (x : X) : (𝟙 X : X → X) x = x

Full source

@[simp] theorem id_apply {X : C} (x : X) : (𝟙 X : X → X) x = x :=
  congr_fun ((forget _).map_id X) x

Identity Morphism Acts as Identity Function on Elements

Informal description

For any object $X$ in a concrete category $C$ and any element $x \in X$, the identity morphism $\mathrm{id}_X : X \to X$ evaluated at $x$ equals $x$, i.e., $\mathrm{id}_X(x) = x$.

CategoryTheory.comp_apply theorem

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x)

Full source

@[simp] theorem comp_apply {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) :=
  congr_fun ((forget _).map_comp _ _) x

Composition of Morphisms in Concrete Categories Evaluates as Function Composition

Informal description

For any objects $X, Y, Z$ in a concrete category $C$, and for any morphisms $f : X \to Y$ and $g : Y \to Z$, the composition $f \gg g$ evaluated at $x \in X$ satisfies $(f \gg g)(x) = g(f(x))$.

CategoryTheory.comp_apply' theorem

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (forget C).map (f ≫ g) x = (forget C).map g ((forget C).map f x)

Full source

/-- Variation of `ConcreteCategory.comp_apply` that uses `forget` instead. -/
theorem comp_apply' {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (forget C).map (f ≫ g) x = (forget C).map g ((forget C).map f x) := comp_apply f g x

Forgetful Functor Preserves Composition in Concrete Categories

Informal description

For any objects $X, Y, Z$ in a concrete category $C$ with forgetful functor $\mathrm{Forget} : C \to \mathrm{Type}$, and for any morphisms $f : X \to Y$ and $g : Y \to Z$, the composition $f \gg g$ evaluated at $x \in X$ satisfies $\mathrm{Forget}(f \gg g)(x) = \mathrm{Forget}(g)(\mathrm{Forget}(f)(x))$.

CategoryTheory.ConcreteCategory.congr_hom theorem

{X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x

Full source

theorem ConcreteCategory.congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
  congr_fun (congr_arg (fun f : X ⟶ Y => (f : X → Y)) h) x

Function Equality Implies Pointwise Equality in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, and for any morphisms $f, g : X \to Y$ such that $f = g$, it holds that $f(x) = g(x)$ for all $x \in X$.

CategoryTheory.ConcreteCategory.congr_arg theorem

{X Y : C} (f : X ⟶ Y) {x x' : X} (h : x = x') : f x = f x'

Full source

theorem ConcreteCategory.congr_arg {X Y : C} (f : X ⟶ Y) {x x' : X} (h : x = x') : f x = f x' :=
  congrArg (f : X → Y) h

Morphism Application Respects Equality in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, and for any morphism $f : X \to Y$, if $x = x'$ for elements $x, x' \in X$, then $f(x) = f(x')$.

CategoryTheory.ConcreteCategory.hasCoeToFun_Type theorem

{X Y : Type u} (f : X ⟶ Y) : CoeFun.coe f = f

Full source

@[simp]
theorem ConcreteCategory.hasCoeToFun_Type {X Y : Type u} (f : X ⟶ Y) : CoeFun.coe f = f := rfl

Canonical Coercion of Type Morphisms to Functions is Identity

Informal description

For any types $X$ and $Y$ in a universe $u$, and for any morphism $f : X \to Y$ in the category of types, the canonical coercion of $f$ to a function is equal to $f$ itself.

CategoryTheory.HasForget₂ structure

(C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C] [Category.{v'} D] [HasForget.{w} D]

Full source

/-- `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`.
-/
class HasForget₂ (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C]
  [Category.{v'} D] [HasForget.{w} D] where
  /-- A functor from `C` to `D` -/
  forget₂ : C ⥤ D
  /-- It covers the `HasForget.forget` for `C` and `D` -/
  forget_comp : forget₂ ⋙ forget D = forget C := by aesop

Forgetful Functor Between Concrete Categories

Informal description

The structure `HasForget₂ C D` provides a forgetful functor from a concrete category `C` to another concrete category `D`, along with a proof that composing this functor with the forgetful functor of `D` yields the forgetful functor of `C`. More precisely, given two concrete categories `C` and `D`, the forgetful functor `forget₂ C D : C ⥤ D` satisfies the condition `forget₂ C D ⋙ forget D = forget C`, where `forget C` and `forget D` are the canonical forgetful functors of `C` and `D`, respectively. This ensures that the objects and morphisms of `C` can be consistently "forgotten" into `D` while preserving the categorical structure.

CategoryTheory.forget₂ abbrev

 (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C] [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D] :
  C ⥤ D

Full source

/-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance
`HasForget₂ C`. -/
abbrev forget₂ (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C]
    [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D] : C ⥤ D :=
  HasForget₂.forget₂

Forgetful Functor Between Concrete Categories

Informal description

Given two concrete categories $C$ and $D$ with forgetful functors to the category of types, and given an instance of `HasForget₂ C D`, the forgetful functor $\text{forget}_2 : C \to D$ is defined such that composition with $D$'s forgetful functor yields $C$'s forgetful functor. More precisely, $\text{forget}_2$ is a functor satisfying $\text{forget}_2 \circ \text{forget}_D = \text{forget}_C$, where $\text{forget}_C$ and $\text{forget}_D$ are the canonical forgetful functors of $C$ and $D$ respectively.

CategoryTheory.forget₂_comp_apply theorem

 {C : Type u} {D : Type u'} [Category.{v} C] [HasForget.{w} C] [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget₂ C D).obj X) :
  ((forget₂ C D).map (f ≫ g) x) = (forget₂ C D).map g ((forget₂ C D).map f x)

Full source

lemma forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C] [HasForget.{w} C]
    [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget₂ C D).obj X) :
    ((forget₂ C D).map (f ≫ g) x) =
      (forget₂ C D).map g ((forget₂ C D).map f x) := by
  rw [Functor.map_comp, comp_apply]

Composition Law for Forgetful Functors Between Concrete Categories

Informal description

For any two concrete categories $C$ and $D$ with forgetful functors to the category of types, and given a forgetful functor $\text{forget}_2 : C \to D$ between them, the following holds: For any objects $X, Y, Z$ in $C$, any morphisms $f : X \to Y$ and $g : Y \to Z$, and any element $x$ in the underlying type of $X$ (via $\text{forget}_2$), we have $$(\text{forget}_2(f \gg g))(x) = \text{forget}_2(g)(\text{forget}_2(f)(x)).$$

CategoryTheory.forget₂_faithful instance

 (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C] [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D] :
  (forget₂ C D).Faithful

Full source

instance forget₂_faithful (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C]
    [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D] : (forget₂ C D).Faithful :=
  HasForget₂.forget_comp.faithful_of_comp

Faithfulness of the Forgetful Functor Between Concrete Categories

Informal description

For any two concrete categories $C$ and $D$ with forgetful functors to the category of types, and given a forgetful functor $\text{forget}_2 : C \to D$ between them, the functor $\text{forget}_2$ is faithful. This means that for any two morphisms $f, g : X \to Y$ in $C$, if $\text{forget}_2(f) = \text{forget}_2(g)$, then $f = g$.

CategoryTheory.InducedCategory.hasForget instance

{C : Type u} {D : Type u'} [Category.{v'} D] [HasForget.{w} D] (f : C → D) : HasForget (InducedCategory D f)

Full source

instance InducedCategory.hasForget {C : Type u} {D : Type u'}
    [Category.{v'} D] [HasForget.{w} D] (f : C → D) :
    HasForget (InducedCategory D f) where
  forget := inducedFunctorinducedFunctor f ⋙ forget D

Forgetful Functor for Induced Categories

Informal description

For any category $\mathcal{D}$ with a forgetful functor to types and any function $f : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ along $f$ also has a forgetful functor to types. This forgetful functor is obtained by composing the forgetful functor of $\mathcal{D}$ with the canonical functor from the induced category to $\mathcal{D}$.

CategoryTheory.InducedCategory.hasForget₂ instance

{C : Type u} {D : Type u'} [Category.{v} D] [HasForget.{w} D] (f : C → D) : HasForget₂ (InducedCategory D f) D

Full source

instance InducedCategory.hasForget₂ {C : Type u} {D : Type u'} [Category.{v} D]
    [HasForget.{w} D] (f : C → D) : HasForget₂ (InducedCategory D f) D where
  forget₂ := inducedFunctor f
  forget_comp := rfl

Forgetful Functor from Induced Category to Concrete Category

Informal description

For any category $\mathcal{D}$ with a forgetful functor to types and any function $f : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ along $f$ admits a forgetful functor to $\mathcal{D}$. This functor satisfies the condition that composing it with the forgetful functor of $\mathcal{D}$ yields the forgetful functor of the induced category.

CategoryTheory.FullSubcategory.hasForget instance

{C : Type u} [Category.{v} C] [HasForget.{w} C] (P : ObjectProperty C) : HasForget P.FullSubcategory

Full source

instance FullSubcategory.hasForget {C : Type u} [Category.{v} C] [HasForget.{w} C]
    (P : ObjectProperty C) : HasForget P.FullSubcategory where
  forget := P.ι ⋙ forget C

Concrete Structure on Full Subcategories

Informal description

For any concrete category $C$ and any property $P$ on objects of $C$, the full subcategory of $C$ consisting of objects satisfying $P$ is also a concrete category with the forgetful functor inherited from $C$.

CategoryTheory.FullSubcategory.hasForget₂ instance

{C : Type u} [Category.{v} C] [HasForget.{w} C] (P : ObjectProperty C) : HasForget₂ P.FullSubcategory C

Full source

instance FullSubcategory.hasForget₂ {C : Type u} [Category.{v} C] [HasForget.{w} C]
    (P : ObjectProperty C) : HasForget₂ P.FullSubcategory C where
  forget₂ := P.ι
  forget_comp := rfl

Forgetful Functor from Full Subcategory to Concrete Category

Informal description

For any concrete category $C$ and any property $P$ on objects of $C$, the full subcategory of $C$ consisting of objects satisfying $P$ admits a forgetful functor to $C$ that commutes with the canonical forgetful functors.

CategoryTheory.HasForget₂.mk' definition

 {C : Type u} {D : Type u'} [Category.{v} C] [HasForget.{w} C] [Category.{v'} D] [HasForget.{w} D] (obj : C → D)
  (h_obj : ∀ X, (forget D).obj (obj X) = (forget C).obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
  (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq ((forget D).map (map f)) ((forget C).map f)) : HasForget₂ C D

Full source

/-- 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`.
-/
def HasForget₂.mk' {C : Type u} {D : Type u'} [Category.{v} C] [HasForget.{w} C]
    [Category.{v'} D] [HasForget.{w} D]
    (obj : C → D) (h_obj : ∀ X, (forget D).obj (obj X) = (forget C).obj X)
    (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq ((forget D).map (map f)) ((forget C).map f)) :
    HasForget₂ C D where
  forget₂ := Functor.Faithful.div _ _ _ @h_obj _ @h_map
  forget_comp := by apply Functor.Faithful.div_comp

Construction of a forgetful functor between concrete categories

Informal description

Given two concrete categories $ C $ and $ D $, each equipped with forgetful functors to the category of types, the function `HasForget₂.mk'` constructs a forgetful functor from $ C $ to $ D $ by specifying: 1. An object function `obj : C → D` that preserves the underlying types, i.e., for any object $ X $ in $ C $, the underlying type of `obj X` in $ D $ matches the underlying type of $ X $ in $ C $. 2. A morphism function `map` that preserves the underlying functions, i.e., for any morphism $ f : X \to Y $ in $ C $, the underlying function of `map f` in $ D $ matches the underlying function of $ f $ in $ C $. This ensures the resulting forgetful functor satisfies the condition `forget₂ C D ⋙ forget D = forget C`, where `forget C` and `forget D` are the canonical forgetful functors of $ C $ and $ D $, respectively.

CategoryTheory.HasForget₂.trans definition

 (C : Type u) [Category.{v} C] [HasForget.{w} C] (D : Type u') [Category.{v'} D] [HasForget.{w} D] (E : Type u'')
  [Category.{v''} E] [HasForget.{w} E] [HasForget₂ C D] [HasForget₂ D E] : HasForget₂ C E

Full source

/-- Composition of `HasForget₂` instances. -/
@[reducible]
def HasForget₂.trans (C : Type u) [Category.{v} C] [HasForget.{w} C]
    (D : Type u') [Category.{v'} D] [HasForget.{w} D]
    (E : Type u'') [Category.{v''} E] [HasForget.{w} E]
    [HasForget₂ C D] [HasForget₂ D E] : HasForget₂ C E where
  forget₂ := CategoryTheory.forget₂CategoryTheory.forget₂ C D ⋙ CategoryTheory.forget₂ D E
  forget_comp := by
    show (CategoryTheory.forget₂ _ D) ⋙ (CategoryTheory.forget₂ D E ⋙ CategoryTheory.forget E) = _
    simp only [HasForget₂.forget_comp]

Composition of forgetful functors between concrete categories

Informal description

Given three concrete categories $ C $, $ D $, and $ E $, each equipped with forgetful functors to the category of types, and given forgetful functors from $ C $ to $ D $ and from $ D $ to $ E $, there exists a composite forgetful functor from $ C $ to $ E $ that factors through $ D $. More precisely, the forgetful functor $\text{forget}_2 : C \to E$ is defined as the composition of the forgetful functors $\text{forget}_2 : C \to D$ and $\text{forget}_2 : D \to E$, ensuring that the composite functor satisfies $\text{forget}_2 \circ \text{forget}_E = \text{forget}_C$, where $\text{forget}_C$, $\text{forget}_D$, and $\text{forget}_E$ are the canonical forgetful functors of $ C $, $ D $, and $ E $ respectively.

CategoryTheory.hasForgetToType definition

(C : Type u) [Category.{v} C] [HasForget.{w} C] : HasForget₂ C (Type w)

Full source

/-- Every forgetful functor factors through the identity functor. This is not a global instance as
    it is prone to creating type class resolution loops. -/
def hasForgetToType (C : Type u) [Category.{v} C] [HasForget.{w} C] :
    HasForget₂ C (Type w) where
  forget₂ := forget C
  forget_comp := Functor.comp_id _

Forgetful functor from concrete category to types via identity

Informal description

For any concrete category $ C $ with a forgetful functor to the category of types, there exists a forgetful functor from $ C $ to the category of types $ \mathrm{Type}_w $ that factors through the identity functor on $ \mathrm{Type}_w $. This means the forgetful functor from $ C $ to $ \mathrm{Type}_w $ is equal to the composition of the identity functor on $ \mathrm{Type}_w $ with itself.

CategoryTheory.ConcreteCategory structure

 (C : Type u) [Category.{v} C] (FC : outParam <| C → C → Type*) {CC : outParam <| C → Type w}
  [outParam <| ∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]

Full source

/-- 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 `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.
-/
class ConcreteCategory (C : Type u) [Category.{v} C]
    (FC : outParam <| C → C → Type*) {CC : outParam <| C → Type w}
    [outParam <| ∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] where
  /-- Convert a morphism of `C` to a bundled function. -/
  (hom : ∀ {X Y}, (X ⟶ Y) → FC X Y)
  /-- Convert a bundled function to a morphism of `C`. -/
  (ofHom : ∀ {X Y}, FC X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : FC X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (id_apply : ∀ {X} (x : CC X), hom (𝟙 X) x = x := by aesop_cat)
  (comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

Concrete Category

Informal description

A concrete category is a category $ C $ where objects are associated with types and morphisms are associated with (bundled) functions between those types. This is formalized by requiring a faithful functor $ \text{forget} : C \to \text{Type} $, which maps objects to their underlying types and morphisms to their underlying functions. The structure depends on three universe levels: - $ w $: the universe level of the types in the codomain of the forgetful functor. - $ v $: the universe level of the morphisms in the category $ C $. - $ u $: the universe level of the objects in $ C $. The forgetful functor ensures that the category $ C $ can be faithfully represented in the category of types and functions.

CategoryTheory.ToType abbrev

[ConcreteCategory C FC]

Full source

/-- `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.
-/
@[nolint unusedArguments] -- Need the instance to trigger unification that finds `CC`.
abbrev ToType [ConcreteCategory C FC] := CC

Underlying Type of an Object in a Concrete Category

Informal description

Given a concrete category $ C $ with objects and morphisms represented by types and functions respectively, the abbreviation `ToType X` converts an object $ X $ of $ C $ to its underlying type.

CategoryTheory.ToHom abbrev

[ConcreteCategory C FC]

Full source

/-- `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.
-/
@[nolint unusedArguments] -- Need the instance to trigger unification that finds `FC`.
abbrev ToHom [ConcreteCategory C FC] := FC

Bundled Hom-Set in a Concrete Category

Informal description

Given a concrete category $ C $ with morphism type constructor $ FC $, the type `ToHom X Y` represents the bundled functions between objects $ X $ and $ Y $ in $ C $.

CategoryTheory.ConcreteCategory.instCoeFunHomForallToType instance

{X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ ToType X → ToType Y)

Full source

/-- We can apply morphisms of concrete categories by first casting them down
to the base functions.
-/
instance {X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ ToType X → ToType Y) where
  coe f := hom f

Morphism Coercion to Functions in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, the morphisms from $X$ to $Y$ can be coerced to functions from the underlying type of $X$ to the underlying type of $Y$.

CategoryTheory.ConcreteCategory.homEquiv definition

{X Y : C} : (X ⟶ Y) ≃ ToHom X Y

Full source

/--
`ConcreteCategory.hom` bundled as an `Equiv`.
-/
def homEquiv {X Y : C} : (X ⟶ Y) ≃ ToHom X Y where
  toFun := hom
  invFun := ofHom
  left_inv := ofHom_hom
  right_inv := hom_ofHom

Equivalence between morphisms and bundled functions in a concrete category

Informal description

For any objects $ X $ and $ Y $ in a concrete category $ C $, there is a bijective equivalence between the morphisms $ X \longrightarrow Y $ and the bundled functions $ \text{ToHom} X Y $. This equivalence is given by the function $ \text{hom} $ that maps a morphism to its underlying bundled function, and its inverse $ \text{ofHom} $ that constructs a morphism from a bundled function. The equivalence satisfies $ \text{ofHom} \circ \text{hom} = \text{id} $ and $ \text{hom} \circ \text{ofHom} = \text{id} $.

CategoryTheory.ConcreteCategory.hom_bijective theorem

{X Y : C} : Function.Bijective (hom : (X ⟶ Y) → ToHom X Y)

Full source

lemma hom_bijective {X Y : C} : Function.Bijective (hom : (X ⟶ Y) → ToHom X Y) :=
  homEquiv.bijective

Bijectivity of the Morphism-to-Function Map in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, the function $\text{hom} : (X \longrightarrow Y) \to \text{ToHom} X Y$ that maps morphisms to their underlying bundled functions is bijective.

CategoryTheory.ConcreteCategory.hom_injective theorem

{X Y : C} : Function.Injective (hom : (X ⟶ Y) → ToHom X Y)

Full source

lemma hom_injective {X Y : C} : Function.Injective (hom : (X ⟶ Y) → ToHom X Y) :=
  hom_bijective.injective

Injectivity of the Morphism-to-Function Map in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, the function $\text{hom} : (X \longrightarrow Y) \to \text{ToHom} X Y$ that maps morphisms to their underlying bundled functions is injective.

CategoryTheory.ConcreteCategory.ext theorem

{X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g

Full source

/-- In any concrete category, we can test equality of morphisms by pointwise evaluations. -/
@[ext] lemma ext {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g :=
  hom_injective h

Morphism Equality via Pointwise Evaluation in Concrete Categories

Informal description

In a concrete category $C$, for any two morphisms $f, g : X \longrightarrow Y$, if their underlying bundled functions $\text{hom}(f)$ and $\text{hom}(g)$ are equal, then $f = g$.

CategoryTheory.ConcreteCategory.coe_ext theorem

{X Y : C} {f g : X ⟶ Y} (h : ⇑(hom f) = ⇑(hom g)) : f = g

Full source

lemma coe_ext {X Y : C} {f g : X ⟶ Y} (h : ⇑(hom f) = ⇑(hom g)) : f = g :=
  ext (DFunLike.coe_injective h)

Morphism Equality via Function Equality in Concrete Categories

Informal description

In a concrete category $ C $, for any two morphisms $ f, g : X \longrightarrow Y $, if the underlying functions $ \text{hom}(f) $ and $ \text{hom}(g) $ are equal, then $ f = g $.

CategoryTheory.ConcreteCategory.ext_apply theorem

{X Y : C} {f g : X ⟶ Y} (h : ∀ x, f x = g x) : f = g

Full source

lemma ext_apply {X Y : C} {f g : X ⟶ Y} (h : ∀ x, f x = g x) : f = g :=
  ext (DFunLike.ext _ _ h)

Morphism Equality via Pointwise Evaluation in Concrete Categories

Informal description

In a concrete category $C$, for any two morphisms $f, g : X \longrightarrow Y$, if $f(x) = g(x)$ for all $x$ in the underlying type of $X$, then $f = g$.

CategoryTheory.ConcreteCategory.toHasForget instance

: HasForget C

Full source

/-- A concrete category comes with a forgetful functor to `Type`.

Warning: because of the way that `ConcreteCategory` and `HasForget` are set up, we can't make
`forget Type` reducibly defeq to the identity functor. -/
instance toHasForget : HasForget C where
  forget.obj := ToType
  forget.map f := ⇑(hom f)
  forget_faithful.map_injective h := coe_ext h

Forgetful Functor from Concrete Categories to Types

Informal description

Every concrete category $C$ has a canonical forgetful functor to the category of types.

CategoryTheory.forget_obj theorem

(X : C) : (forget C).obj X = ToType X

Full source

theorem forget_obj (X : C) : (forget C).obj X = ToType X := by
  with_reducible_and_instances rfl

Forgetful Functor Preserves Underlying Type in Concrete Categories

Informal description

For any object $X$ in a concrete category $C$, the underlying type of $X$ under the forgetful functor is equal to the type associated with $X$ via the `ToType` conversion, i.e., $\text{forget}(C)(X) = \text{ToType}(X)$.

CategoryTheory.ConcreteCategory.forget_map_eq_coe theorem

{X Y : C} (f : X ⟶ Y) : (forget C).map f = f

Full source

@[simp]
theorem ConcreteCategory.forget_map_eq_coe {X Y : C} (f : X ⟶ Y) : (forget C).map f = f := by
  with_reducible_and_instances rfl

Forgetful Functor Preserves Morphisms in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, and any morphism $f \colon X \to Y$, the image of $f$ under the forgetful functor equals $f$ itself when viewed as a function between the underlying types.

CategoryTheory.congr_fun theorem

{X Y : C} {f g : X ⟶ Y} (h : f = g) (x : ToType X) : f x = g x

Full source

/-- Analogue of `congr_fun h x`,
when `h : f = g` is an equality between morphisms in a concrete category.
-/
protected theorem congr_fun {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : ToType X) : f x = g x :=
  congrFun (congrArg (fun k : X ⟶ Y => (k : ToType X → ToType Y)) h) x

Function Equality Implies Pointwise Equality in Concrete Categories

Informal description

Let $C$ be a concrete category, and let $X, Y$ be objects in $C$. For any morphisms $f, g \colon X \to Y$ such that $f = g$, and for any element $x$ of the underlying type of $X$, we have $f(x) = g(x)$.

CategoryTheory.congr_arg theorem

{X Y : C} (f : X ⟶ Y) {x x' : ToType X} (h : x = x') : f x = f x'

Full source

/-- Analogue of `congr_arg f h`,
when `h : x = x'` is an equality between elements of objects in a concrete category.
-/
protected theorem congr_arg {X Y : C} (f : X ⟶ Y) {x x' : ToType X} (h : x = x') : f x = f x' :=
  congrArg (f : ToType X → ToType Y) h

Congruence of Morphisms on Equal Elements in a Concrete Category

Informal description

Let $C$ be a concrete category, and let $X, Y$ be objects in $C$. For any morphism $f \colon X \to Y$ and any elements $x, x'$ of the underlying type of $X$ such that $x = x'$, we have $f(x) = f(x')$.

CategoryTheory.hom_id theorem

{X : C} : (𝟙 X : ToType X → ToType X) = id

Full source

theorem hom_id {X : C} : (𝟙 X : ToType X → ToType X) = id :=
  (forget _).map_id X

Identity Morphism Corresponds to Identity Function in Concrete Categories

Informal description

For any object $X$ in a concrete category $C$, the identity morphism $\mathrm{id}_X \colon X \to X$ corresponds to the identity function $\mathrm{id} \colon \mathrm{ToType}(X) \to \mathrm{ToType}(X)$ on the underlying type of $X$.

CategoryTheory.hom_comp theorem

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : ToType X → ToType Z) = g ∘ f

Full source

theorem hom_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : ToType X → ToType Z) = g ∘ f :=
  (forget _).map_comp f g

Composition of Morphisms in Concrete Categories Corresponds to Function Composition

Informal description

Let $C$ be a concrete category, and let $X, Y, Z$ be objects in $C$. For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, the composition of morphisms $f \gg g$ corresponds to the function composition $g \circ f$ on the underlying types. That is, $(f \gg g)(x) = g(f(x))$ for all $x$ in the underlying type of $X$.

CategoryTheory.coe_toHasForget_instFunLike theorem

 {C : Type*} [Category C] {FC : C → C → Type*} {CC : C → Type*} [inst : ∀ X Y : C, FunLike (FC X Y) (CC X) (CC Y)]
  [ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) :
  @DFunLike.coe (X ⟶ Y) (ToType X) (fun _ => ToType Y) HasForget.instFunLike f = f

Full source

/-- Using the `FunLike` coercion of `HasForget` does the same as the original coercion.
-/
theorem coe_toHasForget_instFunLike {C : Type*} [Category C] {FC : C → C → Type*} {CC : C → Type*}
    [inst : ∀ X Y : C, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C}
    (f : X ⟶ Y) :
    @DFunLike.coe (X ⟶ Y) (ToType X) (fun _ => ToType Y) HasForget.instFunLike f = f := rfl

Forgetful Functor Coercion is Identity on Morphisms in Concrete Categories

Informal description

For any objects $X$ and $Y$ in a concrete category $C$, the function-like coercion of a morphism $f : X \to Y$ via the forgetful functor equals $f$ itself. In other words, the coercion map from $\mathrm{Hom}(X, Y)$ to functions $X \to Y$ is the identity on morphisms.

CategoryTheory.ConcreteCategory.forget₂_comp_apply theorem

 {C : Type u} {D : Type u'} [Category.{v} C] {FC : C → C → Type*} {CC : C → Type w}
  [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{w} C FC] [Category.{v'} D] {FD : D → D → Type*}
  {CD : D → Type w} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD] [HasForget₂ C D] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (x : ToType ((forget₂ C D).obj X)) :
  ((forget₂ C D).map (f ≫ g) x) = (forget₂ C D).map g ((forget₂ C D).map f x)

Full source

lemma ConcreteCategory.forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C]
    {FC : C → C → Type*} {CC : C → Type w} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
    [ConcreteCategory.{w} C FC] [Category.{v'} D] {FD : D → D → Type*} {CD : D → Type w}
    [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD] [HasForget₂ C D] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) (x : ToType ((forget₂ C D).obj X)) :
    ((forget₂ C D).map (f ≫ g) x) =
      (forget₂ C D).map g ((forget₂ C D).map f x) := by
  rw [Functor.map_comp, ConcreteCategory.comp_apply]

Functoriality of Forgetful Functor Composition in Concrete Categories

Informal description

Let $C$ and $D$ be concrete categories with forgetful functors to the category of types, and let $\text{forget}_2 : C \to D$ be a forgetful functor between them. For any morphisms $f : X \to Y$ and $g : Y \to Z$ in $C$, and any element $x$ in the underlying type of $\text{forget}_2(X)$, the following equality holds: \[ \text{forget}_2(f \circ g)(x) = \text{forget}_2(g)(\text{forget}_2(f)(x)). \]

CategoryTheory.hom_isIso instance

{X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso (C := Type _) ⇑(ConcreteCategory.hom f)

Full source

instance hom_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] :
    IsIso (C := Type _) ⇑(ConcreteCategory.hom f) :=
  ((forget C).mapIso (asIso f)).isIso_hom

Underlying Function of an Isomorphism is an Isomorphism

Informal description

For any isomorphism $f : X \to Y$ in a concrete category $C$, the underlying function $\text{hom}(f)$ is an isomorphism in the category of types.

CategoryTheory.NatTrans.naturality_apply theorem

 {C D : Type*} [Category C] [Category D] {FD : D → D → Type*} {CD : D → Type*} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)]
  [ConcreteCategory D FD] {F G : C ⥤ D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : ToType (F.obj X)) :
  φ.app Y (F.map f x) = G.map f (φ.app X x)

Full source

@[simp]
lemma NatTrans.naturality_apply {C D : Type*} [Category C] [Category D] {FD : D → D → Type*}
    {CD : D → Type*} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD]
    {F G : C ⥤ D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : ToType (F.obj X)) :
    φ.app Y (F.map f x) = G.map f (φ.app X x) := by
  simpa only [Functor.map_comp] using congr_fun ((forget D).congr_map (φ.naturality f)) x

Naturality Condition for Concrete Categories: $\varphi_Y \circ F(f) = G(f) \circ \varphi_X$ on Elements

Informal description

Let $C$ and $D$ be categories where $D$ is a concrete category with forgetful functor to types. Given functors $F, G \colon C \to D$ and a natural transformation $\varphi \colon F \to G$, for any morphism $f \colon X \to Y$ in $C$ and any element $x$ in the underlying type of $F(X)$, we have: \[ \varphi_Y(F(f)(x)) = G(f)(\varphi_X(x)) \]

CategoryTheory.HasForget.toFunLike abbrev

[HasForget C] (X Y : C) : FunLike (X ⟶ Y) ((forget C).obj X) ((forget C).obj Y)

Full source

/-- Build a coercion to functions out of `HasForget`.

The intended usecase is to provide a `FunLike` instance in `HasForget.toConcreteCategory`.
See that definition for the considerations in making this an instance.

See note [reducible non-instances].
-/
abbrev HasForget.toFunLike [HasForget C] (X Y : C) :
    FunLike (X ⟶ Y) ((forget C).obj X) ((forget C).obj Y) where
  coe := (forget C).map
  coe_injective' _ _ h := Functor.Faithful.map_injective h

Function-Like Structure on Morphisms in Concrete Categories

Informal description

For any concrete category $C$ with a forgetful functor, and for any objects $X, Y$ in $C$, the hom-set $\mathrm{Hom}(X, Y)$ has a function-like structure that allows its elements to be coerced to functions from the underlying type of $X$ to the underlying type of $Y$ via the forgetful functor.

CategoryTheory.HasForget.toConcreteCategory abbrev

[HasForget C] : ConcreteCategory C (· ⟶ ·)

Full source

/-- Build a concrete category out of `HasForget`.

The intended usecase is to prove theorems referencing only `(forget C)`
and not `(forget C).obj X` nor `(forget C).map f`: those should be written
as `ToType X` and `ConcreteCategory.hom f` respectively.

See note [reducible non-instances].
-/
abbrev HasForget.toConcreteCategory [HasForget C] :
    ConcreteCategory C (· ⟶ ·) where
  hom f := f
  ofHom f := f
  id_apply := congr_fun ((forget C).map_id _)
  comp_apply _ _ := congr_fun ((forget C).map_comp _ _)

Canonical Concrete Category Structure from Forgetful Functor

Informal description

Given a concrete category $C$ with a forgetful functor, there exists a canonical concrete category structure on $C$ where the morphisms between objects $X$ and $Y$ are given by the hom-set $X \to Y$.

CategoryTheory.forget_eq_ConcreteCategory_hom theorem

 [HasForget C] {X Y : C} (f : X ⟶ Y) :
  (forget C).map f = @ConcreteCategory.hom _ _ _ _ _ (HasForget.toConcreteCategory C) _ _ f

Full source

/--
Note that the `ConcreteCategory` and `HasForget` instances here differ from `forget_map_eq_coe`.
-/
theorem forget_eq_ConcreteCategory_hom [HasForget C] {X Y : C} (f : X ⟶ Y) :
    (forget C).map f = @ConcreteCategory.hom _ _ _ _ _ (HasForget.toConcreteCategory C) _ _ f := by
  with_reducible_and_instances rfl

Forgetful Functor Equals Concrete Hom Underlying Function

Informal description

For any objects $X$ and $Y$ in a concrete category $C$ with a forgetful functor, and for any morphism $f : X \to Y$, the action of the forgetful functor on $f$ equals the underlying function of $f$ as defined by the concrete category structure, i.e., $\text{Forget}(f) = f$.

CategoryTheory.Types.instFunLike abbrev

: ∀ X Y : Type u, FunLike (X ⟶ Y) X Y

Full source

/-- A `FunLike` instance on plain functions, in order to instantiate a `ConcreteCategory` structure
on the category of types.

This is not an instance (yet) because that would require a lot of downstream fixes.

See note [reducible non-instances].
-/
abbrev Types.instFunLike : ∀ X Y : Type u, FunLike (X ⟶ Y) X Y := HasForget.toFunLike _

Function-Like Structure on Morphisms in the Category of Types

Informal description

For any types $X$ and $Y$ in a universe $u$, the hom-set $\mathrm{Hom}(X, Y)$ (consisting of functions from $X$ to $Y$) has a function-like structure, meaning its elements can be coerced to functions from $X$ to $Y$.

CategoryTheory.Types.instConcreteCategory abbrev

: ConcreteCategory (Type u) (fun X Y => X ⟶ Y)

Full source

/-- The category of types is concrete, using the identity functor.

This is not an instance (yet) because that would require a lot of downstream fixes.

See note [reducible non-instances].
-/
abbrev Types.instConcreteCategory : ConcreteCategory (Type u) (fun X Y => X ⟶ Y) where
  hom f := f
  ofHom f := f

Concrete Category Structure on the Category of Types

Informal description

The category of types $\mathrm{Type}_u$ in a given universe $u$ is a concrete category, where the objects are types and the morphisms are functions between types. The forgetful functor maps each type to itself and each function to itself, preserving the categorical structure.

CategoryTheory.InducedCategory.concreteCategory instance

 {C : Type u} {D : Type u'} [Category.{v'} D] {FD : D → D → Type*} {CD : D → Type w}
  [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD] (f : C → D) :
  ConcreteCategory (InducedCategory D f) (fun X Y => FD (f X) (f Y))

Full source

instance InducedCategory.concreteCategory {C : Type u} {D : Type u'} [Category.{v'} D]
    {FD : D → D → Type*} {CD : D → Type w} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)]
    [ConcreteCategory.{w} D FD] (f : C → D) :
    ConcreteCategory (InducedCategory D f) (fun X Y => FD (f X) (f Y)) where
  hom := hom (C := D)
  ofHom := ofHom (C := D)
  hom_ofHom := hom_ofHom (C := D)
  ofHom_hom := ofHom_hom (C := D)
  comp_apply := ConcreteCategory.comp_apply (C := D)
  id_apply := ConcreteCategory.id_apply (C := D)

Concrete Category Structure on Induced Categories

Informal description

Given a concrete category $\mathcal{D}$ with objects associated to types via a forgetful functor, and a function $f : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ is also a concrete category. Here, the morphisms between objects $X$ and $Y$ in $C$ are the morphisms between $f(X)$ and $f(Y)$ in $\mathcal{D}$, and the forgetful functor maps $X$ to the type associated with $f(X)$.

CategoryTheory.FullSubcategory.concreteCategory instance

 {C : Type u} [Category.{v} C] {FC : C → C → Type*} {CC : C → Type w} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
  [ConcreteCategory.{w} C FC] (P : ObjectProperty C) : ConcreteCategory P.FullSubcategory (fun X Y => FC X.1 Y.1)

Full source

instance FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
    {FC : C → C → Type*} {CC : C → Type w} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
    [ConcreteCategory.{w} C FC]
    (P : ObjectProperty C) : ConcreteCategory P.FullSubcategory (fun X Y => FC X.1 Y.1) where
  hom := hom (C := C)
  ofHom := ofHom (C := C)
  hom_ofHom := hom_ofHom (C := C)
  ofHom_hom := ofHom_hom (C := C)
  comp_apply := ConcreteCategory.comp_apply (C := C)
  id_apply := ConcreteCategory.id_apply (C := C)

Concrete Category Structure on Full Subcategories

Informal description

For any category $C$ that is a concrete category with morphisms represented by function-like structures, and any property $P$ on the objects of $C$, the full subcategory of $C$ consisting of objects satisfying $P$ is also a concrete category. The forgetful functor for this subcategory is inherited from $C$, mapping objects to their underlying types and morphisms to their underlying functions.