Mathlib.CategoryTheory.Equivalence

CategoryTheory.Equivalence structure

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

Full source

/-- We define an equivalence as a (half)-adjoint equivalence, a pair of functors with
  a unit and counit which are natural isomorphisms and the triangle law `Fη ≫ εF = 1`, or in other
  words the composite `F ⟶ FGF ⟶ F` is the identity.

  In `unit_inverse_comp`, we show that this is actually an adjoint equivalence, i.e., that the
  composite `G ⟶ GFG ⟶ G` is also the identity.

  The triangle equation is written as a family of equalities between morphisms, it is more
  complicated if we write it as an equality of natural transformations, because then we would have
  to insert natural transformations like `F ⟶ F1`. -/
@[ext, stacks 001J]
structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D] where mk' ::
  /-- A functor in one direction -/
  functor : C ⥤ D
  /-- A functor in the other direction -/
  inverse : D ⥤ C
  /-- The composition `functor ⋙ inverse` is isomorphic to the identity -/
  unitIso : 𝟭𝟭 C ≅ functor ⋙ inverse
  /-- The composition `inverse ⋙ functor` is also isomorphic to the identity -/
  counitIso : inverse ⋙ functorinverse ⋙ functor ≅ 𝟭 D
  /-- The natural isomorphisms compose to the identity. -/
  functor_unitIso_comp :
    ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) =
      𝟙 (functor.obj X) := by aesop_cat

Equivalence of Categories (Half-Adjoint)

Informal description

An equivalence of categories $C$ and $D$ is a tuple $(F, G, \eta, \epsilon)$ where: - $F \colon C \to D$ and $G \colon D \to C$ are functors, - $\eta \colon \text{id}_C \cong F \circ G$ and $\epsilon \colon G \circ F \cong \text{id}_D$ are natural isomorphisms, - The triangle identity $F \eta \cdot \epsilon F = \text{id}_F$ holds (meaning the composite $F \to FGF \to F$ is the identity). This structure is called a "half-adjoint equivalence" and automatically implies that the tuple forms an adjoint equivalence (i.e., the composite $G \to GFG \to G$ is also the identity).

CategoryTheory.term_≌_ definition

: Lean.TrailingParserDescr✝

Full source

/-- We infix the usual notation for an equivalence -/
infixr:10 " ≌ " => Equivalence

Equivalence of categories notation (`≌`)

Informal description

The notation `C ≌ D` denotes an equivalence of categories between categories `C` and `D`. An equivalence consists of a pair of functors `F : C → D` and `G : D → C`, along with natural isomorphisms `η : 𝟭_C ≅ F ∘ G` and `ε : G ∘ F ≅ 𝟭_D`, satisfying certain coherence conditions that make it a "half-adjoint equivalence".

CategoryTheory.Equivalence.unit abbrev

(e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse

Full source

/-- The unit of an equivalence of categories. -/
abbrev unit (e : C ≌ D) : 𝟭𝟭 C ⟶ e.functor ⋙ e.inverse :=
  e.unitIso.hom

Unit Natural Transformation of Category Equivalence

Informal description

For an equivalence of categories $e \colon C \simeq D$, the unit $\eta$ is a natural transformation from the identity functor $\text{id}_C$ to the composition of the functor $e.\text{functor} \colon C \to D$ and its inverse $e.\text{inverse} \colon D \to C$.

CategoryTheory.Equivalence.counit abbrev

(e : C ≌ D) : e.inverse ⋙ e.functor ⟶ 𝟭 D

Full source

/-- The counit of an equivalence of categories. -/
abbrev counit (e : C ≌ D) : e.inverse ⋙ e.functore.inverse ⋙ e.functor ⟶ 𝟭 D :=
  e.counitIso.hom

Counit Natural Transformation of Category Equivalence

Informal description

For an equivalence of categories $e \colon C \simeq D$, the counit $\epsilon$ is a natural transformation from the composition of the inverse functor $e.\text{inverse} \colon D \to C$ and the functor $e.\text{functor} \colon C \to D$ to the identity functor $\text{id}_D$.

CategoryTheory.Equivalence.unitInv abbrev

(e : C ≌ D) : e.functor ⋙ e.inverse ⟶ 𝟭 C

Full source

/-- The inverse of the unit of an equivalence of categories. -/
abbrev unitInv (e : C ≌ D) : e.functor ⋙ e.inversee.functor ⋙ e.inverse ⟶ 𝟭 C :=
  e.unitIso.inv

Inverse Unit Natural Transformation of Category Equivalence

Informal description

For an equivalence of categories $e \colon C \simeq D$, the inverse unit $\eta^{-1}$ is a natural transformation from the composition of the functor $e.\text{functor} \colon C \to D$ and its inverse $e.\text{inverse} \colon D \to C$ to the identity functor $\text{id}_C$.

CategoryTheory.Equivalence.counitInv abbrev

(e : C ≌ D) : 𝟭 D ⟶ e.inverse ⋙ e.functor

Full source

/-- The inverse of the counit of an equivalence of categories. -/
abbrev counitInv (e : C ≌ D) : 𝟭𝟭 D ⟶ e.inverse ⋙ e.functor :=
  e.counitIso.inv

Inverse Counit Natural Transformation of Category Equivalence

Informal description

For an equivalence of categories $e \colon C \simeq D$, the inverse counit $\epsilon^{-1}$ is a natural transformation from the identity functor $\text{id}_D$ to the composition of the inverse functor $e.\text{inverse} \colon D \to C$ and the functor $e.\text{functor} \colon C \to D$.

CategoryTheory.Equivalence.Equivalence_mk'_unit theorem

 (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom

Full source

@[simp]
theorem Equivalence_mk'_unit (functor inverse unit_iso counit_iso f) :
    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom :=
  rfl

Unit Natural Transformation in Constructed Equivalence

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to C$, natural isomorphisms $\eta \colon \text{id}_C \cong F \circ G$ and $\epsilon \colon G \circ F \cong \text{id}_D$, and a proof $f$ that the composition $F \to FGF \to F$ is the identity, the unit natural transformation of the constructed equivalence $\langle F, G, \eta, \epsilon, f \rangle \colon C \simeq D$ is equal to the homomorphism component of $\eta$.

CategoryTheory.Equivalence.Equivalence_mk'_counit theorem

 (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom

Full source

@[simp]
theorem Equivalence_mk'_counit (functor inverse unit_iso counit_iso f) :
    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom :=
  rfl

Equivalence Construction Preserves Counit Natural Transformation

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to C$, natural isomorphisms $\eta \colon \text{id}_C \cong F \circ G$ and $\epsilon \colon G \circ F \cong \text{id}_D$, and a proof $f$ that the composition $F \to FGF \to F$ is the identity, the counit natural transformation of the constructed equivalence $\langle F, G, \eta, \epsilon, f \rangle \colon C \simeq D$ is equal to the homomorphism component of $\epsilon$.

CategoryTheory.Equivalence.Equivalence_mk'_unitInv theorem

 (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unitInv = unit_iso.inv

Full source

@[simp]
theorem Equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) :
    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unitInv = unit_iso.inv :=
  rfl

Equivalence Construction Preserves Inverse Unit

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to C$, natural isomorphisms $\eta \colon \text{id}_C \cong F \circ G$ and $\epsilon \colon G \circ F \cong \text{id}_D$, and a proof $f$ that the composition $F \to FGF \to F$ is the identity, the inverse unit of the constructed equivalence $\langle F, G, \eta, \epsilon, f \rangle \colon C \simeq D$ is equal to the inverse of the unit isomorphism $\eta^{-1}$.

CategoryTheory.Equivalence.Equivalence_mk'_counitInv theorem

 (functor inverse unit_iso counit_iso f) :
  (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counitInv = counit_iso.inv

Full source

@[simp]
theorem Equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) :
    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counitInv = counit_iso.inv :=
  rfl

Equivalence Construction Preserves Inverse Counit

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to C$, natural isomorphisms $\eta \colon \text{id}_C \cong F \circ G$ and $\epsilon \colon G \circ F \cong \text{id}_D$, and a proof $f$ that the composition $F \to FGF \to F$ is the identity, the inverse counit of the constructed equivalence $\langle F, G, \eta, \epsilon, f \rangle \colon C \simeq D$ is equal to the inverse of the counit isomorphism $\epsilon^{-1}$.

CategoryTheory.Equivalence.counit_naturality theorem

(e : C ≌ D) {X Y : D} (f : X ⟶ Y) : e.functor.map (e.inverse.map f) ≫ e.counit.app Y = e.counit.app X ≫ f

Full source

@[reassoc]
theorem counit_naturality (e : C ≌ D) {X Y : D} (f : X ⟶ Y) :
    e.functor.map (e.inverse.map f) ≫ e.counit.app Y = e.counit.app X ≫ f :=
  e.counit.naturality f

Naturality of Counit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any morphism $f \colon X \to Y$ in $D$, the following diagram commutes: \[ F(G(f)) \circ \epsilon_Y = \epsilon_X \circ f \] where: - $F = e.\text{functor} \colon C \to D$ is the forward functor, - $G = e.\text{inverse} \colon D \to C$ is the inverse functor, - $\epsilon \colon G \circ F \to \text{id}_D$ is the counit natural transformation.

CategoryTheory.Equivalence.unit_naturality theorem

(e : C ≌ D) {X Y : C} (f : X ⟶ Y) : e.unit.app X ≫ e.inverse.map (e.functor.map f) = f ≫ e.unit.app Y

Full source

@[reassoc]
theorem unit_naturality (e : C ≌ D) {X Y : C} (f : X ⟶ Y) :
    e.unit.app X ≫ e.inverse.map (e.functor.map f) = f ≫ e.unit.app Y :=
  (e.unit.naturality f).symm

Naturality of Unit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any morphism $f \colon X \to Y$ in $C$, the following diagram commutes: \[ \eta_X \circ G(F(f)) = f \circ \eta_Y \] where: - $F = e.\text{functor} \colon C \to D$ and $G = e.\text{inverse} \colon D \to C$ are the functors forming the equivalence, - $\eta \colon \text{id}_C \to G \circ F$ is the unit natural transformation.

CategoryTheory.Equivalence.counitInv_naturality theorem

(e : C ≌ D) {X Y : D} (f : X ⟶ Y) : e.counitInv.app X ≫ e.functor.map (e.inverse.map f) = f ≫ e.counitInv.app Y

Full source

@[reassoc]
theorem counitInv_naturality (e : C ≌ D) {X Y : D} (f : X ⟶ Y) :
    e.counitInv.app X ≫ e.functor.map (e.inverse.map f) = f ≫ e.counitInv.app Y :=
  (e.counitInv.naturality f).symm

Naturality of Inverse Counit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any morphism $f \colon X \to Y$ in $D$, the following diagram commutes: \[ \epsilon^{-1}_X \circ F(G(f)) = f \circ \epsilon^{-1}_Y \] where: - $F = e.\text{functor} \colon C \to D$ and $G = e.\text{inverse} \colon D \to C$ are the functors forming the equivalence, - $\epsilon^{-1} \colon \text{id}_D \to F \circ G$ is the inverse counit natural transformation.

CategoryTheory.Equivalence.unitInv_naturality theorem

(e : C ≌ D) {X Y : C} (f : X ⟶ Y) : e.inverse.map (e.functor.map f) ≫ e.unitInv.app Y = e.unitInv.app X ≫ f

Full source

@[reassoc]
theorem unitInv_naturality (e : C ≌ D) {X Y : C} (f : X ⟶ Y) :
    e.inverse.map (e.functor.map f) ≫ e.unitInv.app Y = e.unitInv.app X ≫ f :=
  e.unitInv.naturality f

Naturality of Inverse Unit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any morphism $f \colon X \to Y$ in $C$, the following diagram commutes: \[ G(F(f)) \circ \eta^{-1}_Y = \eta^{-1}_X \circ f \] where: - $F = e.\text{functor} \colon C \to D$ and $G = e.\text{inverse} \colon D \to C$ are the functors forming the equivalence, - $\eta^{-1} \colon G \circ F \to \text{id}_C$ is the inverse unit natural transformation.

CategoryTheory.Equivalence.functor_unit_comp theorem

(e : C ≌ D) (X : C) : e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X)

Full source

@[reassoc (attr := simp)]
theorem functor_unit_comp (e : C ≌ D) (X : C) :
    e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
  e.functor_unitIso_comp X

Triangle Identity for Functor and Unit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $X$ in $C$, the composition of the functor $F = e.\text{functor}$ applied to the unit morphism $\eta_X \colon X \to GF(X)$ with the counit morphism $\epsilon_{F(X)} \colon FG(F(X)) \to F(X)$ equals the identity morphism on $F(X)$. In symbols: \[ F(\eta_X) \circ \epsilon_{F(X)} = \text{id}_{F(X)} \]

CategoryTheory.Equivalence.counitInv_functor_comp theorem

(e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X)

Full source

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := by
  simpa using Iso.inv_eq_inv
    (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _)

Triangle Identity for Inverse Counit and Functor in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $X$ in $C$, the composition of the inverse counit $\epsilon^{-1}_{F(X)}$ with the functor $F$ applied to the inverse unit $\eta^{-1}_X$ equals the identity morphism on $F(X)$. In symbols: \[ \epsilon^{-1}_{F(X)} \circ F(\eta^{-1}_X) = \text{id}_{F(X)} \] where: - $F = e.\text{functor} \colon C \to D$ is the forward functor, - $\eta^{-1} \colon G \circ F \to \text{id}_C$ is the inverse unit natural transformation, - $\epsilon^{-1} \colon \text{id}_D \to F \circ G$ is the inverse counit natural transformation.

CategoryTheory.Equivalence.counitInv_app_functor theorem

(e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)

Full source

theorem counitInv_app_functor (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X) := by
  symm
  simp only [id_obj, comp_obj, counitInv]
  rw [← Iso.app_inv, ← Iso.comp_hom_eq_id (e.counitIso.app _), Iso.app_hom, functor_unit_comp]
  rfl

Inverse Counit Equals Functor Applied to Unit

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $X$ in $C$, the inverse counit morphism $\epsilon^{-1}_{F(X)}$ at $F(X)$ (where $F = e.\text{functor}$) equals the image under $F$ of the unit morphism $\eta_X \colon X \to GF(X)$. In symbols: \[ \epsilon^{-1}_{F(X)} = F(\eta_X) \]

CategoryTheory.Equivalence.counit_app_functor theorem

(e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

Full source

theorem counit_app_functor (e : C ≌ D) (X : C) :
    e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) := by
  simpa using Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)) (f := e.counit.app _)

Counit Equals Functor Applied to Inverse Unit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $X$ in $C$, the counit morphism $\epsilon_{F(X)}$ at $F(X)$ (where $F = e.\text{functor}$) equals the image under $F$ of the inverse unit morphism $\eta^{-1}_X \colon GF(X) \to X$. In symbols: \[ \epsilon_{F(X)} = F(\eta^{-1}_X) \]

CategoryTheory.Equivalence.unit_inverse_comp theorem

(e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)

Full source

/-- The other triangle equality. The proof follows the following proof in Globular:
  http://globular.science/1905.001 -/
@[reassoc (attr := simp)]
theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
    e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) := by
  rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]
  dsimp
  rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), Iso.app_hom,
    Iso.app_inv]
  slice_lhs 2 3 => rw [← e.unit_naturality]
  slice_lhs 1 2 => rw [← e.unit_naturality]
  slice_lhs 4 4 =>
    rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
  slice_lhs 3 4 =>
    dsimp only [Functor.mapIso_hom, Iso.app_hom]
    rw [← map_comp e.inverse, e.counit_naturality, e.counitIso.hom_inv_id_app]
    dsimp only [Functor.comp_obj]
    rw [map_id]
  dsimp only [comp_obj, id_obj]
  rw [id_comp]
  slice_lhs 2 3 =>
    dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]
  slice_lhs 3 4 => rw [e.unitInv_naturality]
  slice_lhs 4 5 =>
    rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
    dsimp only [Functor.id_obj]
    rw [map_id, map_id]
  dsimp only [comp_obj, id_obj]
  rw [id_comp]
  slice_lhs 3 4 => rw [← e.unitInv_naturality]
  slice_lhs 2 3 =>
    rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]
  dsimp only [Functor.comp_obj]
  simp

Triangle Identity for Unit and Counit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $Y$ in $D$, the composition of the unit morphism $\eta_{G(Y)}$ at $G(Y)$ with the inverse functor $G$ applied to the counit morphism $\epsilon_Y$ equals the identity morphism on $G(Y)$. In symbols: \[ \eta_{G(Y)} \circ G(\epsilon_Y) = \text{id}_{G(Y)} \] where: - $G = e.\text{inverse} \colon D \to C$ is the inverse functor, - $\eta \colon \text{id}_C \to G \circ F$ is the unit natural transformation, - $\epsilon \colon F \circ G \to \text{id}_D$ is the counit natural transformation.

CategoryTheory.Equivalence.inverse_counitInv_comp theorem

(e : C ≌ D) (Y : D) : e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)

Full source

@[reassoc (attr := simp)]
theorem inverse_counitInv_comp (e : C ≌ D) (Y : D) :
    e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) := by
  simpa using Iso.inv_eq_inv
    (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)) (Iso.refl _)

Triangle Identity for Inverse Counit and Inverse Unit in Category Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $Y$ in $D$, the composition of the inverse functor $G = e.\text{inverse}$ applied to the inverse counit morphism $\epsilon^{-1}_Y$ with the inverse unit morphism $\eta^{-1}_{G(Y)}$ equals the identity morphism on $G(Y)$. In symbols: \[ G(\epsilon^{-1}_Y) \circ \eta^{-1}_{G(Y)} = \text{id}_{G(Y)} \]

CategoryTheory.Equivalence.unit_app_inverse theorem

(e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

Full source

theorem unit_app_inverse (e : C ≌ D) (Y : D) :
    e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by
  simpa using Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)) (f := e.unit.app _)

Unit at Inverse Object Equals Inverse of Counit

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $Y$ in $D$, the unit morphism $\eta_{G(Y)}$ at the object $G(Y)$ is equal to the inverse functor $G$ applied to the inverse counit morphism $\epsilon^{-1}_Y$. In symbols: \[ \eta_{G(Y)} = G(\epsilon^{-1}_Y) \] where: - $G = e.\text{inverse} \colon D \to C$ is the inverse functor, - $\eta \colon \text{id}_C \to G \circ F$ is the unit natural transformation, - $\epsilon^{-1} \colon \text{id}_D \to F \circ G$ is the inverse counit natural transformation.

CategoryTheory.Equivalence.unitInv_app_inverse theorem

(e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)

Full source

theorem unitInv_app_inverse (e : C ≌ D) (Y : D) :
    e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) := by
  rw [← Iso.app_inv, ← Iso.app_hom, ← mapIso_hom, Eq.comm, ← Iso.hom_eq_inv]
  simpa using unit_app_inverse e Y

Inverse Unit at Inverse Object Equals Inverse of Counit Morphism

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any object $Y$ in $D$, the inverse unit morphism $\eta^{-1}_{G(Y)}$ at the object $G(Y)$ is equal to the inverse functor $G$ applied to the counit morphism $\epsilon_Y$. In symbols: \[ \eta^{-1}_{G(Y)} = G(\epsilon_Y) \] where: - $G = e.\text{inverse} \colon D \to C$ is the inverse functor, - $\eta^{-1} \colon F \circ G \to \text{id}_C$ is the inverse unit natural transformation, - $\epsilon \colon G \circ F \to \text{id}_D$ is the counit natural transformation.

CategoryTheory.Equivalence.fun_inv_map theorem

(e : C ≌ D) (X Y : D) (f : X ⟶ Y) : e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y

Full source

@[reassoc, simp]
theorem fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
    e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y :=
  (NatIso.naturality_2 e.counitIso f).symm

Functor-Inverse Image of Morphism Under Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$, objects $X, Y \in D$, and morphism $f \colon X \to Y$, the following equality holds: $$ e(F(e^{-1}(f))) = \epsilon_X \circ f \circ \epsilon^{-1}_Y $$ where $\epsilon \colon e^{-1} \circ e \Rightarrow \text{id}_D$ is the counit isomorphism of the equivalence and $\epsilon^{-1}$ is its inverse.

CategoryTheory.Equivalence.inv_fun_map theorem

(e : C ≌ D) (X Y : C) (f : X ⟶ Y) : e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y

Full source

@[reassoc, simp]
theorem inv_fun_map (e : C ≌ D) (X Y : C) (f : X ⟶ Y) :
    e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y :=
  (NatIso.naturality_1 e.unitIso f).symm

Inverse-Functor Image of Morphism Under Equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$, objects $X, Y \in C$, and morphism $f \colon X \to Y$, the following equality holds: $$ e^{-1}(e(f)) = \eta^{-1}_X \circ f \circ \eta_Y $$ where $\eta \colon \text{id}_C \Rightarrow e^{-1} \circ e$ is the unit isomorphism of the equivalence and $\eta^{-1}$ is its inverse.

CategoryTheory.Equivalence.adjointifyη definition

: 𝟭 C ≅ F ⋙ G

Full source

/-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it
to a refined natural isomorphism `adjointifyη η : 𝟭 C ≅ F ⋙ G` which exhibits the properties
required for a half-adjoint equivalence. See `Equivalence.mk`. -/
def adjointifyη : 𝟭𝟭 C ≅ F ⋙ G := by
  calc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ Gcalc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ Gcalc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
    _ ≅ F ⋙ G ⋙ F ⋙ Gcalc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
    _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G)
    _ ≅ (F ⋙ G) ⋙ F ⋙ Gcalc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
    _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G)
    _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
    _ ≅ 𝟭 C ⋙ F ⋙ Gcalc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
    _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G)
    _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
    _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G)
    _ ≅ F ⋙ G := leftUnitor (F ⋙ G)

Refinement of unit isomorphism for half-adjoint equivalence

Informal description

Given natural isomorphisms $\eta: \mathbf{1}_C \cong F \circ G$ and $\varepsilon: G \circ F \cong \mathbf{1}_D$ that form part of an equivalence between categories $C$ and $D$, the function `adjointifyη` refines $\eta$ to a new natural isomorphism $\mathbf{1}_C \cong F \circ G$ that satisfies the additional properties required for a half-adjoint equivalence. This refinement ensures that the composition $F \to FGF \to F$ is the identity, which is a key property in the definition of an equivalence of categories.

CategoryTheory.Equivalence.adjointify_η_ε theorem

(X : C) : F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)

Full source

@[reassoc]
theorem adjointify_η_ε (X : C) :
    F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) := by
  dsimp [adjointifyη,Trans.trans]
  simp only [comp_id, assoc, map_comp]
  have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this
  rw [← assoc _ _ (F.map _)]
  have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this
  have := (ε.app <| F.obj X).hom_inv_id; dsimp at this; rw [this]; clear this
  rw [id_comp]; have := (F.mapIso <| η.app X).hom_inv_id; dsimp at this; rw [this]

Identity Condition for Refined Unit and Counit in Equivalence of Categories

Informal description

For any object $X$ in category $C$, the composition of the morphism $F(\eta_X)$ (where $\eta$ is the refined unit isomorphism obtained from `adjointifyη`) with the counit morphism $\varepsilon_{F(X)}$ is equal to the identity morphism on $F(X)$. That is, $F(\eta_X) \circ \varepsilon_{F(X)} = \mathrm{id}_{F(X)}$.

CategoryTheory.Equivalence.mk definition

(F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : C ≌ D

Full source

/-- Every equivalence of categories consisting of functors `F` and `G` such that `F ⋙ G` and
    `G ⋙ F` are naturally isomorphic to identity functors can be transformed into a half-adjoint
    equivalence without changing `F` or `G`. -/
protected def mk (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭𝟭 C ≅ F ⋙ G) (ε : G ⋙ FG ⋙ F ≅ 𝟭 D) : C ≌ D :=
  ⟨F, G, adjointifyη η ε, ε, adjointify_η_ε η ε⟩

Construction of Equivalence of Categories from Functors and Natural Isomorphisms

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to C$, along with natural isomorphisms $\eta \colon \text{id}_C \cong F \circ G$ and $\varepsilon \colon G \circ F \cong \text{id}_D$, the function `Equivalence.mk` constructs an equivalence of categories $C \simeq D$ by refining $\eta$ to satisfy the half-adjoint condition, ensuring that the composition $F \to FGF \to F$ is the identity.

CategoryTheory.Equivalence.refl definition

: C ≌ C

Full source

/-- Equivalence of categories is reflexive. -/
@[refl, simps]
def refl : C ≌ C :=
  ⟨𝟭 C, 𝟭 C, Iso.refl _, Iso.refl _, fun _ => Category.id_comp _⟩

Reflexive equivalence of categories

Informal description

The reflexive equivalence of a category $C$ is given by the identity functor $\text{id}_C$ on both sides, with both the unit $\eta$ and counit $\epsilon$ being the identity natural isomorphisms. This satisfies the half-adjoint condition trivially since all compositions reduce to identity morphisms.

CategoryTheory.Equivalence.instInhabited instance

: Inhabited (C ≌ C)

Full source

instance : Inhabited (C ≌ C) :=
  ⟨refl⟩

Existence of Trivial Equivalence for Any Category

Informal description

For any category $C$, there exists a trivial equivalence of categories $C \simeq C$ given by the identity functor.

CategoryTheory.Equivalence.symm definition

(e : C ≌ D) : D ≌ C

Full source

/-- Equivalence of categories is symmetric. -/
@[symm, simps]
def symm (e : C ≌ D) : D ≌ C :=
  ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counitInv_comp⟩

Symmetric equivalence of categories

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the symmetric equivalence $D \simeq C$ is defined by: - The functor $G = e.\text{inverse} \colon D \to C$ - The inverse functor $F = e.\text{functor} \colon C \to D$ - The unit isomorphism $\epsilon^{-1} \colon \text{id}_D \cong G \circ F$ - The counit isomorphism $\eta^{-1} \colon F \circ G \cong \text{id}_C$ - The triangle identity $G \epsilon^{-1} \cdot \eta^{-1} G = \text{id}_G$ holds.

CategoryTheory.Equivalence.trans definition

(e : C ≌ D) (f : D ≌ E) : C ≌ E

Full source

/-- Equivalence of categories is transitive. -/
@[trans, simps]
def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E where
  functor := e.functor ⋙ f.functor
  inverse := f.inverse ⋙ e.inverse
  unitIso := e.unitIso ≪≫ isoWhiskerRight (e.functor.rightUnitor.symm ≪≫
    isoWhiskerLeft _ f.unitIso ≪≫ (Functor.associator _ _ _ ).symm) _ ≪≫ Functor.associator _ _ _
  counitIso := (Functor.associator _ _ _ ).symm ≪≫ isoWhiskerRight ((Functor.associator _ _ _ ) ≪≫
      isoWhiskerLeft _ e.counitIso ≪≫ f.inverse.rightUnitor) _ ≪≫ f.counitIso
  -- We wouldn't have needed to give this proof if we'd used `Equivalence.mk`,
  -- but we choose to avoid using that here, for the sake of good structure projection `simp`
  -- lemmas.
  functor_unitIso_comp X := by
    dsimp
    simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
      functor_unit_comp_assoc, assoc]
    slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
    simp

Composition of Equivalences of Categories

Informal description

Given equivalences of categories $e \colon C \simeq D$ and $f \colon D \simeq E$, the composition of equivalences $e \circ f \colon C \simeq E$ is defined by: - The functor $e.functor \circ f.functor \colon C \to E$ - The inverse functor $f.inverse \circ e.inverse \colon E \to C$ - The unit isomorphism $\eta \colon \text{id}_C \cong (e.functor \circ f.functor) \circ (f.inverse \circ e.inverse)$ constructed from $e.unitIso$ and $f.unitIso$ - The counit isomorphism $\epsilon \colon (f.inverse \circ e.inverse) \circ (e.functor \circ f.functor) \cong \text{id}_E$ constructed from $e.counitIso$ and $f.counitIso$ This composition satisfies the triangle identities, making it a valid equivalence of categories.

CategoryTheory.Equivalence.funInvIdAssoc definition

(e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F

Full source

/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
functor. -/
def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ Fe.functor ⋙ e.inverse ⋙ F ≅ F :=
  (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.unitIso.symm F ≪≫ F.leftUnitor

Natural isomorphism for functor composition with equivalence

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any functor $F \colon C \to E$, the composition of functors $e.functor \circ e.inverse \circ F$ is naturally isomorphic to $F$. This isomorphism is constructed using the associator, the inverse of the unit isomorphism of $e$, and the left unitor of $F$.

CategoryTheory.Equivalence.funInvIdAssoc_hom_app theorem

(e : C ≌ D) (F : C ⥤ E) (X : C) : (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X)

Full source

@[simp]
theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
    (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) := by
  dsimp [funInvIdAssoc]
  simp

Component Formula for Natural Isomorphism in Equivalence Composition

Informal description

For any equivalence of categories $e \colon C \simeq D$, any functor $F \colon C \to E$, and any object $X \in C$, the component of the natural isomorphism $(e.\text{functor} \circ e.\text{inverse} \circ F) \cong F$ at $X$ is equal to the image under $F$ of the component of the inverse unit natural transformation $e.\eta^{-1}$ at $X$. In symbols: $$(e.\text{funInvIdAssoc}\, F).\text{hom}_X = F(e.\eta^{-1}_X).$$

CategoryTheory.Equivalence.funInvIdAssoc_inv_app theorem

(e : C ≌ D) (F : C ⥤ E) (X : C) : (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X)

Full source

@[simp]
theorem funInvIdAssoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
    (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) := by
  dsimp [funInvIdAssoc]
  simp

Inverse Component Formula for Natural Isomorphism in Equivalence Composition

Informal description

For any equivalence of categories $e \colon C \simeq D$, any functor $F \colon C \to E$, and any object $X \in C$, the inverse component of the natural isomorphism $(e.\text{functor} \circ e.\text{inverse} \circ F) \cong F$ at $X$ is equal to the image under $F$ of the component of the unit natural transformation $e.\eta$ at $X$. In symbols: $$(e.\text{funInvIdAssoc}\, F)^{-1}_X = F(e.\eta_X).$$

CategoryTheory.Equivalence.invFunIdAssoc definition

(e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F ≅ F

Full source

/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
functor. -/
def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ Fe.inverse ⋙ e.functor ⋙ F ≅ F :=
  (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.counitIso F ≪≫ F.leftUnitor

Natural isomorphism for composition with equivalence inverse and functor

Informal description

For any equivalence of categories $e \colon C \simeq D$ and any functor $F \colon D \to E$, there is a natural isomorphism between the composition $(e^{-1} \circ e) \circ F$ and $F$ itself. This isomorphism is constructed by combining the associator isomorphism with the counit isomorphism of $e$ and the left unitor of $F$.

CategoryTheory.Equivalence.invFunIdAssoc_hom_app theorem

(e : C ≌ D) (F : D ⥤ E) (X : D) : (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X)

Full source

@[simp]
theorem invFunIdAssoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
    (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) := by
  dsimp [invFunIdAssoc]
  simp

Component Formula for Natural Isomorphism in Equivalence Composition

Informal description

For any equivalence of categories $e \colon C \simeq D$, any functor $F \colon D \to E$, and any object $X$ in $D$, the component of the natural isomorphism $(e^{-1} \circ e) \circ F \cong F$ at $X$ is given by applying $F$ to the counit morphism $\epsilon_X \colon e^{-1}(e(X)) \to X$. In symbols, the homomorphism component at $X$ satisfies: $$(\text{invFunIdAssoc}\ e\ F).\text{hom}_X = F(\epsilon_X)$$

CategoryTheory.Equivalence.invFunIdAssoc_inv_app theorem

(e : C ≌ D) (F : D ⥤ E) (X : D) : (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X)

Full source

@[simp]
theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
    (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) := by
  dsimp [invFunIdAssoc]
  simp

Inverse Component Formula for Natural Isomorphism in Equivalence Composition

Informal description

For any equivalence of categories $e \colon C \simeq D$, any functor $F \colon D \to E$, and any object $X$ in $D$, the inverse component of the natural isomorphism $(e^{-1} \circ e) \circ F \cong F$ at $X$ is given by applying $F$ to the inverse counit morphism $\epsilon^{-1}_X \colon X \to e^{-1}(e(X))$. In symbols, the inverse morphism component at $X$ satisfies: $$(\text{invFunIdAssoc}\ e\ F)^{-1}_X = F(\epsilon^{-1}_X)$$

CategoryTheory.Equivalence.congrLeft definition

(e : C ≌ D) : C ⥤ E ≌ D ⥤ E

Full source

/-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
@[simps! functor inverse unitIso counitIso]
def congrLeft (e : C ≌ D) : C ⥤ EC ⥤ E ≌ D ⥤ E where
  functor := (whiskeringLeft _ _ _).obj e.inverse
  inverse := (whiskeringLeft _ _ _).obj e.functor
  unitIso := (NatIso.ofComponents fun F => (e.funInvIdAssoc F).symm)
  counitIso := (NatIso.ofComponents fun F => e.invFunIdAssoc F)
  functor_unitIso_comp F := by
    ext X
    dsimp
    simp only [funInvIdAssoc_inv_app, id_obj, comp_obj, invFunIdAssoc_hom_app,
      Functor.comp_map, ← F.map_comp, unit_inverse_comp, map_id]

Equivalence of functor categories induced by precomposition with equivalence

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the functor category $C \to E$ is equivalent to the functor category $D \to E$ via precomposition with the functors in $e$. Specifically: - The forward functor is given by precomposition with $e$'s inverse functor $G \colon D \to C$ - The inverse functor is given by precomposition with $e$'s functor $F \colon C \to D$ - The unit and counit natural isomorphisms are constructed using the associator isomorphisms and the unit/counit of $e$.

CategoryTheory.Equivalence.congrRight definition

(e : C ≌ D) : E ⥤ C ≌ E ⥤ D

Full source

/-- If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`. -/
@[simps! functor inverse unitIso counitIso]
def congrRight (e : C ≌ D) : E ⥤ CE ⥤ C ≌ E ⥤ D where
  functor := (whiskeringRight _ _ _).obj e.functor
  inverse := (whiskeringRight _ _ _).obj e.inverse
  unitIso := NatIso.ofComponents
      fun F => F.rightUnitor.symm ≪≫ isoWhiskerLeft F e.unitIso ≪≫ Functor.associator _ _ _
  counitIso := NatIso.ofComponents
      fun F => Functor.associator _ _ _ ≪≫ isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor

Equivalence of functor categories by precomposition

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the functor category $E \to C$ is equivalent to the functor category $E \to D$ via precomposition with the functors in $e$. Specifically: - The forward functor is given by precomposition with $e$'s functor $F \colon C \to D$ - The inverse functor is given by precomposition with $e$'s inverse functor $G \colon D \to C$ - The unit and counit natural isomorphisms are constructed using the unit and counit of $e$ along with appropriate whiskering and associator isomorphisms.

CategoryTheory.Equivalence.cancel_unit_right theorem

{X Y : C} (f f' : X ⟶ Y) : f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

Full source

@[simp]
theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) :
    f ≫ e.unit.app Yf ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f' := by simp only [cancel_mono]

Cancellation Property for Unit of Category Equivalence

Informal description

For any objects $X, Y$ in a category $C$ and morphisms $f, f' \colon X \to Y$, the compositions $f \circ \eta_Y$ and $f' \circ \eta_Y$ are equal if and only if $f = f'$, where $\eta$ is the unit isomorphism of the equivalence $e \colon C \simeq D$.

CategoryTheory.Equivalence.cancel_unitInv_right theorem

{X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f'

Full source

@[simp]
theorem cancel_unitInv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :
    f ≫ e.unitInv.app Yf ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f' := by simp only [cancel_mono]

Cancellation Property for Inverse Unit of Category Equivalence

Informal description

For any objects $X, Y$ in category $C$ and morphisms $f, f' \colon X \to G(F(Y))$ (where $F \colon C \to D$ and $G \colon D \to C$ are the functors in the equivalence), we have $f \circ \eta^{-1}_Y = f' \circ \eta^{-1}_Y$ if and only if $f = f'$. Here $\eta^{-1}$ is the inverse unit isomorphism of the equivalence.

CategoryTheory.Equivalence.cancel_counit_right theorem

{X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f'

Full source

@[simp]
theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) :
    f ≫ e.counit.app Yf ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f' := by simp only [cancel_mono]

Cancellation Property for Counit of Category Equivalence

Informal description

For any objects $X, Y$ in category $D$ and morphisms $f, f' \colon X \to F(G(Y))$ (where $F \colon C \to D$ and $G \colon D \to C$ are the functors in the equivalence), we have $f \circ \epsilon_Y = f' \circ \epsilon_Y$ if and only if $f = f'$. Here $\epsilon$ is the counit isomorphism of the equivalence.

CategoryTheory.Equivalence.cancel_counitInv_right theorem

{X Y : D} (f f' : X ⟶ Y) : f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'

Full source

@[simp]
theorem cancel_counitInv_right {X Y : D} (f f' : X ⟶ Y) :
    f ≫ e.counitInv.app Yf ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by simp only [cancel_mono]

Cancellation Property for Inverse Counit of Category Equivalence

Informal description

For any objects $X, Y$ in category $D$ and morphisms $f, f' \colon X \to Y$, we have $f \circ \epsilon^{-1}_Y = f' \circ \epsilon^{-1}_Y$ if and only if $f = f'$, where $\epsilon^{-1}$ is the inverse counit isomorphism of the equivalence $e \colon C \simeq D$.

CategoryTheory.Equivalence.cancel_unit_right_assoc theorem

 {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
  f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g'

Full source

@[simp]
theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
    f ≫ g ≫ e.unit.app Yf ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono]

Cancellation Property for Compositions with Unit in Category Equivalence

Informal description

For any objects $W, X, X', Y$ in category $C$ and morphisms $f \colon W \to X$, $g \colon X \to Y$, $f' \colon W \to X'$, $g' \colon X' \to Y$, the compositions $f \circ g \circ \eta_Y$ and $f' \circ g' \circ \eta_Y$ are equal if and only if $f \circ g = f' \circ g'$, where $\eta$ is the unit isomorphism of the equivalence $e \colon C \simeq D$.

CategoryTheory.Equivalence.cancel_counitInv_right_assoc theorem

 {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
  f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g'

Full source

@[simp]
theorem cancel_counitInv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
    (g' : X' ⟶ Y) : f ≫ g ≫ e.counitInv.app Yf ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono]

Cancellation Property for Compositions with Inverse Counit in Category Equivalence

Informal description

For any objects $W, X, X', Y$ in category $D$ and morphisms $f \colon W \to X$, $g \colon X \to Y$, $f' \colon W \to X'$, $g' \colon X' \to Y$, the compositions $f \circ g \circ \epsilon^{-1}_Y$ and $f' \circ g' \circ \epsilon^{-1}_Y$ are equal if and only if $f \circ g = f' \circ g'$, where $\epsilon^{-1}$ is the inverse counit isomorphism of the equivalence $e \colon C \simeq D$.

CategoryTheory.Equivalence.cancel_unit_right_assoc' theorem

 {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
  f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Full source

@[simp]
theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
    (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
    f ≫ g ≫ h ≫ e.unit.app Zf ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by
  simp only [← Category.assoc, cancel_mono]

Cancellation Property for Compositions with Unit in Category Equivalence

Informal description

For any morphisms $f \colon W \to X$, $g \colon X \to Y$, $h \colon Y \to Z$ and $f' \colon W \to X'$, $g' \colon X' \to Y'$, $h' \colon Y' \to Z$ in category $C$, the compositions $f \circ g \circ h \circ \eta_Z$ and $f' \circ g' \circ h' \circ \eta_Z$ are equal if and only if $f \circ g \circ h = f' \circ g' \circ h'$, where $\eta$ is the unit of the equivalence $e \colon C \simeq D$.

CategoryTheory.Equivalence.cancel_counitInv_right_assoc' theorem

 {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
  f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Full source

@[simp]
theorem cancel_counitInv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
    (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
    f ≫ g ≫ h ≫ e.counitInv.app Zf ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔
    f ≫ g ≫ h = f' ≫ g' ≫ h' := by simp only [← Category.assoc, cancel_mono]

Cancellation Property for Compositions with Inverse Counit in Category Equivalence

Informal description

For any morphisms $f \colon W \to X$, $g \colon X \to Y$, $h \colon Y \to Z$ and $f' \colon W \to X'$, $g' \colon X' \to Y'$, $h' \colon Y' \to Z$ in category $D$, the compositions $f \circ g \circ h \circ \epsilon^{-1}_Z$ and $f' \circ g' \circ h' \circ \epsilon^{-1}_Z$ are equal if and only if $f \circ g \circ h = f' \circ g' \circ h'$, where $\epsilon^{-1}$ is the inverse counit of the equivalence $e \colon C \simeq D$.

CategoryTheory.Equivalence.powNat definition

(e : C ≌ C) : ℕ → (C ≌ C)

Full source

/-- Natural number powers of an auto-equivalence.  Use `(^)` instead. -/
def powNat (e : C ≌ C) : ℕ → (C ≌ C)
  | 0 => Equivalence.refl
  | 1 => e
  | n + 2 => e.trans (powNat e (n + 1))

Natural number powers of an auto-equivalence

Informal description

Given an equivalence of categories $e \colon C \simeq C$ and a natural number $n$, the $n$-th power of $e$ is defined recursively as: - $e^0$ is the reflexive equivalence (identity functor) - $e^1 = e$ - $e^{n+2} = e \circ e^{n+1}$ (composition of equivalences) This defines the natural number power of an auto-equivalence of a category.

CategoryTheory.Equivalence.pow definition

(e : C ≌ C) : ℤ → (C ≌ C)

Full source

/-- Powers of an auto-equivalence.  Use `(^)` instead. -/
def pow (e : C ≌ C) : ℤ → (C ≌ C)
  | Int.ofNat n => e.powNat n
  | Int.negSucc n => e.symm.powNat (n + 1)

Integer powers of an auto-equivalence

Informal description

Given an equivalence of categories $e \colon C \simeq C$ and an integer $n$, the $n$-th power of $e$ is defined as: - For non-negative integers $n$, it is the $n$-fold composition of $e$ with itself (as defined in `powNat`). - For negative integers $-n-1$, it is the $(n+1)$-fold composition of the symmetric equivalence $e^{-1} \colon C \simeq C$ (the inverse of $e$). This defines integer powers of an auto-equivalence of a category.

CategoryTheory.Equivalence.instPowInt instance

: Pow (C ≌ C) ℤ

Full source

instance : Pow (C ≌ C) ℤ :=
  ⟨pow⟩

Integer Powers of Auto-Equivalences

Informal description

For any category $C$, the collection of auto-equivalences $C \simeq C$ forms a group under composition, where the integer power operation $e^n$ for $n \in \mathbb{Z}$ is defined as: - For $n \geq 0$, $e^n$ is the $n$-fold composition of $e$ with itself. - For $n < 0$, $e^n$ is the $|n|$-fold composition of the inverse equivalence $e^{-1}$ with itself. This operation satisfies $e^0 = \text{id}_C$ and $e^1 = e$.

CategoryTheory.Equivalence.pow_zero theorem

(e : C ≌ C) : e ^ (0 : ℤ) = Equivalence.refl

Full source

@[simp]
theorem pow_zero (e : C ≌ C) : e ^ (0 : ℤ) = Equivalence.refl :=
  rfl

Zeroth Power of Auto-Equivalence is Identity

Informal description

For any auto-equivalence $e \colon C \simeq C$ of a category $C$, the zeroth power $e^0$ is equal to the reflexive equivalence $\text{id}_C$.

CategoryTheory.Equivalence.pow_one theorem

(e : C ≌ C) : e ^ (1 : ℤ) = e

Full source

@[simp]
theorem pow_one (e : C ≌ C) : e ^ (1 : ℤ) = e :=
  rfl

First Power of Auto-Equivalence is Itself

Informal description

For any auto-equivalence $e \colon C \simeq C$ of a category $C$, the first integer power of $e$ equals $e$ itself, i.e., $e^1 = e$.

CategoryTheory.Equivalence.pow_neg_one theorem

(e : C ≌ C) : e ^ (-1 : ℤ) = e.symm

Full source

@[simp]
theorem pow_neg_one (e : C ≌ C) : e ^ (-1 : ℤ) = e.symm :=
  rfl

Negative One Power of Auto-Equivalence Equals Its Inverse

Informal description

For any auto-equivalence $e \colon C \simeq C$ of a category $C$, the $-1$ power of $e$ is equal to the symmetric equivalence $e^{-1} \colon C \simeq C$.

CategoryTheory.Equivalence.essSurj_functor instance

(e : C ≌ E) : e.functor.EssSurj

Full source

/-- The functor of an equivalence of categories is essentially surjective. -/
@[stacks 02C3]
instance essSurj_functor (e : C ≌ E) : e.functor.EssSurj :=
  ⟨fun Y => ⟨e.inverse.obj Y, ⟨e.counitIso.app Y⟩⟩⟩

Essential Surjectivity of the Functor in an Equivalence of Categories

Informal description

For any equivalence of categories $e \colon C \simeq E$, the functor $e.functor \colon C \to E$ is essentially surjective. That is, for every object $d$ in $E$, there exists an object $c$ in $C$ such that $e.functor(c)$ is isomorphic to $d$.

CategoryTheory.Equivalence.essSurj_inverse instance

(e : C ≌ E) : e.inverse.EssSurj

Full source

instance essSurj_inverse (e : C ≌ E) : e.inverse.EssSurj :=
  e.symm.essSurj_functor

Essential Surjectivity of the Inverse Functor in an Equivalence of Categories

Informal description

For any equivalence of categories $e \colon C \simeq E$, the inverse functor $e^{-1} \colon E \to C$ is essentially surjective. That is, for every object $c$ in $C$, there exists an object $d$ in $E$ such that $e^{-1}(d)$ is isomorphic to $c$.

CategoryTheory.Equivalence.fullyFaithfulFunctor definition

(e : C ≌ E) : e.functor.FullyFaithful

Full source

/-- The functor of an equivalence of categories is fully faithful. -/
def fullyFaithfulFunctor (e : C ≌ E) : e.functor.FullyFaithful where
  preimage {X Y} f := e.unitIso.hom.app X ≫ e.inverse.map f ≫ e.unitIso.inv.app Y

Fully faithfulness of the functor in an equivalence of categories

Informal description

For any equivalence of categories $e \colon C \simeq D$, the functor $e.functor \colon C \to D$ is fully faithful. This means that for any two objects $X, Y$ in $C$, the map $\text{Hom}_C(X, Y) \to \text{Hom}_D(e.functor(X), e.functor(Y))$ induced by $e.functor$ is bijective. The preimage of a morphism $f \colon e.functor(X) \to e.functor(Y)$ is given by composing with the unit and inverse unit isomorphisms of the equivalence.

CategoryTheory.Equivalence.fullyFaithfulInverse definition

(e : C ≌ E) : e.inverse.FullyFaithful

Full source

/-- The inverse of an equivalence of categories is fully faithful. -/
def fullyFaithfulInverse (e : C ≌ E) : e.inverse.FullyFaithful where
  preimage {X Y} f := e.counitIso.inv.app X ≫ e.functor.map f ≫ e.counitIso.hom.app Y

Inverse functor of an equivalence is fully faithful

Informal description

For any equivalence of categories $e \colon C \simeq D$, the inverse functor $e^{-1} \colon D \to C$ is fully faithful. This means that for any two objects $X, Y$ in $D$, the map $\text{Hom}_D(X, Y) \to \text{Hom}_C(e^{-1}X, e^{-1}Y)$ induced by $e^{-1}$ is bijective.

CategoryTheory.Equivalence.faithful_functor instance

(e : C ≌ E) : e.functor.Faithful

Full source

/-- The functor of an equivalence of categories is faithful. -/
@[stacks 02C3]
instance faithful_functor (e : C ≌ E) : e.functor.Faithful :=
  e.fullyFaithfulFunctor.faithful

Faithfulness of the Functor in an Equivalence of Categories

Informal description

For any equivalence of categories $e \colon C \simeq D$, the functor $e.\text{functor} \colon C \to D$ is faithful. This means that for any two objects $X, Y$ in $C$, the map $\text{Hom}_C(X, Y) \to \text{Hom}_D(e.\text{functor}(X), e.\text{functor}(Y))$ induced by $e.\text{functor}$ is injective.

CategoryTheory.Equivalence.faithful_inverse instance

(e : C ≌ E) : e.inverse.Faithful

Full source

instance faithful_inverse (e : C ≌ E) : e.inverse.Faithful :=
  e.fullyFaithfulInverse.faithful

Faithfulness of the Inverse Functor in an Equivalence of Categories

Informal description

For any equivalence of categories $e \colon C \simeq D$, the inverse functor $e^{-1} \colon D \to C$ is faithful. This means that for any two objects $X, Y$ in $D$, the map $\text{Hom}_D(X, Y) \to \text{Hom}_C(e^{-1}X, e^{-1}Y)$ induced by $e^{-1}$ is injective.

CategoryTheory.Equivalence.full_functor instance

(e : C ≌ E) : e.functor.Full

Full source

/-- The functor of an equivalence of categories is full. -/
@[stacks 02C3]
instance full_functor (e : C ≌ E) : e.functor.Full :=
  e.fullyFaithfulFunctor.full

Fullness of the Functor in an Equivalence of Categories

Informal description

For any equivalence of categories $e \colon C \simeq D$, the functor $e.\text{functor} \colon C \to D$ is full. This means that for any two objects $X, Y$ in $C$, the map $\text{Hom}_C(X, Y) \to \text{Hom}_D(e.\text{functor}(X), e.\text{functor}(Y))$ induced by $e.\text{functor}$ is surjective.

CategoryTheory.Equivalence.full_inverse instance

(e : C ≌ E) : e.inverse.Full

Full source

instance full_inverse (e : C ≌ E) : e.inverse.Full :=
  e.fullyFaithfulInverse.full

Fullness of the Inverse Functor in an Equivalence of Categories

Informal description

For any equivalence of categories $e \colon C \simeq D$, the inverse functor $e^{-1} \colon D \to C$ is full. This means that for any two objects $X, Y$ in $D$, the map $\text{Hom}_D(X, Y) \to \text{Hom}_C(e^{-1}X, e^{-1}Y)$ induced by $e^{-1}$ is surjective.

CategoryTheory.Equivalence.changeFunctor definition

(e : C ≌ D) {G : C ⥤ D} (iso : e.functor ≅ G) : C ≌ D

Full source

/-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is
an isomorphism, then there is an equivalence of categories whose functor is `G`. -/
@[simps!]
def changeFunctor (e : C ≌ D) {G : C ⥤ D} (iso : e.functor ≅ G) : C ≌ D where
  functor := G
  inverse := e.inverse
  unitIso := e.unitIso ≪≫ isoWhiskerRight iso _
  counitIso := isoWhiskerLeft _ iso.symm ≪≫ e.counitIso

Equivalence of Categories with Modified Functor

Informal description

Given an equivalence of categories $e \colon C \simeq D$ and an isomorphism $\text{iso} \colon e.\text{functor} \cong G$ between the functor of $e$ and another functor $G \colon C \to D$, this constructs a new equivalence of categories where the functor is replaced by $G$. The inverse functor remains $e.\text{inverse}$, while the unit and counit isomorphisms are adjusted by composing with $\text{iso}$ and its inverse appropriately.

CategoryTheory.Equivalence.changeFunctor_refl theorem

(e : C ≌ D) : e.changeFunctor (Iso.refl _) = e

Full source

/-- Compatibility of `changeFunctor` with identity isomorphisms of functors -/
theorem changeFunctor_refl (e : C ≌ D) : e.changeFunctor (Iso.refl _) = e := by aesop_cat

Identity Functor Modification Preserves Equivalence

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the modification of $e$ by replacing its functor with itself via the identity isomorphism $\text{id}_{e.\text{functor}}$ yields the original equivalence $e$.

CategoryTheory.Equivalence.changeFunctor_trans theorem

 (e : C ≌ D) {G G' : C ⥤ D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G') :
  (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Full source

/-- Compatibility of `changeFunctor` with the composition of isomorphisms of functors -/
theorem changeFunctor_trans (e : C ≌ D) {G G' : C ⥤ D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G') :
    (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂) := by aesop_cat

Composition Law for Functor Modification in Equivalence of Categories

Informal description

Given an equivalence of categories $e \colon C \simeq D$ and two isomorphisms of functors $\text{iso}_1 \colon e.\text{functor} \cong G$ and $\text{iso}_2 \colon G \cong G'$, the composition of the modifications of $e$ via $\text{iso}_1$ and then $\text{iso}_2$ is equal to modifying $e$ via the composition $\text{iso}_1 \circ \text{iso}_2$. That is, $(e.\text{changeFunctor} \text{iso}_1).\text{changeFunctor} \text{iso}_2 = e.\text{changeFunctor} (\text{iso}_1 \circ \text{iso}_2)$.

CategoryTheory.Equivalence.changeInverse definition

(e : C ≌ D) {G : D ⥤ C} (iso : e.inverse ≅ G) : C ≌ D

Full source

/-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is
an isomorphism, then there is an equivalence of categories whose inverse is `G`. -/
@[simps!]
def changeInverse (e : C ≌ D) {G : D ⥤ C} (iso : e.inverse ≅ G) : C ≌ D where
  functor := e.functor
  inverse := G
  unitIso := e.unitIso ≪≫ isoWhiskerLeft _ iso
  counitIso := isoWhiskerRightisoWhiskerRight iso.symm _ ≪≫ e.counitIso
  functor_unitIso_comp X := by
    dsimp
    rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]

Equivalence of categories with modified inverse functor

Informal description

Given an equivalence of categories $e \colon C \simeq D$ and an isomorphism $\text{iso} \colon e.\text{inverse} \cong G$ between the inverse functor of $e$ and another functor $G \colon D \to C$, we can construct a new equivalence of categories where: - The forward functor remains $e.\text{functor} \colon C \to D$, - The inverse functor is replaced by $G$, - The unit isomorphism is modified to $e.\text{unitIso} \circ (\text{id}_C \times \text{iso})$, - The counit isomorphism is modified to $(\text{iso}^{-1} \times \text{id}_D) \circ e.\text{counitIso}$. This construction preserves the equivalence structure while changing the inverse functor.

CategoryTheory.Functor.IsEquivalence structure

(F : C ⥤ D)

Full source

/-- A functor is an equivalence of categories if it is faithful, full and
essentially surjective. -/
class Functor.IsEquivalence (F : C ⥤ D) : Prop where
  faithful : F.Faithful := by infer_instance
  full : F.Full := by infer_instance
  essSurj : F.EssSurj := by infer_instance

Equivalence of Categories (Functor Condition)

Informal description

A functor $F \colon C \to D$ is an equivalence of categories if it is faithful, full, and essentially surjective. This means: 1. $F$ is injective on morphisms (faithful), 2. $F$ is surjective on morphisms between any two objects in its image (full), and 3. For every object $d$ in $D$, there exists an object $c$ in $C$ such that $F(c)$ is isomorphic to $d$ (essentially surjective).

CategoryTheory.Equivalence.isEquivalence_functor instance

(F : C ≌ D) : IsEquivalence F.functor

Full source

instance Equivalence.isEquivalence_functor (F : C ≌ D) : IsEquivalence F.functor where

The Forward Functor in an Equivalence is an Equivalence

Informal description

For any equivalence of categories $F \colon C \simeq D$, the functor $F.\text{functor} \colon C \to D$ is an equivalence of categories. This means that $F.\text{functor}$ is full, faithful, and essentially surjective.

CategoryTheory.Equivalence.isEquivalence_inverse instance

(F : C ≌ D) : IsEquivalence F.inverse

Full source

instance Equivalence.isEquivalence_inverse (F : C ≌ D) : IsEquivalence F.inverse :=
  F.symm.isEquivalence_functor

The Inverse Functor in an Equivalence is an Equivalence

Informal description

For any equivalence of categories $F \colon C \simeq D$, the inverse functor $F.\text{inverse} \colon D \to C$ is an equivalence of categories. This means that $F.\text{inverse}$ is full, faithful, and essentially surjective.

CategoryTheory.Functor.IsEquivalence.mk' theorem

{F : C ⥤ D} (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : IsEquivalence F

Full source

/-- To see that a functor is an equivalence, it suffices to provide an inverse functor `G` such that
    `F ⋙ G` and `G ⋙ F` are naturally isomorphic to identity functors. -/
protected lemma mk' {F : C ⥤ D} (G : D ⥤ C) (η : 𝟭𝟭 C ≅ F ⋙ G) (ε : G ⋙ FG ⋙ F ≅ 𝟭 D) :
    IsEquivalence F :=
  inferInstanceAs (IsEquivalence (Equivalence.mk F G η ε).functor)

Equivalence of Categories via Natural Isomorphisms

Informal description

Given functors $F \colon C \to D$ and $G \colon D \to C$, along with natural isomorphisms $\eta \colon \text{id}_C \cong F \circ G$ and $\varepsilon \colon G \circ F \cong \text{id}_D$, the functor $F$ is an equivalence of categories.

CategoryTheory.Functor.inv definition

(F : C ⥤ D) [F.IsEquivalence] : D ⥤ C

Full source

/-- A quasi-inverse `D ⥤ C` to a functor that `F : C ⥤ D` that is an equivalence,
i.e. faithful, full, and essentially surjective. -/
noncomputable def inv (F : C ⥤ D) [F.IsEquivalence] : D ⥤ C where
  obj X := F.objPreimage X
  map {X Y} f := F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
  map_id X := by apply F.map_injective; simp
  map_comp {X Y Z} f g := by apply F.map_injective; simp

Quasi-inverse functor of an equivalence

Informal description

Given a functor $F \colon C \to D$ that is an equivalence of categories (i.e., faithful, full, and essentially surjective), the quasi-inverse functor $F^{-1} \colon D \to C$ is defined as follows: - On objects: $F^{-1}(X) = c_X$, where $c_X$ is a chosen preimage of $X$ under $F$ (i.e., $F(c_X) \cong X$). - On morphisms: For a morphism $f \colon X \to Y$ in $D$, the morphism $F^{-1}(f) \colon F^{-1}(X) \to F^{-1}(Y)$ is the unique morphism in $C$ that $F$ maps to the composition $(F(c_X) \cong X) \xrightarrow{f} (Y \cong F(c_Y))$. This construction ensures that $F^{-1}$ is indeed a functor and forms an equivalence with $F$.

CategoryTheory.Functor.asEquivalence definition

(F : C ⥤ D) [F.IsEquivalence] : C ≌ D

Full source

/-- Interpret a functor that is an equivalence as an equivalence. -/
@[simps functor, stacks 02C3]
noncomputable def asEquivalence (F : C ⥤ D) [F.IsEquivalence] : C ≌ D where
  functor := F
  inverse := F.inv
  unitIso := NatIso.ofComponents
    (fun X => (F.preimageIso <| F.objObjPreimageIso <| F.obj X).symm)
      (fun f => F.map_injective (by simp [inv]))
  counitIso := NatIso.ofComponents F.objObjPreimageIso (by simp [inv])

Equivalence from an equivalence functor

Informal description

Given a functor $F \colon C \to D$ that is an equivalence of categories (i.e., faithful, full, and essentially surjective), the construction `asEquivalence` packages $F$ together with its quasi-inverse $F^{-1}$ into an equivalence of categories $C \simeq D$. This equivalence includes: - The functor $F$ itself, - The quasi-inverse functor $F^{-1} \colon D \to C$, - A natural isomorphism $\eta \colon \text{id}_C \cong F \circ F^{-1}$, - A natural isomorphism $\epsilon \colon F^{-1} \circ F \cong \text{id}_D$. The natural isomorphisms satisfy the triangle identities making this a half-adjoint equivalence.

CategoryTheory.Functor.isEquivalence_refl instance

: IsEquivalence (𝟭 C)

Full source

instance isEquivalence_refl : IsEquivalence (𝟭 C) :=
  Equivalence.refl.isEquivalence_functor

Identity Functor is an Equivalence

Informal description

The identity functor $\text{id}_C \colon C \to C$ is an equivalence of categories.

CategoryTheory.Functor.isEquivalence_inv instance

(F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv

Full source

instance isEquivalence_inv (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv :=
  F.asEquivalence.symm.isEquivalence_functor

Quasi-inverse of an Equivalence is an Equivalence

Informal description

For any equivalence of categories $F \colon C \to D$, the quasi-inverse functor $F^{-1} \colon D \to C$ is also an equivalence of categories.

CategoryTheory.Functor.isEquivalence_trans instance

(F : C ⥤ D) (G : D ⥤ E) [IsEquivalence F] [IsEquivalence G] : IsEquivalence (F ⋙ G)

Full source

instance isEquivalence_trans (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence F] [IsEquivalence G] :
    IsEquivalence (F ⋙ G) where

Composition of Equivalences is an Equivalence

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ that are equivalences of categories, their composition $F \circ G \colon C \to E$ is also an equivalence of categories.

CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft instance

(F : C ⥤ D) [IsEquivalence F] : IsEquivalence ((whiskeringLeft C D E).obj F)

Full source

instance (F : C ⥤ D) [IsEquivalence F] : IsEquivalence ((whiskeringLeft C D E).obj F) :=
  (inferInstance : IsEquivalence (Equivalence.congrLeft F.asEquivalence).inverse)

Precomposition with an Equivalence is an Equivalence

Informal description

For any equivalence of categories $F \colon C \to D$, the functor obtained by precomposing with $F$ (i.e., the whiskering left functor $(- \circ F) \colon (D \to E) \to (C \to E)$) is also an equivalence of categories.

CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight instance

(F : C ⥤ D) [IsEquivalence F] : IsEquivalence ((whiskeringRight E C D).obj F)

Full source

instance (F : C ⥤ D) [IsEquivalence F] : IsEquivalence ((whiskeringRight E C D).obj F) :=
  (inferInstance : IsEquivalence (Equivalence.congrRight F.asEquivalence).functor)

Post-composition with an equivalence is an equivalence

Informal description

Given a functor $F \colon C \to D$ that is an equivalence of categories, the functor obtained by post-composing with $F$ (i.e., the whiskering right functor $(F \circ -) \colon (E \to C) \to (E \to D)$) is also an equivalence of categories.

CategoryTheory.Functor.fun_inv_map theorem

 (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) :
  F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y

Full source

@[simp]
theorem fun_inv_map (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) :
    F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y := by
  simpa using (NatIso.naturality_2 (α := F.asEquivalence.counitIso) (f := f)).symm

Functor Image of Quasi-inverse Morphism via Equivalence

Informal description

Let $F \colon C \to D$ be an equivalence of categories, and let $X, Y$ be objects in $D$ with a morphism $f \colon X \to Y$. Then the image of $f$ under the functor $F$ applied to the quasi-inverse functor $F^{-1}$ satisfies: \[ F(F^{-1}(f)) = \epsilon_X \circ f \circ \epsilon^{-1}_Y, \] where $\epsilon \colon F \circ F^{-1} \Rightarrow \text{id}_D$ is the counit natural isomorphism of the equivalence, and $\epsilon^{-1}$ is its inverse.

CategoryTheory.Functor.inv_fun_map theorem

 (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) :
  F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y

Full source

@[simp]
theorem inv_fun_map (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) :
    F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y := by
  simpa using (NatIso.naturality_1 (α := F.asEquivalence.unitIso) (f := f)).symm

Quasi-inverse Functor Image of Morphism via Equivalence

Informal description

Let $F \colon C \to D$ be an equivalence of categories, and let $X, Y$ be objects in $C$ with a morphism $f \colon X \to Y$. Then the image of $f$ under the quasi-inverse functor $F^{-1}$ applied to $F$ satisfies: \[ F^{-1}(F(f)) = \eta^{-1}_X \circ f \circ \eta_Y, \] where $\eta \colon \text{id}_C \Rightarrow F \circ F^{-1}$ is the unit natural isomorphism of the equivalence, and $\eta^{-1}$ is its inverse.

CategoryTheory.Functor.isEquivalence_of_iso theorem

{F G : C ⥤ D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence

Full source

lemma isEquivalence_of_iso {F G : C ⥤ D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence :=
  ((asEquivalence F).changeFunctor e).isEquivalence_functor

Equivalence of Categories is Preserved by Natural Isomorphism

Informal description

Given two functors $F, G \colon C \to D$ and a natural isomorphism $e \colon F \cong G$, if $F$ is an equivalence of categories (i.e., full, faithful, and essentially surjective), then $G$ is also an equivalence of categories.

CategoryTheory.Functor.isEquivalence_iff_of_iso theorem

{F G : C ⥤ D} (e : F ≅ G) : F.IsEquivalence ↔ G.IsEquivalence

Full source

lemma isEquivalence_iff_of_iso {F G : C ⥤ D} (e : F ≅ G) :
    F.IsEquivalence ↔ G.IsEquivalence :=
  ⟨fun _ => isEquivalence_of_iso e, fun _ => isEquivalence_of_iso e.symm⟩

Equivalence of Categories is Preserved Under Natural Isomorphism

Informal description

Given two functors $F, G \colon C \to D$ and a natural isomorphism $e \colon F \cong G$, the functor $F$ is an equivalence of categories if and only if $G$ is an equivalence of categories.

CategoryTheory.Functor.isEquivalence_of_comp_right theorem

{E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence G] [IsEquivalence (F ⋙ G)] : IsEquivalence F

Full source

/-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/
lemma isEquivalence_of_comp_right {E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E)
    [IsEquivalence G] [IsEquivalence (F ⋙ G)] : IsEquivalence F := by
  rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]
  exact ((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

Equivalence of categories via right composition

Informal description

Let $C$, $D$, and $E$ be categories, and let $F \colon C \to D$ and $G \colon D \to E$ be functors. If $G$ and the composition $F \circ G \colon C \to E$ are equivalences of categories, then $F$ is also an equivalence of categories.

CategoryTheory.Functor.isEquivalence_of_comp_left theorem

{E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence F] [IsEquivalence (F ⋙ G)] : IsEquivalence G

Full source

/-- If `F` and `F ⋙ G` are equivalence of categories, then `G` is also an equivalence. -/
lemma isEquivalence_of_comp_left {E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E)
    [IsEquivalence F] [IsEquivalence (F ⋙ G)] : IsEquivalence G := by
  rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)]
  exact (F.asEquivalence.symm.trans (F ⋙ G).asEquivalence).isEquivalence_functor

Equivalence of Categories via Composition with Left Equivalence

Informal description

Let $C$, $D$, and $E$ be categories, and let $F \colon C \to D$ and $G \colon D \to E$ be functors. If $F$ is an equivalence of categories and the composition $F \circ G \colon C \to E$ is also an equivalence of categories, then $G$ is an equivalence of categories.

CategoryTheory.Equivalence.essSurjInducedFunctor instance

{C' : Type*} (e : C' ≃ D) : (inducedFunctor e).EssSurj

Full source

instance essSurjInducedFunctor {C' : Type*} (e : C' ≃ D) : (inducedFunctor e).EssSurj where
  mem_essImage Y := ⟨e.symm Y, by simpa using ⟨default⟩⟩

Essential Surjectivity of Induced Functor from Type Equivalence

Informal description

For any equivalence $e \colon C' \simeq D$ of types, the induced functor $\text{inducedFunctor}\, e$ is essentially surjective. That is, for every object $d$ in $D$, there exists an object $c$ in $C'$ such that $(\text{inducedFunctor}\, e)(c)$ is isomorphic to $d$.

CategoryTheory.Equivalence.inducedFunctorOfEquiv instance

{C' : Type*} (e : C' ≃ D) : IsEquivalence (inducedFunctor e)

Full source

noncomputable instance inducedFunctorOfEquiv {C' : Type*} (e : C' ≃ D) :
    IsEquivalence (inducedFunctor e) where

Equivalence of Categories Induced by Type Equivalence

Informal description

For any equivalence $e \colon C' \simeq D$ of types, the induced functor $\text{inducedFunctor}\, e$ is an equivalence of categories.

CategoryTheory.Equivalence.fullyFaithfulToEssImage instance

(F : C ⥤ D) [F.Full] [F.Faithful] : IsEquivalence F.toEssImage

Full source

noncomputable instance fullyFaithfulToEssImage (F : C ⥤ D) [F.Full] [F.Faithful] :
    IsEquivalence F.toEssImage where

Full and Faithful Functors Induce Equivalence on Essential Image

Informal description

For any full and faithful functor $F \colon C \to D$, the restriction of $F$ to its essential image $F.\text{toEssImage}$ is an equivalence of categories.

CategoryTheory.ObjectProperty.fullSubcategoryCongr definition

{P P' : ObjectProperty C} (h : P = P') : P.FullSubcategory ≌ P'.FullSubcategory

Full source

/-- An equality of properties of objects of a category `C` induces an equivalence of the
respective induced full subcategories of `C`. -/
@[simps]
def ObjectProperty.fullSubcategoryCongr {P P' : ObjectProperty C} (h : P = P') :
    P.FullSubcategory ≌ P'.FullSubcategory where
  functor := ObjectProperty.ιOfLE h.le
  inverse := ObjectProperty.ιOfLE h.symm.le
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Equivalence of full subcategories induced by equal object properties

Informal description

Given two object properties $P$ and $P'$ of a category $C$ that are equal ($P = P'$), this defines an equivalence of categories between their respective full subcategories $P.\text{FullSubcategory}$ and $P'.\text{FullSubcategory}$. The equivalence is constructed using the inclusion functors and identity natural isomorphisms.

CategoryTheory.Iso.compInverseIso definition

{H : D ≌ E} (i : F ≅ G ⋙ H.functor) : F ⋙ H.inverse ≅ G

Full source

/-- Construct an isomorphism `F ⋙ H.inverse ≅ G` from an isomorphism `F ≅ G ⋙ H.functor`. -/
@[simps!]
def compInverseIso {H : D ≌ E} (i : F ≅ G ⋙ H.functor) : F ⋙ H.inverseF ⋙ H.inverse ≅ G :=
  isoWhiskerRightisoWhiskerRight i H.inverse ≪≫
    associator G _ H.inverse ≪≫ isoWhiskerLeft G H.unitIso.symm ≪≫ G.rightUnitor

Isomorphism from composition with equivalence inverse

Informal description

Given an equivalence of categories $H \colon D \simeq E$ and a natural isomorphism $i \colon F \cong G \circ H.functor$, this constructs a natural isomorphism $F \circ H.inverse \cong G$. The construction uses: 1. The whiskering of $i$ with $H.inverse$ on the right, 2. The associator isomorphism between $G$, $H.functor$, and $H.inverse$, 3. The whiskering of the inverse of $H$'s unit isomorphism with $G$ on the left, and 4. The right unitor isomorphism for $G$.

CategoryTheory.Iso.isoCompInverse definition

{H : D ≌ E} (i : G ⋙ H.functor ≅ F) : G ≅ F ⋙ H.inverse

Full source

/-- Construct an isomorphism `G ≅ F ⋙ H.inverse` from an isomorphism `G ⋙ H.functor ≅ F`. -/
@[simps!]
def isoCompInverse {H : D ≌ E} (i : G ⋙ H.functorG ⋙ H.functor ≅ F) : G ≅ F ⋙ H.inverse :=
  G.rightUnitor.symm ≪≫ isoWhiskerLeft G H.unitIso ≪≫ (associator _ _ _).symm ≪≫
    isoWhiskerRight i H.inverse

Isomorphism from composition with equivalence functor to inverse composition

Informal description

Given an equivalence of categories $H \colon D \simeq E$ and a natural isomorphism $i \colon G \circ H.functor \cong F$, this constructs a natural isomorphism $G \cong F \circ H.inverse$. The construction uses: 1. The inverse of the right unitor isomorphism for $G$, 2. The whiskering of $H$'s unit isomorphism with $G$ on the left, 3. The inverse of the associator isomorphism, and 4. The whiskering of $i$ with $H.inverse$ on the right.

CategoryTheory.Iso.inverseCompIso definition

{G : C ≌ D} (i : F ≅ G.functor ⋙ H) : G.inverse ⋙ F ≅ H

Full source

/-- Construct an isomorphism `G.inverse ⋙ F ≅ H` from an isomorphism `F ≅ G.functor ⋙ H`. -/
@[simps!]
def inverseCompIso {G : C ≌ D} (i : F ≅ G.functor ⋙ H) : G.inverse ⋙ FG.inverse ⋙ F ≅ H :=
  isoWhiskerLeftisoWhiskerLeft G.inverse i ≪≫ (associator _ _ _).symm ≪≫
    isoWhiskerRight G.counitIso H ≪≫ H.leftUnitor

Isomorphism from inverse composition with equivalence functor

Informal description

Given an equivalence of categories $G \colon C \simeq D$ and a natural isomorphism $i \colon F \cong G.functor \circ H$, this constructs a natural isomorphism $G.inverse \circ F \cong H$. The construction uses: 1. The whiskering of $i$ with $G.inverse$ on the left, 2. The inverse of the associator isomorphism, 3. The whiskering of $G$'s counit isomorphism with $H$ on the right, and 4. The left unitor isomorphism for $H$.

CategoryTheory.Iso.isoInverseComp definition

{G : C ≌ D} (i : G.functor ⋙ H ≅ F) : H ≅ G.inverse ⋙ F

Full source

/-- Construct an isomorphism `H ≅ G.inverse ⋙ F` from an isomorphism `G.functor ⋙ H ≅ F`. -/
@[simps!]
def isoInverseComp {G : C ≌ D} (i : G.functor ⋙ HG.functor ⋙ H ≅ F) : H ≅ G.inverse ⋙ F :=
  H.leftUnitor.symm ≪≫ isoWhiskerRight G.counitIso.symm H ≪≫ associator _ _ _
    ≪≫ isoWhiskerLeft G.inverse i

Isomorphism from equivalence functor composition to inverse composition

Informal description

Given an equivalence of categories $G \colon C \simeq D$ and a natural isomorphism $i \colon G.functor \circ H \cong F$, this constructs a natural isomorphism $H \cong G.inverse \circ F$. The construction uses: 1. The inverse of the left unitor isomorphism for $H$, 2. The whiskering of the inverse of $G$'s counit isomorphism with $H$ on the right, 3. The associator isomorphism, and 4. The whiskering of $i$ with $G.inverse$ on the left.

CategoryTheory.Iso.isoInverseOfIsoFunctor definition

{G G' : C ≌ D} (i : G.functor ≅ G'.functor) : G.inverse ≅ G'.inverse

Full source

/-- As a special case, given two equivalences `G` and `G'` between the same categories,
 construct an isomorphism `G.inverse ≅ G.inverse` from an isomorphism `G.functor ≅ G.functor`. -/
@[simps!]
def isoInverseOfIsoFunctor {G G' : C ≌ D} (i : G.functor ≅ G'.functor) : G.inverse ≅ G'.inverse :=
  isoCompInverseisoCompInverse ((isoWhiskerLeft G.inverse i).symm ≪≫ G.counitIso) ≪≫ leftUnitor G'.inverse

Isomorphism of inverse functors from isomorphism of forward functors

Informal description

Given two equivalences of categories $G, G' \colon C \simeq D$ and a natural isomorphism $i \colon G.functor \cong G'.functor$, this constructs a natural isomorphism $G.inverse \cong G'.inverse$ between their inverse functors. The construction uses: 1. The inverse of the whiskering of $i$ with $G.inverse$ on the left, 2. The counit isomorphism of $G$, 3. The composition with the inverse functor, and 4. The left unitor isomorphism for $G'.inverse$.

CategoryTheory.Iso.isoFunctorOfIsoInverse definition

{G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) : G.functor ≅ G'.functor

Full source

/-- As a special case, given two equivalences `G` and `G'` between the same categories,
 construct an isomorphism `G.functor ≅ G.functor` from an isomorphism `G.inverse ≅ G.inverse`. -/
@[simps!]
def isoFunctorOfIsoInverse {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) : G.functor ≅ G'.functor :=
  isoInverseOfIsoFunctor (G := G.symm) (G' := G'.symm) i

Isomorphism of forward functors from isomorphism of inverse functors

Informal description

Given two equivalences of categories $G, G' \colon C \simeq D$ and a natural isomorphism $i \colon G.inverse \cong G'.inverse$ between their inverse functors, this constructs a natural isomorphism $G.functor \cong G'.functor$ between their forward functors. The construction is obtained by applying the inverse construction to the symmetric equivalences $G.symm$ and $G'.symm$ with the given isomorphism $i$.

CategoryTheory.Iso.isoFunctorOfIsoInverse_isoInverseOfIsoFunctor theorem

{G G' : C ≌ D} (i : G.functor ≅ G'.functor) : isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i) = i

Full source

/-- Sanity check: `isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i)` is just `i`. -/
@[simp]
lemma isoFunctorOfIsoInverse_isoInverseOfIsoFunctor {G G' : C ≌ D} (i : G.functor ≅ G'.functor) :
    isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i) = i := by
  ext X
  simp [← NatTrans.naturality]

Inverse Construction Roundtrip for Functor Isomorphisms in Category Equivalence

Informal description

For any two equivalences of categories $G, G' \colon C \simeq D$ and any natural isomorphism $i \colon G.functor \cong G'.functor$, the composition of the constructions `isoInverseOfIsoFunctor` followed by `isoFunctorOfIsoInverse` applied to $i$ yields back $i$ itself. In other words, the following equality holds: \[ \text{isoFunctorOfIsoInverse}(\text{isoInverseOfIsoFunctor}(i)) = i \]

CategoryTheory.Iso.isoInverseOfIsoFunctor_isoFunctorOfIsoInverse theorem

{G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) : isoInverseOfIsoFunctor (isoFunctorOfIsoInverse i) = i

Full source

@[simp]
lemma isoInverseOfIsoFunctor_isoFunctorOfIsoInverse {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) :
    isoInverseOfIsoFunctor (isoFunctorOfIsoInverse i) = i :=
  isoFunctorOfIsoInverse_isoInverseOfIsoFunctor (G := G.symm) (G' := G'.symm) i

Roundtrip Isomorphism Preservation for Inverse Functors in Category Equivalence

Informal description

For any two equivalences of categories $G, G' \colon C \simeq D$ and any natural isomorphism $i \colon G.inverse \cong G'.inverse$ between their inverse functors, the composition of the constructions `isoFunctorOfIsoInverse` followed by `isoInverseOfIsoFunctor` applied to $i$ yields back $i$ itself. In other words, the following equality holds: \[ \text{isoInverseOfIsoFunctor}(\text{isoFunctorOfIsoInverse}(i)) = i \]

Mathlib.CategoryTheory.Equivalence

Main definitions

Main results

Notations