doc-next-gen

Mathlib.CategoryTheory.Discrete.Basic

Module docstring

{"# Discrete categories

We define Discrete α as a structure containing a term a : α for any type α, and use this type alias to provide a SmallCategory instance whose only morphisms are the identities.

There is an annoying technical difficulty that it has turned out to be inconvenient to allow categories with morphisms living in Prop, so instead of defining X ⟶ Y in Discrete α as X = Y, one might define it as PLift (X = Y). In fact, to allow Discrete α to be a SmallCategory (i.e. with morphisms in the same universe as the objects), we actually define the hom type X ⟶ Y as ULift (PLift (X = Y)).

Discrete.functor promotes a function f : I → C (for any category C) to a functor Discrete.functor f : Discrete I ⥤ C.

Similarly, Discrete.natTrans and Discrete.natIso promote I-indexed families of morphisms, or I-indexed families of isomorphisms to natural transformations or natural isomorphism.

We show equivalences of types are the same as (categorical) equivalences of the corresponding discrete categories. "}

CategoryTheory.Discrete structure
(α : Type u₁)
Full source 
/-- A wrapper for promoting any type to a category,
with the only morphisms being equalities.
-/
@[ext, aesop safe cases (rule_sets := [CategoryTheory])]
structure Discrete (α : Type u₁) where
  /-- A wrapper for promoting any type to a category,
  with the only morphisms being equalities. -/
  as : α
Discrete category over a type
Informal description
The structure `Discrete α` represents a category where the objects are elements of a type `α` and the only morphisms are the identity morphisms. This is achieved by defining the hom type between two objects `X` and `Y` as `ULift (PLift (X = Y))`, ensuring that the category is small (i.e., morphisms live in the same universe as the objects).
CategoryTheory.Discrete.mk_as theorem
{α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X
Full source 
@[simp]
theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X := by
  rfl
Identity of Discrete Category Construction
Informal description
For any object $X$ in the discrete category over a type $\alpha$, the construction `Discrete.mk` applied to the underlying element `X.as` yields $X$ itself, i.e., $\text{Discrete.mk}(X.\text{as}) = X$.
CategoryTheory.discreteEquiv definition
{α : Type u₁} : Discrete α ≃ α
Full source 
/-- `Discrete α` is equivalent to the original type `α`. -/
@[simps]
def discreteEquiv {α : Type u₁} : DiscreteDiscrete α ≃ α where
  toFun := Discrete.as
  invFun := Discrete.mk
  left_inv := by aesop_cat
  right_inv := by aesop_cat
Equivalence between discrete category and its base type
Informal description
The equivalence between the discrete category over a type $\alpha$ and the original type $\alpha$, where the forward map extracts the underlying element and the inverse map constructs an object in the discrete category.
CategoryTheory.instDecidableEqDiscrete instance
{α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α)
Full source 
instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) :=
  discreteEquiv.decidableEq
Decidable Equality in Discrete Categories
Informal description
For any type $\alpha$ with decidable equality, the discrete category $\mathrm{Discrete}\,\alpha$ also has decidable equality.
CategoryTheory.discreteCategory instance
(α : Type u₁) : SmallCategory (Discrete α)
Full source 
/-- The "Discrete" category on a type, whose morphisms are equalities.

Because we do not allow morphisms in `Prop` (only in `Type`),
somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`. -/
@[stacks 001A]
instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) where
  Hom X Y := ULift (PLift (X.as = Y.as))
  id _ := ULift.up (PLift.up rfl)
  comp {X Y Z} g f := by
    cases X
    cases Y
    cases Z
    rcases f with ⟨⟨⟨⟩⟩⟩
    exact g
Discrete Category as a Small Category
Informal description
For any type $\alpha$, the discrete category $\mathrm{Discrete}\,\alpha$ is a small category where the only morphisms are the identity morphisms. Specifically, the hom type between two objects $X$ and $Y$ is defined as $\mathrm{ULift}\,(\mathrm{PLift}\,(X = Y))$, ensuring that the category is small (i.e., morphisms live in the same universe as the objects).
CategoryTheory.Discrete.instInhabited instance
[Inhabited α] : Inhabited (Discrete α)
Full source 
instance [Inhabited α] : Inhabited (Discrete α) :=
  ⟨⟨default⟩⟩
Inhabited Discrete Category
Informal description
For any inhabited type $\alpha$, the discrete category $\mathrm{Discrete}\,\alpha$ is also inhabited.
CategoryTheory.Discrete.instSubsingleton instance
[Subsingleton α] : Subsingleton (Discrete α)
Full source 
instance [Subsingleton α] : Subsingleton (Discrete α) :=
  ⟨by aesop_cat⟩
Discrete Category of a Subsingleton is a Subsingleton
Informal description
For any type $\alpha$ that is a subsingleton (i.e., has at most one element), the discrete category $\mathrm{Discrete}\,\alpha$ is also a subsingleton.
CategoryTheory.Discrete.instSubsingletonDiscreteHom instance
(X Y : Discrete α) : Subsingleton (X ⟶ Y)
Full source 
instance instSubsingletonDiscreteHom (X Y : Discrete α) : Subsingleton (X ⟶ Y) :=
  show Subsingleton (ULift (PLift _)) from inferInstance
Subsingleton Property of Morphisms in Discrete Categories
Informal description
For any objects $X$ and $Y$ in the discrete category over a type $\alpha$, the hom-set $\mathrm{Hom}(X, Y)$ is a subsingleton (i.e., it has at most one morphism).
CategoryTheory.Discrete.tacticDiscrete_cases definition
: Lean.ParserDescr✝
Full source 
macromacro "discrete_cases" : tactic =>
  `(tactic| fail_if_no_progress casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
Discrete cases tactic
Informal description
The tactic `discrete_cases` performs case analysis on any hypotheses of type `Discrete α` or morphisms between objects in the discrete category. It uses the `cases` tactic to decompose these hypotheses into their constituent parts.
CategoryTheory.Discrete.discreteCases definition
: TacticM Unit
Full source 
/--
Use:
```
attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
  CategoryTheory.Discrete.discreteCases
```
to locally gives `aesop_cat` the ability to call `cases` on
`Discrete` and `(_ : Discrete _) ⟶ (_ : Discrete _)` hypotheses.
-/
def discreteCases : TacticM Unit := do
  evalTacticevalTactic (← `(tactic| discrete_cases))
Case analysis tactic for discrete categories
Informal description
The tactic `discreteCases` is used to perform case analysis on hypotheses involving the `Discrete` type and morphisms between objects in the `Discrete` category. It enables automated reasoning tools like `aesop_cat` to break down goals involving discrete categories by cases.
CategoryTheory.Discrete.instUnique instance
[Unique α] : Unique (Discrete α)
Full source 
instance [Unique α] : Unique (Discrete α) :=
  Unique.mk' (Discrete α)
Unique Objects in Discrete Categories from Unique Types
Informal description
For any type $\alpha$ with a unique element, the discrete category $\mathrm{Discrete}\,\alpha$ also has a unique object.
CategoryTheory.Discrete.eqToHom abbrev
{X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y
Full source 
/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to a morphism `X ⟶ Y`
in the discrete category. -/
protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
  eqToHom (by aesop_cat)
Morphism from Equality of Underlying Elements in Discrete Category
Informal description
Given two objects $X$ and $Y$ in the discrete category over a type $\alpha$, and an equality $h : X.\mathrm{as} = Y.\mathrm{as}$ between their underlying elements, the function constructs a morphism $X \to Y$ in the discrete category.
CategoryTheory.Discrete.eqToIso abbrev
{X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y
Full source 
/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to an isomorphism `X ≅ Y`
in the discrete category. -/
protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
  eqToIso (by aesop_cat)
Isomorphism from Equality in Discrete Category
Informal description
Given objects $X$ and $Y$ in the discrete category over type $\alpha$, and an equality $h$ between their underlying elements $X.\mathrm{as} = Y.\mathrm{as}$, the function constructs an isomorphism $X \cong Y$ in the discrete category.
CategoryTheory.Discrete.eqToHom' abbrev
{a b : α} (h : a = b) : Discrete.mk a ⟶ Discrete.mk b
Full source 
/-- A variant of `eqToHom` that lifts terms to the discrete category. -/
abbrev eqToHom' {a b : α} (h : a = b) : Discrete.mkDiscrete.mk a ⟶ Discrete.mk b :=
  Discrete.eqToHom h
Morphism from Equality in Discrete Category (Unpacked Version)
Informal description
Given two elements $a$ and $b$ of a type $\alpha$ and an equality $h : a = b$, the function constructs a morphism from the object $\mathrm{Discrete.mk}\,a$ to $\mathrm{Discrete.mk}\,b$ in the discrete category over $\alpha$.
CategoryTheory.Discrete.eqToIso' abbrev
{a b : α} (h : a = b) : Discrete.mk a ≅ Discrete.mk b
Full source 
/-- A variant of `eqToIso` that lifts terms to the discrete category. -/
abbrev eqToIso' {a b : α} (h : a = b) : Discrete.mkDiscrete.mk a ≅ Discrete.mk b :=
  Discrete.eqToIso h
Isomorphism from Equality in Discrete Category (Unbundled Version)
Informal description
Given elements $a$ and $b$ of a type $\alpha$ and an equality $h : a = b$, the function constructs an isomorphism $\mathrm{Discrete.mk}\,a \cong \mathrm{Discrete.mk}\,b$ in the discrete category over $\alpha$.
CategoryTheory.Discrete.id_def theorem
(X : Discrete α) : ULift.up (PLift.up (Eq.refl X.as)) = 𝟙 X
Full source 
@[simp]
theorem id_def (X : Discrete α) : ULift.up (PLift.up (Eq.refl X.as)) = 𝟙 X :=
  rfl
Identity Morphism in Discrete Category Equals Lifted Reflexivity Proof
Informal description
For any object $X$ in the discrete category $\mathrm{Discrete}\,\alpha$, the identity morphism $\mathrm{id}_X$ is equal to the lifted proof of reflexivity of $X$'s underlying element, i.e., $\mathrm{ULift.up}\,(\mathrm{PLift.up}\,(\mathrm{Eq.refl}\,X.\mathrm{as})) = \mathrm{id}_X$.
CategoryTheory.Discrete.functor definition
{I : Type u₁} (F : I → C) : Discrete I ⥤ C
Full source 
/-- Any function `I → C` gives a functor `Discrete I ⥤ C`. -/
def functor {I : Type u₁} (F : I → C) : DiscreteDiscrete I ⥤ C where
  obj := F ∘ Discrete.as
  map {X Y} f := by
    dsimp
    rcases f with ⟨⟨h⟩⟩
    exact eqToHom (congrArg _ h)
Functor from discrete category induced by a function
Informal description
Given a function $F \colon I \to C$ from a type $I$ to the objects of a category $C$, the functor $\mathrm{Discrete.functor}\,F \colon \mathrm{Discrete}\,I \to C$ maps each object $i$ in the discrete category over $I$ to $F(i)$, and each morphism (which is necessarily an identity) to the corresponding identity morphism in $C$.
CategoryTheory.Discrete.functor_obj theorem
{I : Type u₁} (F : I → C) (i : I) : (Discrete.functor F).obj (Discrete.mk i) = F i
Full source 
@[simp]
theorem functor_obj {I : Type u₁} (F : I → C) (i : I) :
    (Discrete.functor F).obj (Discrete.mk i) = F i :=
  rfl
Functor Object Mapping in Discrete Category: $\mathrm{Discrete.functor}\,F\,(\mathrm{Discrete.mk}\,i) = F(i)$
Informal description
For any function $F \colon I \to C$ from a type $I$ to the objects of a category $C$, the functor $\mathrm{Discrete.functor}\,F$ maps the object $\mathrm{Discrete.mk}\,i$ (for any $i \in I$) to $F(i)$.
CategoryTheory.Discrete.functor_map theorem
{I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) : (Discrete.functor F).map f = 𝟙 (F i.as)
Full source 
theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) :
    (Discrete.functor F).map f = 𝟙 (F i.as) := by aesop_cat
Functor from Discrete Category Maps Identity to Identity
Informal description
For any function $F \colon I \to C$ from a type $I$ to the objects of a category $C$, and any morphism $f \colon i \to i$ in the discrete category $\mathrm{Discrete}\,I$ (which must be the identity morphism), the functor $\mathrm{Discrete.functor}\,F$ maps $f$ to the identity morphism $\mathrm{id}_{F(i)}$ in $C$, where $i$ is the underlying element of the object $i$ in $\mathrm{Discrete}\,I$.
CategoryTheory.Discrete.functor_obj_eq_as theorem
{I : Type u₁} (F : I → C) (X : Discrete I) : (Discrete.functor F).obj X = F X.as
Full source 
@[simp]
theorem functor_obj_eq_as {I : Type u₁} (F : I → C) (X : Discrete I) :
    (Discrete.functor F).obj X = F X.as :=
  rfl
Functor Object Equality in Discrete Category
Informal description
For any type $I$ and function $F \colon I \to C$ to the objects of a category $C$, the functor $\mathrm{Discrete.functor}\,F$ maps an object $X$ in the discrete category $\mathrm{Discrete}\,I$ to $F(X.\mathrm{as})$, where $X.\mathrm{as}$ is the underlying element of $I$ associated with $X$.
CategoryTheory.Discrete.functorComp definition
{I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) : Discrete.functor (f ∘ g) ≅ Discrete.functor (Discrete.mk ∘ g) ⋙ Discrete.functor f
Full source 
/-- The discrete functor induced by a composition of maps can be written as a
composition of two discrete functors.
-/
@[simps!]
def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
    Discrete.functorDiscrete.functor (f ∘ g) ≅ Discrete.functor (Discrete.mk ∘ g) ⋙ Discrete.functor f :=
  NatIso.ofComponents fun _ => Iso.refl _
Natural isomorphism between composition of discrete functors and functor of composition
Informal description
Given a function \( f \colon J \to C \) and a function \( g \colon I \to J \), the functor induced by the composition \( f \circ g \) is naturally isomorphic to the composition of the functor induced by \( g \) followed by the functor induced by \( f \).
CategoryTheory.Discrete.natTrans definition
{I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) : F ⟶ G
Full source 
/-- For functors out of a discrete category,
a natural transformation is just a collection of maps,
as the naturality squares are trivial.
-/
@[simps]
def natTrans {I : Type u₁} {F G : DiscreteDiscrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) :
    F ⟶ G where
  app := f
  naturality := fun {X Y} ⟨⟨g⟩⟩ => by
    discrete_cases
    rcases g
    change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
    simp
Natural transformation between functors out of a discrete category
Informal description
Given a type $I$ and two functors $F, G \colon \mathrm{Discrete}\,I \to C$ from the discrete category over $I$ to a category $C$, a natural transformation $\eta \colon F \Rightarrow G$ is defined by specifying a morphism $\eta_i \colon F(i) \to G(i)$ for each object $i$ in $\mathrm{Discrete}\,I$. The naturality condition is automatically satisfied since the only morphisms in $\mathrm{Discrete}\,I$ are identities.
CategoryTheory.Discrete.natIso definition
{I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) : F ≅ G
Full source 
/-- For functors out of a discrete category,
a natural isomorphism is just a collection of isomorphisms,
as the naturality squares are trivial.
-/
@[simps!]
def natIso {I : Type u₁} {F G : DiscreteDiscrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) :
    F ≅ G :=
  NatIso.ofComponents f fun ⟨⟨g⟩⟩ => by
    discrete_cases
    rcases g
    change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
    simp
Natural isomorphism from objectwise isomorphisms in a discrete category
Informal description
Given a family of isomorphisms $f_i : F(i) \to G(i)$ for each object $i$ in the discrete category over $I$, the function constructs a natural isomorphism between the functors $F$ and $G$ from $\mathrm{Discrete}\,I$ to $\mathcal{C}$. The naturality condition is trivially satisfied since the only morphisms in the discrete category are identities.
CategoryTheory.Discrete.instIsIsoFunctorNatTrans instance
{I : Type*} {F G : Discrete I ⥤ C} (f : ∀ i, F.obj i ⟶ G.obj i) [∀ i, IsIso (f i)] : IsIso (Discrete.natTrans f)
Full source 
instance {I : Type*} {F G : DiscreteDiscrete I ⥤ C} (f : ∀ i, F.obj i ⟶ G.obj i) [∀ i, IsIso (f i)] :
    IsIso (Discrete.natTrans f) := by
  change IsIso (Discrete.natIso (fun i => asIso (f i))).hom
  infer_instance
Natural Isomorphism from Objectwise Isomorphisms in a Discrete Category
Informal description
Given a type $I$, two functors $F, G \colon \mathrm{Discrete}\,I \to \mathcal{C}$ from the discrete category over $I$ to a category $\mathcal{C}$, and a family of morphisms $f_i \colon F(i) \to G(i)$ for each object $i$ in $\mathrm{Discrete}\,I$, if each $f_i$ is an isomorphism, then the natural transformation $\mathrm{Discrete.natTrans}\,f \colon F \Rightarrow G$ is also a natural isomorphism.
CategoryTheory.Discrete.natIso_app theorem
{I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) (i : Discrete I) : (Discrete.natIso f).app i = f i
Full source 
@[simp]
theorem natIso_app {I : Type u₁} {F G : DiscreteDiscrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i)
    (i : Discrete I) : (Discrete.natIso f).app i = f i := by aesop_cat
Component of Natural Isomorphism in Discrete Category Equals Given Isomorphism
Informal description
For any family of isomorphisms $f_i : F(i) \to G(i)$ between objects in a category $\mathcal{C}$, indexed by objects $i$ in the discrete category over $I$, the component of the natural isomorphism $\mathrm{Discrete.natIso}\,f$ at $i$ is equal to $f_i$. That is, $(\mathrm{Discrete.natIso}\,f).app\,i = f_i$.
CategoryTheory.Discrete.natIsoFunctor definition
{I : Type u₁} {F : Discrete I ⥤ C} : F ≅ Discrete.functor (F.obj ∘ Discrete.mk)
Full source 
/-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to
  `Discrete.functor (F.obj)`. -/
@[simps!]
def natIsoFunctor {I : Type u₁} {F : DiscreteDiscrete I ⥤ C} : F ≅ Discrete.functor (F.obj ∘ Discrete.mk) :=
  natIso fun _ => Iso.refl _
Natural isomorphism between a functor and its induced functor on discrete category
Informal description
For any functor $F$ from the discrete category over a type $I$ to a category $\mathcal{C}$, there is a natural isomorphism between $F$ and the functor $\mathrm{Discrete.functor}\,(F \circ \mathrm{Discrete.mk})$, where $\mathrm{Discrete.mk}$ is the constructor for objects in the discrete category. This isomorphism is given by the identity isomorphism at each object.
CategoryTheory.Discrete.compNatIsoDiscrete definition
{I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : I → C) (G : C ⥤ D) : Discrete.functor F ⋙ G ≅ Discrete.functor (G.obj ∘ F)
Full source 
/-- Composing `Discrete.functor F` with another functor `G` amounts to composing `F` with `G.obj` -/
@[simps!]
def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : I → C) (G : C ⥤ D) :
    Discrete.functorDiscrete.functor F ⋙ GDiscrete.functor F ⋙ G ≅ Discrete.functor (G.obj ∘ F) :=
  natIso fun _ => Iso.refl _
Natural isomorphism between composition of functors and functor of composition in discrete categories
Informal description
Given a function $F \colon I \to C$ from a type $I$ to the objects of a category $C$, and a functor $G \colon C \to D$ between categories $C$ and $D$, the composition of the functor $\mathrm{Discrete.functor}\,F$ with $G$ is naturally isomorphic to the functor $\mathrm{Discrete.functor}\,(G \circ F)$.
CategoryTheory.Discrete.equivalence definition
{I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J
Full source 
/-- We can promote a type-level `Equiv` to
an equivalence between the corresponding `discrete` categories.
-/
@[simps]
def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : DiscreteDiscrete I ≌ Discrete J where
  functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
  inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
  unitIso :=
    Discrete.natIso fun i => eqToIso (by simp)
  counitIso :=
    Discrete.natIso fun j => eqToIso (by simp)
Equivalence of discrete categories induced by a type equivalence
Informal description
Given a type equivalence $e : I \simeq J$, the function constructs an equivalence of categories between the discrete categories $\mathrm{Discrete}\,I$ and $\mathrm{Discrete}\,J$. Specifically: - The forward functor maps each object $i$ in $\mathrm{Discrete}\,I$ to $e(i)$ in $\mathrm{Discrete}\,J$. - The inverse functor maps each object $j$ in $\mathrm{Discrete}\,J$ to $e^{-1}(j)$ in $\mathrm{Discrete}\,I$. - The unit isomorphism is the identity isomorphism, since applying both functors in sequence returns the original object. - The counit isomorphism is the identity isomorphism, since applying both functors in sequence returns the original object.
CategoryTheory.Discrete.equivOfEquivalence definition
{α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β
Full source 
/-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/
@[simps]
def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : DiscreteDiscrete α ≌ Discrete β) : α ≃ β where
  toFun := Discrete.asDiscrete.as ∘ h.functor.obj ∘ Discrete.mk
  invFun := Discrete.asDiscrete.as ∘ h.inverse.obj ∘ Discrete.mk
  left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
  right_inv a := by simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1
Type equivalence from discrete category equivalence
Informal description
Given an equivalence of discrete categories $h \colon \mathrm{Discrete}\,\alpha \simeq \mathrm{Discrete}\,\beta$, the function constructs a type-level equivalence (bijection) between $\alpha$ and $\beta$. Specifically: - The forward map sends $a \in \alpha$ to the underlying element of the object obtained by applying the functor part of $h$ to the discrete object $\mathrm{mk}\,a$. - The inverse map sends $b \in \beta$ to the underlying element of the object obtained by applying the inverse functor part of $h$ to the discrete object $\mathrm{mk}\,b$. - The left inverse property is satisfied due to the naturality of the unit isomorphism of $h$. - The right inverse property is satisfied due to the naturality of the counit isomorphism of $h$.
CategoryTheory.Discrete.opposite definition
(α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α
Full source 
/-- A discrete category is equivalent to its opposite category. -/
@[simps! functor_obj_as inverse_obj]
protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ(Discrete α)ᵒᵖ ≌ Discrete α :=
  let F : DiscreteDiscrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x)
  { functor := F.leftOp
    inverse := F
    unitIso := NatIso.ofComponents fun ⟨_⟩ => Iso.refl _
    counitIso := Discrete.natIso fun ⟨_⟩ => Iso.refl _ }
Equivalence between a discrete category and its opposite
Informal description
For any type $\alpha$, the opposite category of the discrete category over $\alpha$ is equivalent to the discrete category over $\alpha$ itself. This equivalence is constructed using: - A functor $F$ that maps each object $x$ in $\mathrm{Discrete}\,\alpha$ to its opposite $\mathrm{op}\,x$ in $(\mathrm{Discrete}\,\alpha)^{\mathrm{op}}$ - An inverse functor that maps objects back from the opposite category - Natural isomorphisms given by identity morphisms at each object
CategoryTheory.Discrete.functor_map_id theorem
(F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F.map f = 𝟙 (F.obj j)
Full source 
@[simp]
theorem functor_map_id (F : DiscreteDiscrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) :
    F.map f = 𝟙 (F.obj j) := by
  have h : f = 𝟙 j := by aesop_cat
  rw [h]
  simp
Functor from Discrete Category Maps Endomorphisms to Identities
Informal description
For any functor $F$ from the discrete category $\mathrm{Discrete}\,J$ to a category $C$, and any endomorphism $f$ on an object $j$ in $\mathrm{Discrete}\,J$, the image of $f$ under $F$ is equal to the identity morphism on $F(j)$ in $C$.
CategoryTheory.piEquivalenceFunctorDiscrete definition
(J : Type u₂) (C : Type u₁) [Category.{v₁} C] : (J → C) ≌ (Discrete J ⥤ C)
Full source 
/-- The equivalence of categories `(J → C) ≌ (Discrete J ⥤ C)`. -/
@[simps]
def piEquivalenceFunctorDiscrete (J : Type u₂) (C : Type u₁) [Category.{v₁} C] :
    (J → C) ≌ (Discrete J ⥤ C) where
  functor :=
    { obj := fun F => Discrete.functor F
      map := fun f => Discrete.natTrans (fun j => f j.as) }
  inverse :=
    { obj := fun F j => F.obj ⟨j⟩
      map := fun f j => f.app ⟨j⟩ }
  unitIso := Iso.refl _
  counitIso := NatIso.ofComponents (fun F => (NatIso.ofComponents (fun _ => Iso.refl _)
    (by
      rintro ⟨x⟩ ⟨y⟩ f
      obtain rfl : x = y := Discrete.eq_of_hom f
      obtain rfl : f = 𝟙 _ := rfl
      simp))) (by aesop_cat)
Equivalence between $J$-indexed families and functors from discrete $J$
Informal description
The equivalence of categories between the category of $J$-indexed families of objects in a category $C$ and the category of functors from the discrete category over $J$ to $C$. Specifically, this equivalence consists of: - A functor that takes a family $F \colon J \to C$ to the functor $\mathrm{Discrete.functor}\,F \colon \mathrm{Discrete}\,J \to C$. - An inverse functor that takes a functor $G \colon \mathrm{Discrete}\,J \to C$ to the family $G \circ \langle \cdot \rangle \colon J \to C$. - Natural isomorphisms witnessing the equivalence, where the unit is the identity and the counit is constructed from identity isomorphisms.
CategoryTheory.IsDiscrete structure
(C : Type*) [Category C]
Full source 
/-- A category is discrete when there is at most one morphism between two objects,
in which case they are equal. -/
class IsDiscrete (C : Type*) [Category C] : Prop where
  subsingleton (X Y : C) : Subsingleton (X ⟶ Y) := by infer_instance
  eq_of_hom {X Y : C} (f : X ⟶ Y) : X = Y
Discrete category
Informal description
A category \( C \) is called *discrete* if for any two objects \( X \) and \( Y \) in \( C \), there is at most one morphism from \( X \) to \( Y \), and such a morphism exists only when \( X = Y \). In other words, the only morphisms in a discrete category are the identity morphisms.
CategoryTheory.obj_ext_of_isDiscrete theorem
{C : Type*} [Category C] [IsDiscrete C] {X Y : C} (f : X ⟶ Y) : X = Y
Full source 
lemma obj_ext_of_isDiscrete {C : Type*} [Category C] [IsDiscrete C]
    {X Y : C} (f : X ⟶ Y) : X = Y := IsDiscrete.eq_of_hom f
Objects in a Discrete Category are Equal if a Morphism Exists
Informal description
In a discrete category \( C \), for any objects \( X \) and \( Y \) and any morphism \( f : X \to Y \), the objects \( X \) and \( Y \) are equal, i.e., \( X = Y \).