mathlib docs: category_theory.equivalence

source

structure category_theory.equivalence (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

Type (max u₁ u₂ v₁ v₂)

functor : C ⥤ D
inverse : D ⥤ C
unit_iso : 𝟭 C ≅ c.functor ⋙ c.inverse
counit_iso : c.inverse ⋙ c.functor ≅ 𝟭 D
functor_unit_iso_comp' : (∀ (X : C), c.functor.map (c.unit_iso.hom.app X) ≫ c.counit_iso.hom.app (c.functor.obj X) = 𝟙 (c.functor.obj X)) . "obviously"

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.

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.

See https://stacks.math.columbia.edu/tag/001J

source

def category_theory.equivalence.unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

𝟭 C ⟶ e.functor ⋙ e.inverse

source

def category_theory.equivalence.counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.inverse ⋙ e.functor ⟶ 𝟭 D

source

def category_theory.equivalence.unit_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.functor ⋙ e.inverse ⟶ 𝟭 C

source

def category_theory.equivalence.counit_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

𝟭 D ⟶ e.inverse ⋙ e.functor

source

@[simp]

theorem category_theory.equivalence.equivalence_mk'_unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (functor : C ⥤ D) (inverse : D ⥤ C) (unit_iso : 𝟭 C ≅ functor ⋙ inverse) (counit_iso : inverse ⋙ functor ≅ 𝟭 D) (f : (∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)) . "obviously") :

{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.unit = unit_iso.hom

source

@[simp]

theorem category_theory.equivalence.equivalence_mk'_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (functor : C ⥤ D) (inverse : D ⥤ C) (unit_iso : 𝟭 C ≅ functor ⋙ inverse) (counit_iso : inverse ⋙ functor ≅ 𝟭 D) (f : (∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)) . "obviously") :

{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.counit = counit_iso.hom

source

@[simp]

theorem category_theory.equivalence.equivalence_mk'_unit_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (functor : C ⥤ D) (inverse : D ⥤ C) (unit_iso : 𝟭 C ≅ functor ⋙ inverse) (counit_iso : inverse ⋙ functor ≅ 𝟭 D) (f : (∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)) . "obviously") :

{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.unit_inv = unit_iso.inv

source

@[simp]

theorem category_theory.equivalence.equivalence_mk'_counit_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (functor : C ⥤ D) (inverse : D ⥤ C) (unit_iso : 𝟭 C ≅ functor ⋙ inverse) (counit_iso : inverse ⋙ functor ≅ 𝟭 D) (f : (∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)) . "obviously") :

{functor := functor, inverse := inverse, unit_iso := unit_iso, counit_iso := counit_iso, functor_unit_iso_comp' := f}.counit_inv = counit_iso.inv

source

@[simp]

theorem category_theory.equivalence.functor_unit_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X)

source

@[simp]

theorem category_theory.equivalence.counit_inv_functor_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

e.counit_inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_inv.app X) = 𝟙 (e.functor.obj X)

source

theorem category_theory.equivalence.functor_unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

e.functor.map (e.unit.app X) = e.counit_inv.app (e.functor.obj X)

source

theorem category_theory.equivalence.counit_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

e.counit.app (e.functor.obj X) = e.functor.map (e.unit_inv.app X)

source

@[simp]

theorem category_theory.equivalence.unit_inverse_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (Y : D) :

e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)

The other triangle equality. The proof follows the following proof in Globular: http://globular.science/1905.001

source

@[simp]

theorem category_theory.equivalence.inverse_counit_inv_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (Y : D) :

e.inverse.map (e.counit_inv.app Y) ≫ e.unit_inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)

source

theorem category_theory.equivalence.unit_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (Y : D) :

e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counit_inv.app Y)

source

theorem category_theory.equivalence.inverse_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (Y : D) :

e.inverse.map (e.counit.app Y) = e.unit_inv.app (e.inverse.obj Y)

source

@[simp]

theorem category_theory.equivalence.fun_inv_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :

e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counit_inv.app Y

source

@[simp]

theorem category_theory.equivalence.inv_fun_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) :

e.inverse.map (e.functor.map f) = e.unit_inv.app X ≫ f ≫ e.unit.app Y

source

def category_theory.equivalence.adjointify_η {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) :

𝟭 C ≅ F ⋙ G

Equations

category_theory.equivalence.adjointify_η η ε = (((((η ≪≫ category_theory.iso_whisker_left F G.left_unitor.symm) ≪≫ category_theory.iso_whisker_left F (category_theory.iso_whisker_right ε.symm G)) ≪≫ category_theory.iso_whisker_left F (G.associator F G)) ≪≫ (F.associator G (F ⋙ G)).symm) ≪≫ category_theory.iso_whisker_right η.symm (F ⋙ G)) ≪≫ (F ⋙ G).left_unitor

source

theorem category_theory.equivalence.adjointify_η_ε {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) (X : C) :

F.map ((category_theory.equivalence.adjointify_η η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)

source

def category_theory.equivalence.mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) :

C ≌ D

Equations

category_theory.equivalence.mk F G η ε = {functor := F, inverse := G, unit_iso := category_theory.equivalence.adjointify_η η ε, counit_iso := ε, functor_unit_iso_comp' := _}

source

@[simp]

theorem category_theory.equivalence.refl_counit_iso {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.counit_iso = category_theory.iso.refl (𝟭 C ⋙ 𝟭 C)

source

@[simp]

theorem category_theory.equivalence.refl_inverse {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.inverse = 𝟭 C

source

@[simp]

theorem category_theory.equivalence.refl_unit_iso {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.unit_iso = category_theory.iso.refl (𝟭 C)

source

def category_theory.equivalence.refl {C : Type u₁} [category_theory.category C] :

C ≌ C

Equations

category_theory.equivalence.refl = {functor := 𝟭 C _inst_1, inverse := 𝟭 C _inst_1, unit_iso := category_theory.iso.refl (𝟭 C), counit_iso := category_theory.iso.refl (𝟭 C ⋙ 𝟭 C), functor_unit_iso_comp' := _}

source

@[simp]

theorem category_theory.equivalence.refl_functor {C : Type u₁} [category_theory.category C] :

category_theory.equivalence.refl.functor = 𝟭 C

source

@[simp]

theorem category_theory.equivalence.symm_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.inverse = e.functor

source

@[simp]

theorem category_theory.equivalence.symm_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.functor = e.inverse

source

def category_theory.equivalence.symm {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

D ≌ C

Equations

e.symm = {functor := e.inverse, inverse := e.functor, unit_iso := e.counit_iso.symm, counit_iso := e.unit_iso.symm, functor_unit_iso_comp' := _}

source

@[simp]

theorem category_theory.equivalence.symm_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.unit_iso = e.counit_iso.symm

source

@[simp]

theorem category_theory.equivalence.symm_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

e.symm.counit_iso = e.unit_iso.symm

source

def category_theory.equivalence.trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (f : D ≌ E) :

C ≌ E

Equations

e.trans f = {functor := e.functor ⋙ f.functor, inverse := f.inverse ⋙ e.inverse, unit_iso := e.unit_iso ≪≫ category_theory.iso_whisker_left e.functor (category_theory.iso_whisker_right f.unit_iso e.inverse), counit_iso := category_theory.iso_whisker_left f.inverse (category_theory.iso_whisker_right e.counit_iso f.functor) ≪≫ f.counit_iso, functor_unit_iso_comp' := _}

source

@[simp]

theorem category_theory.equivalence.trans_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (f : D ≌ E) :

(e.trans f).functor = e.functor ⋙ f.functor

source

@[simp]

theorem category_theory.equivalence.trans_counit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (f : D ≌ E) :

(e.trans f).counit_iso = category_theory.iso_whisker_left f.inverse (category_theory.iso_whisker_right e.counit_iso f.functor) ≪≫ f.counit_iso

source

@[simp]

theorem category_theory.equivalence.trans_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (f : D ≌ E) :

(e.trans f).inverse = f.inverse ⋙ e.inverse

source

@[simp]

theorem category_theory.equivalence.trans_unit_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (f : D ≌ E) :

(e.trans f).unit_iso = e.unit_iso ≪≫ category_theory.iso_whisker_left e.functor (category_theory.iso_whisker_right f.unit_iso e.inverse)

source

def category_theory.equivalence.fun_inv_id_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (F : C ⥤ E) :

e.functor ⋙ e.inverse ⋙ F ≅ F

Equations

e.fun_inv_id_assoc F = (e.functor.associator e.inverse F).symm ≪≫ category_theory.iso_whisker_right e.unit_iso.symm F ≪≫ F.left_unitor

source

@[simp]

theorem category_theory.equivalence.fun_inv_id_assoc_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (F : C ⥤ E) (X : C) :

(e.fun_inv_id_assoc F).hom.app X = F.map (e.unit_inv.app X)

source

@[simp]

theorem category_theory.equivalence.fun_inv_id_assoc_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (F : C ⥤ E) (X : C) :

(e.fun_inv_id_assoc F).inv.app X = F.map (e.unit.app X)

source

def category_theory.equivalence.inv_fun_id_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (F : D ⥤ E) :

e.inverse ⋙ e.functor ⋙ F ≅ F

Equations

e.inv_fun_id_assoc F = (e.inverse.associator e.functor F).symm ≪≫ category_theory.iso_whisker_right e.counit_iso F ≪≫ F.left_unitor

source

@[simp]

theorem category_theory.equivalence.inv_fun_id_assoc_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (F : D ⥤ E) (X : D) :

(e.inv_fun_id_assoc F).hom.app X = F.map (e.counit.app X)

source

@[simp]

theorem category_theory.equivalence.inv_fun_id_assoc_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (e : C ≌ D) (F : D ⥤ E) (X : D) :

(e.inv_fun_id_assoc F).inv.app X = F.map (e.counit_inv.app X)

source

@[simp]

theorem category_theory.equivalence.cancel_unit_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ Y) :

f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

source

@[simp]

theorem category_theory.equivalence.cancel_unit_inv_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :

f ≫ e.unit_inv.app Y = f' ≫ e.unit_inv.app Y ↔ f = f'

source

@[simp]

theorem category_theory.equivalence.cancel_counit_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {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'

source

@[simp]

theorem category_theory.equivalence.cancel_counit_inv_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ Y) :

f ≫ e.counit_inv.app Y = f' ≫ e.counit_inv.app Y ↔ f = f'

source

@[simp]

theorem category_theory.equivalence.cancel_unit_right_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {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'

source

@[simp]

theorem category_theory.equivalence.cancel_counit_inv_right_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :

f ≫ g ≫ e.counit_inv.app Y = f' ≫ g' ≫ e.counit_inv.app Y ↔ f ≫ g = f' ≫ g'

source

@[simp]

theorem category_theory.equivalence.cancel_unit_right_assoc' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {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'

source

@[simp]

theorem category_theory.equivalence.cancel_counit_inv_right_assoc' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {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.counit_inv.app Z = f' ≫ g' ≫ h' ≫ e.counit_inv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

source

def category_theory.equivalence.pow {C : Type u₁} [category_theory.category C] (e : C ≌ C) (a : ℤ) :

C ≌ C

Powers of an auto-equivalence.

Equations

e.pow -[1+ n + 1] = e.symm.trans (e.pow -[1+ n])
e.pow -[1+ 0] = e.symm
e.pow (int.of_nat (n + 2)) = e.trans (e.pow (int.of_nat (n + 1)))
e.pow (int.of_nat 1) = e
e.pow (int.of_nat 0) = category_theory.equivalence.refl

source

@[instance]

def category_theory.equivalence.has_pow {C : Type u₁} [category_theory.category C] :

has_pow (C ≌ C) ℤ

Equations

category_theory.equivalence.has_pow = {pow := category_theory.equivalence.pow _inst_1}

source

@[simp]

theorem category_theory.equivalence.pow_zero {C : Type u₁} [category_theory.category C] (e : C ≌ C) :

e ^ 0 = category_theory.equivalence.refl

source

@[simp]

theorem category_theory.equivalence.pow_one {C : Type u₁} [category_theory.category C] (e : C ≌ C) :

e ^ 1 = e

source

@[simp]

theorem category_theory.equivalence.pow_minus_one {C : Type u₁} [category_theory.category C] (e : C ≌ C) :

e ^ -1 = e.symm

source

@[class]

structure category_theory.is_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

Type (max u₁ u₂ v₁ v₂)

inverse : D ⥤ C
unit_iso : 𝟭 C ≅ F ⋙ category_theory.is_equivalence.inverse F
counit_iso : category_theory.is_equivalence.inverse F ⋙ F ≅ 𝟭 D
functor_unit_iso_comp' : (∀ (X : C), F.map (category_theory.is_equivalence.unit_iso.hom.app X) ≫ category_theory.is_equivalence.counit_iso.hom.app (F.obj X) = 𝟙 (F.obj X)) . "obviously"

A functor that is part of a (half) adjoint equivalence

Instances

source

@[instance]

def category_theory.is_equivalence.of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ≌ D) :

category_theory.is_equivalence F.functor

Equations

category_theory.is_equivalence.of_equivalence F = {inverse := F.inverse, unit_iso := F.unit_iso, counit_iso := F.counit_iso, functor_unit_iso_comp' := _}

source

@[instance]

def category_theory.is_equivalence.of_equivalence_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ≌ D) :

category_theory.is_equivalence F.inverse

Equations

category_theory.is_equivalence.of_equivalence_inverse F = category_theory.is_equivalence.of_equivalence F.symm

source

def category_theory.is_equivalence.mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) :

category_theory.is_equivalence F

Equations

category_theory.is_equivalence.mk G η ε = {inverse := G, unit_iso := category_theory.equivalence.adjointify_η η ε, counit_iso := ε, functor_unit_iso_comp' := _}

source

def category_theory.functor.as_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

C ≌ D

Equations

F.as_equivalence = {functor := F, inverse := category_theory.is_equivalence.inverse F _inst_3, unit_iso := category_theory.is_equivalence.unit_iso _inst_3, counit_iso := category_theory.is_equivalence.counit_iso _inst_3, functor_unit_iso_comp' := _}

source

@[instance]

def category_theory.functor.is_equivalence_refl {C : Type u₁} [category_theory.category C] :

category_theory.is_equivalence (𝟭 C)

Equations

category_theory.functor.is_equivalence_refl = category_theory.is_equivalence.of_equivalence category_theory.equivalence.refl

source

def category_theory.functor.inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

D ⥤ C

Equations

F.inv = category_theory.is_equivalence.inverse F

source

@[instance]

def category_theory.functor.is_equivalence_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.is_equivalence F.inv

Equations

F.is_equivalence_inv = category_theory.is_equivalence.of_equivalence F.as_equivalence.symm

source

@[simp]

theorem category_theory.functor.as_equivalence_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F.as_equivalence.functor = F

source

@[simp]

theorem category_theory.functor.as_equivalence_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F.as_equivalence.inverse = F.inv

source

@[simp]

theorem category_theory.functor.inv_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F.inv.inv = F

source

def category_theory.functor.fun_inv_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F ⋙ F.inv ≅ 𝟭 C

Equations

F.fun_inv_id = category_theory.is_equivalence.unit_iso.symm

source

def category_theory.functor.inv_fun_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

F.inv ⋙ F ≅ 𝟭 D

Equations

F.inv_fun_id = category_theory.is_equivalence.counit_iso

source

@[instance]

def category_theory.functor.is_equivalence_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.is_equivalence F] [category_theory.is_equivalence G] :

category_theory.is_equivalence (F ⋙ G)

Equations

F.is_equivalence_trans G = category_theory.is_equivalence.of_equivalence (F.as_equivalence.trans G.as_equivalence)

source

@[simp]

theorem category_theory.equivalence.functor_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.functor.inv = E.inverse

source

@[simp]

theorem category_theory.equivalence.inverse_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.inverse.inv = E.functor

source

@[simp]

theorem category_theory.equivalence.functor_as_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.functor.as_equivalence = E

source

@[simp]

theorem category_theory.equivalence.inverse_as_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ≌ D) :

E.inverse.as_equivalence = E.symm

source

@[simp]

theorem category_theory.is_equivalence.fun_inv_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] (X Y : D) (f : X ⟶ Y) :

F.map (F.inv.map f) = F.inv_fun_id.hom.app X ≫ f ≫ F.inv_fun_id.inv.app Y

source

@[simp]

theorem category_theory.is_equivalence.inv_fun_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] (X Y : C) (f : X ⟶ Y) :

F.inv.map (F.map f) = F.fun_inv_id.hom.app X ≫ f ≫ F.fun_inv_id.inv.app Y

source

@[simp]

theorem category_theory.is_equivalence.functor_unit_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ⥤ D) [category_theory.is_equivalence E] (Y : C) :

E.map (E.fun_inv_id.inv.app Y) ≫ E.inv_fun_id.hom.app (E.obj Y) = 𝟙 (E.obj ((𝟭 C).obj Y))

source

@[simp]

theorem category_theory.is_equivalence.inv_fun_id_inv_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (E : C ⥤ D) [category_theory.is_equivalence E] (Y : C) :

E.inv_fun_id.inv.app (E.obj Y) ≫ E.map (E.fun_inv_id.hom.app Y) = 𝟙 ((𝟭 D).obj (E.obj Y))

source

@[class]

structure category_theory.ess_surj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

Type (max u₁ u₂ v₂)

obj_preimage : D → C
iso' : Π (d : D), (F.obj (category_theory.ess_surj.obj_preimage F d) ≅ d) . "obviously"

A functor F : C ⥤ D is essentially surjective if for every d : D, there is some c : C so F.obj c ≅ D.

See https://stacks.math.columbia.edu/tag/001C.

Instances

source

def category_theory.functor.obj_preimage {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.ess_surj F] (d : D) :

C

Equations

F.obj_preimage d = category_theory.ess_surj.obj_preimage F d

source

def category_theory.functor.fun_obj_preimage_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.ess_surj F] (d : D) :

F.obj (F.obj_preimage d) ≅ d

Equations

F.fun_obj_preimage_iso d = category_theory.ess_surj.iso d

source

def category_theory.equivalence.ess_surj_of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.ess_surj F

An equivalence is essentially surjective.

See https://stacks.math.columbia.edu/tag/02C3.

Equations

category_theory.equivalence.ess_surj_of_equivalence F = {obj_preimage := λ (Y : D), F.inv.obj Y, iso' := λ (Y : D), F.inv_fun_id.app Y}

source

@[instance]

def category_theory.equivalence.faithful_of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.faithful F

An equivalence is faithful.

See https://stacks.math.columbia.edu/tag/02C3.

source

@[instance]

def category_theory.equivalence.full_of_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] :

category_theory.full F

An equivalence is full.

See https://stacks.math.columbia.edu/tag/02C3.

Equations

category_theory.equivalence.full_of_equivalence F = {preimage := λ (X Y : C) (f : F.obj X ⟶ F.obj Y), F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y, witness' := _}

source

def category_theory.equivalence.equivalence_of_fully_faithfully_ess_surj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.full F] [category_theory.faithful F] [category_theory.ess_surj F] :

category_theory.is_equivalence F

A functor which is full, faithful, and essentially surjective is an equivalence.

See https://stacks.math.columbia.edu/tag/02C3.

Equations

category_theory.equivalence.equivalence_of_fully_faithfully_ess_surj F = category_theory.is_equivalence.mk (equivalence_inverse F) (category_theory.nat_iso.of_components (λ (X : C), (category_theory.preimage_iso (F.fun_obj_preimage_iso (F.obj X))).symm) _) (category_theory.nat_iso.of_components (λ (Y : D), F.fun_obj_preimage_iso Y) _)

source

@[simp]

theorem category_theory.equivalence.functor_map_inj_iff {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) :

e.functor.map f = e.functor.map g ↔ f = g

source

@[simp]

theorem category_theory.equivalence.inverse_map_inj_iff {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) :

e.inverse.map f = e.inverse.map g ↔ f = g