Mathlib.CategoryTheory.Types

CategoryTheory.types instance

: LargeCategory (Type u)

Full source

@[to_additive existing CategoryTheory.types]
instance types : LargeCategory (Type u) where
  Hom a b := a → b
  id _ := id
  comp f g := g ∘ f

The Category of Types

Informal description

The category of types in a given universe $u$, denoted $\mathrm{Type}_u$, forms a large category where the objects are types and the morphisms are functions between types.

CategoryTheory.types_hom theorem

{α β : Type u} : (α ⟶ β) = (α → β)

Full source

theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
  rfl

Morphisms in the Category of Types are Functions

Informal description

For any types $\alpha$ and $\beta$ in the same universe $u$, the type of morphisms $\alpha \longrightarrow \beta$ in the category of types is equal to the function type $\alpha \to \beta$.

CategoryTheory.types_ext theorem

{α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g

Full source

@[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g := by
  funext x
  exact h x

Extensionality of Morphisms in the Category of Types

Informal description

For any types $\alpha$ and $\beta$ in the same universe, and any two morphisms $f, g: \alpha \to \beta$ in the category of types, if $f(a) = g(a)$ for all elements $a \in \alpha$, then $f = g$.

CategoryTheory.types_id theorem

(X : Type u) : 𝟙 X = id

Full source

theorem types_id (X : Type u) : 𝟙 X = id :=
  rfl

Identity Morphism Equals Identity Function in Type Category

Informal description

For any type $X$ in universe $u$, the identity morphism $\mathbf{1}_X$ in the category of types is equal to the identity function $\mathrm{id} : X \to X$.

CategoryTheory.types_comp theorem

{X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g = g ∘ f

Full source

theorem types_comp {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g = g ∘ f :=
  rfl

Composition in the Category of Types Equals Function Composition

Informal description

For any types $X, Y, Z$ in a universe $u$, and any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the category of types, the composition $f \gg g$ is equal to the function composition $g \circ f$.

CategoryTheory.types_id_apply theorem

(X : Type u) (x : X) : (𝟙 X : X → X) x = x

Full source

@[simp]
theorem types_id_apply (X : Type u) (x : X) : (𝟙 X : X → X) x = x :=
  rfl

Identity Morphism Acts as Identity Function in Category of Types

Informal description

For any type $X$ in universe $u$ and any element $x \in X$, the identity morphism $\mathrm{id}_X$ in the category of types satisfies $\mathrm{id}_X(x) = x$.

CategoryTheory.types_comp_apply theorem

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

Full source

@[simp]
theorem types_comp_apply {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) :=
  rfl

Composition of Functions in the Category of Types Equals Function Composition

Informal description

For any types $X, Y, Z$ in a universe $u$ and functions $f : X \to Y$, $g : Y \to Z$, the composition of morphisms $f \gg g$ in the category of types is equal to the function composition $g \circ f$, i.e., for any $x \in X$, we have $(f \gg g)(x) = g(f(x))$.

CategoryTheory.hom_inv_id_apply theorem

{X Y : Type u} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x

Full source

@[simp]
theorem hom_inv_id_apply {X Y : Type u} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x :=
  congr_fun f.hom_inv_id x

Isomorphism Inverse Property in Type Category: $f^{-1} \circ f = \text{id}_X$

Informal description

For any isomorphism $f \colon X \cong Y$ in the category of types and any element $x \in X$, applying the inverse morphism $f^{-1}$ to the forward morphism $f(x)$ yields $x$ again, i.e., $f^{-1}(f(x)) = x$.

CategoryTheory.inv_hom_id_apply theorem

{X Y : Type u} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y

Full source

@[simp]
theorem inv_hom_id_apply {X Y : Type u} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y :=
  congr_fun f.inv_hom_id y

Isomorphism Inverse Property in Type Category: $f_{\text{hom}} \circ f_{\text{inv}} = \text{id}_Y$

Informal description

For any isomorphism $f \colon X \cong Y$ in the category of types and any element $y \in Y$, applying the forward morphism $f_{\text{hom}}$ to the inverse morphism $f_{\text{inv}}$ evaluated at $y$ yields $y$ again, i.e., $f_{\text{hom}}(f_{\text{inv}}(y)) = y$.

CategoryTheory.asHom abbrev

{α β : Type u} (f : α → β) : α ⟶ β

Full source

/-- `asHom f` helps Lean type check a function as a morphism in the category `Type`. -/
abbrev asHom {α β : Type u} (f : α → β) : α ⟶ β :=
  f

Function as Morphism in Type Category

Informal description

Given types $\alpha$ and $\beta$ in universe $u$, the function $\mathrm{asHom}$ maps a function $f : \alpha \to \beta$ to a morphism $\alpha \longrightarrow \beta$ in the category of types.

CategoryTheory.term↾_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "↾" f:200 => CategoryTheory.asHom f

Type category morphism notation

Informal description

The notation `↾ f` is used to guide type checking when treating a function `f : α → β` as a morphism in the category of types. It is an abbreviation for `CategoryTheory.asHom f`.

CategoryTheory.Functor.sections definition

(F : J ⥤ Type w) : Set (∀ j, F.obj j)

Full source

/-- The sections of a functor `F : J ⥤ Type` are
the choices of a point `u j : F.obj j` for each `j`,
such that `F.map f (u j) = u j'` for every morphism `f : j ⟶ j'`.

We later use these to define limits in `Type` and in many concrete categories.
-/
def sections (F : J ⥤ Type w) : Set (∀ j, F.obj j) :=
  { u | ∀ {j j'} (f : j ⟶ j'), F.map f (u j) = u j' }

Sections of a Type-Valued Functor

Informal description

Given a functor $ F : J \to \mathrm{Type}_w $ from a category $ J $ to the category of types in universe $ w $, the sections of $ F $ are the families of elements $ u_j \in F(j) $ for each object $ j $ in $ J $, such that for every morphism $ f : j \to j' $ in $ J $, the map $ F(f) $ sends $ u_j $ to $ u_{j'} $. In other words, the sections are the consistent choices of points in the fibers of $ F $ that respect the functorial action.

CategoryTheory.Functor.sections_property theorem

{F : J ⥤ Type w} (s : (F.sections : Type _)) {j j' : J} (f : j ⟶ j') : F.map f (s.val j) = s.val j'

Full source

@[simp]
lemma sections_property {F : J ⥤ Type w} (s : (F.sections : Type _))
    {j j' : J} (f : j ⟶ j') : F.map f (s.val j) = s.val j' :=
  s.property f

Functoriality of Sections in the Category of Types

Informal description

For any functor $F \colon J \to \mathrm{Type}_w$ from a category $J$ to the category of types in universe $w$, and for any section $s$ of $F$ (i.e., a family of elements $s_j \in F(j)$ for each object $j$ in $J$), the following holds: for any morphism $f \colon j \to j'$ in $J$, the map $F(f)$ applied to $s_j$ equals $s_{j'}$.

CategoryTheory.Functor.sections_ext_iff theorem

{F : J ⥤ Type w} {x y : F.sections} : x = y ↔ ∀ j, x.val j = y.val j

Full source

lemma sections_ext_iff {F : J ⥤ Type w} {x y : F.sections} : x = y ↔ ∀ j, x.val j = y.val j :=
  Subtype.ext_iff.trans funext_iff

Equality of Functor Sections is Pointwise Equality

Informal description

For any functor $F \colon J \to \mathrm{Type}_w$ and any two sections $x, y$ of $F$, the sections $x$ and $y$ are equal if and only if for every object $j$ in $J$, the values $x_j$ and $y_j$ are equal. In other words: \[ x = y \leftrightarrow \forall j \in J, x_j = y_j. \]

CategoryTheory.Functor.sectionsFunctor definition

: (J ⥤ Type w) ⥤ Type max u w

Full source

/-- The functor which sends a functor to types to its sections. -/
@[simps]
def sectionsFunctor : (J ⥤ Type w) ⥤ Type max u w where
  obj F := F.sections
  map {F G} φ x := ⟨fun j => φ.app j (x.1 j), fun {j j'} f =>
    (congr_fun (φ.naturality f) (x.1 j)).symm.trans (by simp [x.2 f])⟩

Sections Functor for Type-Valued Functors

Informal description

The functor that takes a type-valued functor $ F : J \to \mathrm{Type}_w $ and returns the type of its sections, which are families of elements $ (u_j \in F(j))_{j \in J} $ such that for every morphism $ f : j \to j' $ in $ J $, the map $ F(f) $ sends $ u_j $ to $ u_{j'} $. Given a natural transformation $ \varphi : F \to G $ between type-valued functors, the functor maps it to the function that sends a section $ x $ of $ F $ to the section $ \langle \lambda j, \varphi_j (x_j), \dots \rangle $ of $ G $, where the omitted part ensures compatibility with morphisms in $ J $.

CategoryTheory.FunctorToTypes.map_comp_apply theorem

(f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a)

Full source

@[simp]
theorem map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) :
    (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) := by simp [types_comp]

Functoriality of Composition in the Category of Types

Informal description

For any functor $F$ from a category to the category of types, and for any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the source category, the application of $F$ to the composition $f \circ g$ evaluated at an element $a \in F(X)$ is equal to the application of $F$ to $g$ evaluated at the result of applying $F$ to $f$ evaluated at $a$. In symbols: \[ F(f \circ g)(a) = F(g)(F(f)(a)). \]

CategoryTheory.FunctorToTypes.map_id_apply theorem

(a : F.obj X) : (F.map (𝟙 X)) a = a

Full source

@[simp]
theorem map_id_apply (a : F.obj X) : (F.map (𝟙 X)) a = a := by simp [types_id]

Functoriality of Identity Morphisms in the Category of Types

Informal description

For any functor $F$ from the category of types to itself and any object $X$ in this category, the application of $F$ to the identity morphism $\mathrm{id}_X$ at an element $a \in F(X)$ satisfies $F(\mathrm{id}_X)(a) = a$.

CategoryTheory.FunctorToTypes.naturality theorem

(f : X ⟶ Y) (x : F.obj X) : σ.app Y ((F.map f) x) = (G.map f) (σ.app X x)

Full source

theorem naturality (f : X ⟶ Y) (x : F.obj X) : σ.app Y ((F.map f) x) = (G.map f) (σ.app X x) :=
  congr_fun (σ.naturality f) x

Naturality Condition for Functors on Types

Informal description

Let $F$ and $G$ be functors from the category of types to itself, and let $\sigma \colon F \to G$ be a natural transformation between them. For any morphism $f \colon X \to Y$ in the category of types and any element $x \in F(X)$, the following diagram commutes: \[ \sigma_Y(F(f)(x)) = G(f)(\sigma_X(x)). \]

CategoryTheory.FunctorToTypes.comp theorem

(x : F.obj X) : (σ ≫ τ).app X x = τ.app X (σ.app X x)

Full source

@[simp]
theorem comp (x : F.obj X) : (σ ≫ τ).app X x = τ.app X (σ.app X x) :=
  rfl

Composition of Natural Transformations in the Category of Types

Informal description

For any functor $F$ from the category of types to itself, and any natural transformations $\sigma$ and $\tau$ between functors valued in types, the application of the composition $\sigma \circ \tau$ at an object $X$ to an element $x \in F(X)$ is equal to the application of $\tau$ at $X$ to the result of applying $\sigma$ at $X$ to $x$. In symbols: $$(\sigma \circ \tau)_X(x) = \tau_X(\sigma_X(x)).$$

CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply theorem

(p : X = Y) (q : Y = Z) (x : F.obj X) : F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom <| p.trans q) x

Full source

@[simp]
theorem eqToHom_map_comp_apply (p : X = Y) (q : Y = Z) (x : F.obj X) :
    F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom <| p.trans q) x := by
  aesop_cat

Functoriality of Composition of Equality-Induced Morphisms in the Category of Types

Informal description

Let $F$ be a functor from the category of types to itself. For any equalities $p : X = Y$ and $q : Y = Z$ between types $X$, $Y$, and $Z$, and for any element $x \in F(X)$, the following holds: $$F(\text{eqToHom}(q))(F(\text{eqToHom}(p))(x)) = F(\text{eqToHom}(p \cdot q))(x).$$ Here, $\text{eqToHom}(p)$ denotes the morphism $X \to Y$ induced by the equality $p$, and $p \cdot q$ is the composition (transitivity) of the equalities $p$ and $q$.

CategoryTheory.FunctorToTypes.hcomp theorem

(x : (I ⋙ F).obj W) : (ρ ◫ σ).app W x = (G.map (ρ.app W)) (σ.app (I.obj W) x)

Full source

@[simp]
theorem hcomp (x : (I ⋙ F).obj W) : (ρ ◫ σ).app W x = (G.map (ρ.app W)) (σ.app (I.obj W) x) :=
  rfl

Horizontal Composition of Natural Transformations in Type Category

Informal description

Let $I$, $F$, $G$ be functors in the category of types, and let $\rho$ and $\sigma$ be natural transformations. For any object $W$ and any element $x$ in the object $(I \circ F)(W)$, the application of the horizontal composition $\rho \circ \sigma$ at $W$ to $x$ equals the application of $G$ to $\rho_W$ evaluated at $\sigma_{I(W)}(x)$. In symbols: $$(\rho \circ \sigma)_W(x) = G(\rho_W)(\sigma_{I(W)}(x))$$

CategoryTheory.FunctorToTypes.map_inv_map_hom_apply theorem

(f : X ≅ Y) (x : F.obj X) : F.map f.inv (F.map f.hom x) = x

Full source

@[simp]
theorem map_inv_map_hom_apply (f : X ≅ Y) (x : F.obj X) : F.map f.inv (F.map f.hom x) = x :=
  congr_fun (F.mapIso f).hom_inv_id x

Functorial Preservation of Isomorphism Inverses in Type Category

Informal description

Let $F$ be a functor from a category $\mathcal{C}$ to the category of types, and let $f : X \cong Y$ be an isomorphism in $\mathcal{C}$. For any element $x \in F(X)$, applying the functor $F$ to the inverse morphism $f^{-1}$ of the isomorphism $f$ after applying $F$ to the forward morphism $f$ of $f$ returns $x$, i.e., $F(f^{-1})(F(f)(x)) = x$.

CategoryTheory.FunctorToTypes.map_hom_map_inv_apply theorem

(f : X ≅ Y) (y : F.obj Y) : F.map f.hom (F.map f.inv y) = y

Full source

@[simp]
theorem map_hom_map_inv_apply (f : X ≅ Y) (y : F.obj Y) : F.map f.hom (F.map f.inv y) = y :=
  congr_fun (F.mapIso f).inv_hom_id y

Functorial Preservation of Isomorphism Composition in Type Category: $F(f) \circ F(f^{-1}) = \mathrm{id}$

Informal description

Let $F \colon \mathcal{C} \to \mathrm{Type}$ be a functor from a category $\mathcal{C}$ to the category of types, and let $f \colon X \cong Y$ be an isomorphism in $\mathcal{C}$. For any element $y \in F(Y)$, applying the functor $F$ to the forward morphism $f$ after applying $F$ to the inverse morphism $f^{-1}$ returns $y$, i.e., $F(f)(F(f^{-1})(y)) = y$.

CategoryTheory.FunctorToTypes.hom_inv_id_app_apply theorem

(α : F ≅ G) (X) (x) : α.inv.app X (α.hom.app X x) = x

Full source

@[simp]
theorem hom_inv_id_app_apply (α : F ≅ G) (X) (x) : α.inv.app X (α.hom.app X x) = x :=
  congr_fun (α.hom_inv_id_app X) x

Natural Isomorphism Component Identity: $\alpha.inv \circ \alpha.hom = \mathrm{id}$ on Elements

Informal description

For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to \mathrm{Type}$ and any object $X$ in $C$, applying the inverse component $\alpha.inv.app\ X$ to the result of applying the forward component $\alpha.hom.app\ X$ to an element $x \in F(X)$ yields $x$ again, i.e., $\alpha.inv.app\ X (\alpha.hom.app\ X x) = x$.

CategoryTheory.FunctorToTypes.inv_hom_id_app_apply theorem

(α : F ≅ G) (X) (x) : α.hom.app X (α.inv.app X x) = x

Full source

@[simp]
theorem inv_hom_id_app_apply (α : F ≅ G) (X) (x) : α.hom.app X (α.inv.app X x) = x :=
  congr_fun (α.inv_hom_id_app X) x

Natural Isomorphism Component Identity: $\alpha.hom \circ \alpha.inv = \mathrm{id}$ on Elements

Informal description

For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to \mathrm{Type}$ and any object $X$ in $C$, the application of the forward component $\alpha.hom.app\ X$ followed by the inverse component $\alpha.inv.app\ X$ to an element $x \in G(X)$ returns $x$, i.e., $\alpha.hom.app\ X (\alpha.inv.app\ X x) = x$.

CategoryTheory.uliftTrivial definition

(V : Type u) : ULift.{u} V ≅ V

Full source

/-- The isomorphism between a `Type` which has been `ULift`ed to the same universe,
and the original type.
-/
def uliftTrivial (V : Type u) : ULiftULift.{u} V ≅ V where
  hom a := a.1
  inv a := .up a

Isomorphism between a type and its lifted version

Informal description

The isomorphism between a type $V$ and its lifted version $\mathrm{ULift}\, V$ in the same universe, where the forward morphism extracts the underlying value and the inverse morphism lifts the value.

CategoryTheory.uliftFunctor definition

: Type u ⥤ Type max u v

Full source

/-- The functor embedding `Type u` into `Type (max u v)`.
Write this as `uliftFunctor.{5, 2}` to get `Type 2 ⥤ Type 5`.
-/
@[pp_with_univ]
def uliftFunctor : Type u ⥤ Type max u v where
  obj X := ULift.{v} X
  map {X} {_} f := fun x : ULift.{v} X => ULift.up (f x.down)

Type lifting functor

Informal description

The functor that embeds the category of types in universe $u$ into the category of types in universe $\max(u, v)$ by lifting types via the `ULift` construction. Specifically, it maps a type $X$ to $\mathrm{ULift}\, X$ and a function $f : X \to Y$ to the lifted function $\mathrm{ULift.up} \circ f \circ \mathrm{ULift.down}$.

CategoryTheory.uliftFunctor_obj theorem

{X : Type u} : uliftFunctor.obj.{v} X = ULift.{v} X

Full source

@[simp]
theorem uliftFunctor_obj {X : Type u} : uliftFunctor.obj.{v} X = ULift.{v} X :=
  rfl

Object Mapping of Type Lifting Functor: $\mathrm{uliftFunctor}.obj\, X = \mathrm{ULift}\, X$

Informal description

For any type $X$ in universe $u$, the object obtained by applying the type lifting functor $\mathrm{uliftFunctor}$ to $X$ is equal to the lifted type $\mathrm{ULift}\, X$ in universe $\max(u,v)$.

CategoryTheory.uliftFunctor_map theorem

{X Y : Type u} (f : X ⟶ Y) (x : ULift.{v} X) : uliftFunctor.map f x = ULift.up (f x.down)

Full source

@[simp]
theorem uliftFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : ULift.{v} X) :
    uliftFunctor.map f x = ULift.up (f x.down) :=
  rfl

Action of Type Lifting Functor on Morphisms

Informal description

For any types $X$ and $Y$ in universe $u$, and any morphism $f : X \to Y$ in the category of types, the action of the type lifting functor on $f$ applied to a lifted element $x \in \mathrm{ULift}\, X$ is given by $\mathrm{uliftFunctor}.map\, f\, x = \mathrm{ULift.up}\, (f\, x.\mathrm{down})$.

CategoryTheory.uliftFunctor_full instance

: Functor.Full.{u} uliftFunctor

Full source

instance uliftFunctor_full : Functor.Full.{u} uliftFunctor where
  map_surjective f := ⟨fun x => (f (ULift.up x)).down, rfl⟩

Fullness of the Type Lifting Functor

Informal description

The type lifting functor $\mathrm{uliftFunctor} : \mathrm{Type}_u \to \mathrm{Type}_{\max(u,v)}$ is full. That is, for any types $X$ and $Y$ in universe $u$, every morphism $g : \mathrm{ULift}\, X \to \mathrm{ULift}\, Y$ in $\mathrm{Type}_{\max(u,v)}$ is of the form $\mathrm{uliftFunctor}.map\, f$ for some morphism $f : X \to Y$ in $\mathrm{Type}_u$.

CategoryTheory.uliftFunctor_faithful instance

: uliftFunctor.Faithful

Full source

instance uliftFunctor_faithful : uliftFunctor.Faithful where
  map_injective {_X} {_Y} f g p :=
    funext fun x =>
      congr_arg ULift.down (congr_fun p (ULift.up x) : ULift.up (f x) = ULift.up (g x))

Faithfulness of the Type Lifting Functor

Informal description

The type lifting functor $\mathrm{uliftFunctor} : \mathrm{Type}_u \to \mathrm{Type}_{\max(u,v)}$ is faithful. That is, for any types $X$ and $Y$ in universe $u$, if two morphisms $f, g : X \to Y$ in $\mathrm{Type}_u$ satisfy $\mathrm{uliftFunctor}.map\, f = \mathrm{uliftFunctor}.map\, g$, then $f = g$.

CategoryTheory.uliftFunctorTrivial definition

: uliftFunctor.{u, u} ≅ 𝟭 _

Full source

/-- The functor embedding `Type u` into `Type u` via `ULift` is isomorphic to the identity functor.
-/
def uliftFunctorTrivial : uliftFunctoruliftFunctor.{u, u}uliftFunctor.{u, u} ≅ 𝟭 _ :=
  NatIso.ofComponents uliftTrivial

Isomorphism between type lifting functor and identity functor in the same universe

Informal description

The functor that lifts types in universe $u$ to the same universe via `ULift` is isomorphic to the identity functor on the category of types in universe $u$. Specifically, this isomorphism is constructed using the natural isomorphism `uliftTrivial` which provides component-wise isomorphisms between a type and its lifted version.

CategoryTheory.homOfElement definition

{X : Type u} (x : X) : PUnit ⟶ X

Full source

/-- Any term `x` of a type `X` corresponds to a morphism `PUnit ⟶ X`. -/
def homOfElement {X : Type u} (x : X) : PUnitPUnit ⟶ X := fun _ => x

Morphism from terminal object induced by an element

Informal description

For any type $X$ and element $x \in X$, the function `homOfElement x` maps the unique element of the terminal object `PUnit` to $x$, representing a morphism from the terminal object to $X$ in the category of types.

CategoryTheory.homOfElement_eq_iff theorem

{X : Type u} (x y : X) : homOfElement x = homOfElement y ↔ x = y

Full source

theorem homOfElement_eq_iff {X : Type u} (x y : X) : homOfElementhomOfElement x = homOfElement y ↔ x = y :=
  ⟨fun H => congr_fun H PUnit.unit, by aesop⟩

Equality of Terminal Morphisms Induced by Elements

Informal description

For any type $X$ and elements $x, y \in X$, the morphisms $\mathrm{homOfElement}\,x$ and $\mathrm{homOfElement}\,y$ from the terminal object to $X$ are equal if and only if $x = y$.

CategoryTheory.mono_iff_injective theorem

{X Y : Type u} (f : X ⟶ Y) : Mono f ↔ Function.Injective f

Full source

/-- A morphism in `Type` is a monomorphism if and only if it is injective. -/
@[stacks 003C]
theorem mono_iff_injective {X Y : Type u} (f : X ⟶ Y) : MonoMono f ↔ Function.Injective f := by
  constructor
  · intro H x x' h
    rw [← homOfElement_eq_iff] at h ⊢
    exact (cancel_mono f).mp h
  · exact fun H => ⟨fun g g' h => H.comp_left h⟩

Monomorphisms in Type Category are Injective Functions

Informal description

For any function $f \colon X \to Y$ between types $X$ and $Y$ in a fixed universe, $f$ is a monomorphism in the category of types if and only if $f$ is injective.

CategoryTheory.injective_of_mono theorem

{X Y : Type u} (f : X ⟶ Y) [hf : Mono f] : Function.Injective f

Full source

theorem injective_of_mono {X Y : Type u} (f : X ⟶ Y) [hf : Mono f] : Function.Injective f :=
  (mono_iff_injective f).1 hf

Monomorphisms in Type Category are Injective

Informal description

For any function $f \colon X \to Y$ between types $X$ and $Y$ in a fixed universe, if $f$ is a monomorphism in the category of types, then $f$ is injective.

CategoryTheory.epi_iff_surjective theorem

{X Y : Type u} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f

Full source

/-- A morphism in `Type` is an epimorphism if and only if it is surjective. -/
@[stacks 003C]
theorem epi_iff_surjective {X Y : Type u} (f : X ⟶ Y) : EpiEpi f ↔ Function.Surjective f := by
  constructor
  · rintro ⟨H⟩
    refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_
    rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]
    apply H
    change ULift.upULift.up ∘ g₁ ∘ f = ULift.upULift.up ∘ g₂ ∘ f
    rw [hg]
  · exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩

Epimorphisms in Type Category are Surjective Functions

Informal description

For any function $f \colon X \to Y$ between types $X$ and $Y$ in a fixed universe, $f$ is an epimorphism in the category of types if and only if $f$ is surjective.

CategoryTheory.surjective_of_epi theorem

{X Y : Type u} (f : X ⟶ Y) [hf : Epi f] : Function.Surjective f

Full source

theorem surjective_of_epi {X Y : Type u} (f : X ⟶ Y) [hf : Epi f] : Function.Surjective f :=
  (epi_iff_surjective f).1 hf

Epimorphisms in Type Category are Surjective

Informal description

For any function $f \colon X \to Y$ between types $X$ and $Y$ in a fixed universe, if $f$ is an epimorphism in the category of types, then $f$ is surjective.

CategoryTheory.ofTypeFunctor definition

(m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] : Type u ⥤ Type v

Full source

/-- `ofTypeFunctor m` converts from Lean's `Type`-based `Category` to `CategoryTheory`. This
allows us to use these functors in category theory. -/
def ofTypeFunctor (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] : Type u ⥤ Type v where
  obj := m
  map f := Functor.map f
  map_id := fun α => by funext X; apply id_map

Functor from Type to Type induced by a type constructor

Informal description

The definition `ofTypeFunctor m` constructs a functor from the category of types in universe $u$ to the category of types in universe $v$, given a type constructor `m : Type u → Type v` that is equipped with a lawful functor instance. The functor maps objects via `m` and morphisms via the `Functor.map` operation of `m$.

CategoryTheory.ofTypeFunctor_obj theorem

: (ofTypeFunctor m).obj = m

Full source

@[simp]
theorem ofTypeFunctor_obj : (ofTypeFunctor m).obj = m :=
  rfl

Object Mapping of `ofTypeFunctor` Equals Type Constructor

Informal description

The object mapping of the functor `ofTypeFunctor m` is equal to the type constructor `m`, i.e., $(ofTypeFunctor\, m).obj = m$.

CategoryTheory.ofTypeFunctor_map theorem

{α β} (f : α → β) : (ofTypeFunctor m).map f = (Functor.map f : m α → m β)

Full source

@[simp]
theorem ofTypeFunctor_map {α β} (f : α → β) :
    (ofTypeFunctor m).map f = (Functor.map f : m α → m β) :=
  rfl

Functoriality of `ofTypeFunctor`'s Morphism Mapping

Informal description

For any types $\alpha$ and $\beta$ in universe $u$, and any function $f : \alpha \to \beta$, the morphism mapping of the functor `ofTypeFunctor m` at $f$ is equal to the functorial mapping of $f$ under the type constructor $m$, i.e., $(ofTypeFunctor\, m).map\, f = Functor.map\, f$ as functions from $m\,\alpha$ to $m\,\beta$.

Equiv.toIso definition

(e : X ≃ Y) : X ≅ Y

Full source

/-- Any equivalence between types in the same universe gives
a categorical isomorphism between those types.
-/
def toIso (e : X ≃ Y) : X ≅ Y where
  hom := e.toFun
  inv := e.invFun
  hom_inv_id := funext e.left_inv
  inv_hom_id := funext e.right_inv

Equivalence induces isomorphism in the category of types

Informal description

Given an equivalence $e : X \simeq Y$ between types $X$ and $Y$ in the same universe, the function `Equiv.toIso` constructs a categorical isomorphism $X \cong Y$ where: - The forward morphism is given by $e$'s underlying function $e : X \to Y$ - The inverse morphism is given by $e$'s inverse function $e^{-1} : Y \to X$ - The composition laws follow from $e$ being an equivalence (with left and right inverse properties)

Equiv.toIso_hom theorem

{e : X ≃ Y} : e.toIso.hom = e

Full source

@[simp]
theorem toIso_hom {e : X ≃ Y} : e.toIso.hom = e :=
  rfl

Forward Morphism of Equivalence-Induced Isomorphism

Informal description

For any equivalence $e : X \simeq Y$ between types $X$ and $Y$, the forward morphism component of the induced isomorphism $e.toIso$ is equal to $e$ itself.

Equiv.toIso_inv theorem

{e : X ≃ Y} : e.toIso.inv = e.symm

Full source

@[simp]
theorem toIso_inv {e : X ≃ Y} : e.toIso.inv = e.symm :=
  rfl

Inverse Morphism of Equivalence-Induced Isomorphism Equals Equivalence Inverse

Informal description

For any equivalence $e \colon X \simeq Y$ between types $X$ and $Y$, the inverse morphism component of the induced isomorphism $e.\text{toIso}$ is equal to the inverse function $e^{-1}$ of the equivalence.

CategoryTheory.Iso.toEquiv definition

(i : X ≅ Y) : X ≃ Y

Full source

/-- Any isomorphism between types gives an equivalence. -/
def toEquiv (i : X ≅ Y) : X ≃ Y where
  toFun := i.hom
  invFun := i.inv
  left_inv x := congr_fun i.hom_inv_id x
  right_inv y := congr_fun i.inv_hom_id y

Isomorphism to Equivalence in Type Category

Informal description

Given an isomorphism $i$ between types $X$ and $Y$ in the category of types, the function constructs an equivalence (i.e., a bijection) between $X$ and $Y$ where: - The forward map is the morphism component of $i$, - The inverse map is the inverse morphism component of $i$, - The left inverse property follows from the isomorphism's left inverse condition, - The right inverse property follows from the isomorphism's right inverse condition.

CategoryTheory.Iso.toEquiv_fun theorem

(i : X ≅ Y) : (i.toEquiv : X → Y) = i.hom

Full source

@[simp]
theorem toEquiv_fun (i : X ≅ Y) : (i.toEquiv : X → Y) = i.hom :=
  rfl

Equivalence Function of an Isomorphism in Type Category Matches Its Homomorphism

Informal description

For any isomorphism $i \colon X \cong Y$ in the category of types, the underlying function of the equivalence $i.\text{toEquiv} \colon X \to Y$ is equal to the homomorphism component $i.\text{hom}$ of the isomorphism.

CategoryTheory.Iso.toEquiv_symm_fun theorem

(i : X ≅ Y) : (i.toEquiv.symm : Y → X) = i.inv

Full source

@[simp]
theorem toEquiv_symm_fun (i : X ≅ Y) : (i.toEquiv.symm : Y → X) = i.inv :=
  rfl

Inverse Equivalence Function of an Isomorphism Matches Its Inverse Morphism

Informal description

For any isomorphism $i \colon X \cong Y$ in the category of types, the underlying function of the inverse equivalence $i.\text{toEquiv}.\text{symm} \colon Y \to X$ is equal to the inverse morphism component $i.\text{inv}$ of the isomorphism.

CategoryTheory.Iso.toEquiv_id theorem

(X : Type u) : (Iso.refl X).toEquiv = Equiv.refl X

Full source

@[simp]
theorem toEquiv_id (X : Type u) : (Iso.refl X).toEquiv = Equiv.refl X :=
  rfl

Identity Isomorphism Yields Identity Equivalence in Type Category

Informal description

For any type $X$ in a universe $u$, the equivalence obtained from the identity isomorphism on $X$ is equal to the identity equivalence on $X$. That is, $(\text{Iso.refl } X).\text{toEquiv} = \text{Equiv.refl } X$.

CategoryTheory.Iso.toEquiv_comp theorem

{X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) : (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv

Full source

@[simp]
theorem toEquiv_comp {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) :
    (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv :=
  rfl

Composition of Isomorphisms Preserves Equivalence in the Category of Types

Informal description

For any types $X$, $Y$, and $Z$ in a universe $u$, and given isomorphisms $f \colon X \cong Y$ and $g \colon Y \cong Z$ in the category of types, the equivalence obtained from the composition $f \ggg g$ is equal to the composition of the equivalences obtained from $f$ and $g$. That is, $(f \ggg g).toEquiv = f.toEquiv \circ g.toEquiv$.

CategoryTheory.isIso_iff_bijective theorem

{X Y : Type u} (f : X ⟶ Y) : IsIso f ↔ Function.Bijective f

Full source

/-- A morphism in `Type u` is an isomorphism if and only if it is bijective. -/
theorem isIso_iff_bijective {X Y : Type u} (f : X ⟶ Y) : IsIsoIsIso f ↔ Function.Bijective f :=
  Iff.intro (fun _ => (asIso f : X ≅ Y).toEquiv.bijective) fun b =>
    (Equiv.ofBijective f b).toIso.isIso_hom

Isomorphism in Type Category is Equivalent to Bijective Function

Informal description

For any types $X$ and $Y$ in the same universe, a function $f : X \to Y$ is an isomorphism in the category of types if and only if $f$ is bijective.

CategoryTheory.instSplitEpiCategoryType instance

: SplitEpiCategory (Type u)

Full source

instance : SplitEpiCategory (Type u) where
  isSplitEpi_of_epi f hf :=
    IsSplitEpi.mk' <|
      { section_ := Function.surjInv <| (epi_iff_surjective f).1 hf
        id := funext <| Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf }

Split Epimorphisms in the Category of Types

Informal description

The category of types $\mathrm{Type}_u$ in a given universe $u$ is a split epi category, meaning every epimorphism in this category has a right inverse.

equivIsoIso definition

{X Y : Type u} : X ≃ Y ≅ X ≅ Y

Full source

/-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
of types. -/
@[simps]
def equivIsoIso {X Y : Type u} : X ≃ YX ≃ Y ≅ X ≅ Y where
  hom e := e.toIso
  inv i := i.toEquiv

Equivalence-Iso Correspondence in Type Category

Informal description

For any types $X$ and $Y$ in the same universe, there is a natural isomorphism between the type of equivalences $X \simeq Y$ and the type of categorical isomorphisms $X \cong Y$ in the category of types. This isomorphism is given by: - The forward map sends an equivalence $e: X \simeq Y$ to its corresponding categorical isomorphism $e.toIso$ - The inverse map sends a categorical isomorphism $i: X \cong Y$ to its corresponding equivalence $i.toEquiv$

equivEquivIso definition

{X Y : Type u} : X ≃ Y ≃ (X ≅ Y)

Full source

/-- Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms
of types. -/
def equivEquivIso {X Y : Type u} : X ≃ YX ≃ Y ≃ (X ≅ Y) :=
  equivIsoIso.toEquiv

Equivalence between Equivalences and Isomorphisms in Type Category

Informal description

For any types $X$ and $Y$ in the same universe, there is a natural equivalence between the type of equivalences $X \simeq Y$ and the type of categorical isomorphisms $X \cong Y$ in the category of types. This equivalence is given by: - The forward map sends an equivalence $e: X \simeq Y$ to its corresponding categorical isomorphism $e.toIso$ - The inverse map sends a categorical isomorphism $i: X \cong Y$ to its corresponding equivalence $i.toEquiv$

equivEquivIso_hom theorem

{X Y : Type u} (e : X ≃ Y) : equivEquivIso e = e.toIso

Full source

@[simp]
theorem equivEquivIso_hom {X Y : Type u} (e : X ≃ Y) : equivEquivIso e = e.toIso :=
  rfl

Homomorphism Component of Equivalence-Isomorphism Correspondence

Informal description

For any types $X$ and $Y$ in the same universe, and for any equivalence $e : X \simeq Y$, the application of the equivalence `equivEquivIso` to $e$ yields the categorical isomorphism $e.toIso$.

equivEquivIso_inv theorem

{X Y : Type u} (e : X ≅ Y) : equivEquivIso.symm e = e.toEquiv

Full source

@[simp]
theorem equivEquivIso_inv {X Y : Type u} (e : X ≅ Y) : equivEquivIso.symm e = e.toEquiv :=
  rfl

Inverse of `equivEquivIso` equals `toEquiv` for isomorphisms in the category of types

Informal description

For any types $X$ and $Y$ in the same universe, and for any isomorphism $e : X \cong Y$ in the category of types, the inverse of the equivalence `equivEquivIso` applied to $e$ is equal to the equivalence obtained from $e$ via `toEquiv`.