Loogle!

Result

Found 4018 declarations mentioning CategoryTheory.Functor.id. Of these, only the first 200 are shown.

CategoryTheory.Functor.id 📋 Mathlib.CategoryTheory.Functor.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor C C
CategoryTheory.Functor.id_obj 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.id C).obj X = X
CategoryTheory.Functor.comp_id 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : F.comp (CategoryTheory.Functor.id D) = F
CategoryTheory.Functor.id_comp 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.id C).comp F = F
CategoryTheory.Functor.id_map 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Functor.id C).map f = f
CategoryTheory.Functor.leftUnitor 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.id C).comp F ≅ F
CategoryTheory.Functor.rightUnitor 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : F.comp (CategoryTheory.Functor.id D) ≅ F
CategoryTheory.Functor.leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.leftUnitor_inv_app 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.rightUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.rightUnitor_inv_app 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.rightUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.NatTrans.id_comm 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (α β : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.id C) : CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.comp β α
CategoryTheory.Functor.Faithful.id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).Faithful
CategoryTheory.Functor.Full.id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).Full
CategoryTheory.Functor.FullyFaithful.id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).FullyFaithful
CategoryTheory.Functor.FullyFaithful.id_preimage 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : (CategoryTheory.Functor.id C).obj X✝ ⟶ (CategoryTheory.Functor.id C).obj Y✝) : (CategoryTheory.Functor.FullyFaithful.id C).preimage f = f
CategoryTheory.Functor.whiskeringLeft_obj_id 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor C E)
CategoryTheory.Functor.whiskeringRight_obj_id 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor E C)
CategoryTheory.Functor.whiskeringLeftObjIdIso 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor C E)
CategoryTheory.Functor.whiskeringRightObjIdIso 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor E C)
CategoryTheory.Functor.triangleIso 📋 Mathlib.CategoryTheory.Whiskering
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) : F.associator (CategoryTheory.Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor = CategoryTheory.Functor.isoWhiskerRight F.rightUnitor G
CategoryTheory.Functor.triangleIso_assoc 📋 Mathlib.CategoryTheory.Whiskering
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) {Z : CategoryTheory.Functor A C} (h : F.comp G ≅ Z) : F.associator (CategoryTheory.Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor ≪≫ h = CategoryTheory.Functor.isoWhiskerRight F.rightUnitor G ≪≫ h
CategoryTheory.Functor.triangle 📋 Mathlib.CategoryTheory.Whiskering
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) : CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom (F.whiskerLeft G.leftUnitor.hom) = CategoryTheory.Functor.whiskerRight F.rightUnitor.hom G
CategoryTheory.Functor.whiskeringLeftObjIdIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor C E) (X✝ : C) : (CategoryTheory.Functor.whiskeringLeftObjIdIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Functor.whiskeringLeftObjIdIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor C E) (X✝ : C) : (CategoryTheory.Functor.whiskeringLeftObjIdIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Functor.whiskeringRightObjIdIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor E C) (X✝ : E) : (CategoryTheory.Functor.whiskeringRightObjIdIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Functor.whiskeringRightObjIdIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor E C) (X✝ : E) : (CategoryTheory.Functor.whiskeringRightObjIdIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Functor.instEssSurjId 📋 Mathlib.CategoryTheory.EssentialImage
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).EssSurj
CategoryTheory.Functor.isEquivalence_refl 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).IsEquivalence
CategoryTheory.Equivalence.refl_functor 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.functor = CategoryTheory.Functor.id C
CategoryTheory.Equivalence.refl_inverse 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.inverse = CategoryTheory.Functor.id C
CategoryTheory.Equivalence.refl_unitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C)
CategoryTheory.Equivalence.counitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) : self.inverse.comp self.functor ≅ CategoryTheory.Functor.id D
CategoryTheory.Equivalence.unitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) : CategoryTheory.Functor.id C ≅ self.functor.comp self.inverse
CategoryTheory.Equivalence.counit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.inverse.comp e.functor ⟶ CategoryTheory.Functor.id D
CategoryTheory.Equivalence.counitInv 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.id D ⟶ e.inverse.comp e.functor
CategoryTheory.Equivalence.unit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.id C ⟶ e.functor.comp e.inverse
CategoryTheory.Equivalence.unitInv 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.functor.comp e.inverse ⟶ CategoryTheory.Functor.id C
CategoryTheory.Equivalence.mk 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) : C ≌ D
CategoryTheory.Functor.IsEquivalence.mk' 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (G : CategoryTheory.Functor D C) (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) : F.IsEquivalence
CategoryTheory.Equivalence.refl_counitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).comp (CategoryTheory.Functor.id C))
CategoryTheory.Equivalence.symm_counit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.counit = e.unitInv
CategoryTheory.Equivalence.symm_unit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.unit = e.counitInv
CategoryTheory.Equivalence.adjointifyη 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) : CategoryTheory.Functor.id C ≅ F.comp G
CategoryTheory.Equivalence.symm_counitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.counitIso = e.unitIso.symm
CategoryTheory.Equivalence.symm_unitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.unitIso = e.counitIso.symm
CategoryTheory.Equivalence.counitIso_inv_hom_id_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.counit.app Y) = CategoryTheory.CategoryStruct.id Y
CategoryTheory.Equivalence.unitIso_hom_inv_id_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.unitInv.app X) = CategoryTheory.CategoryStruct.id X
CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.FullSubcategory)
CategoryTheory.Functor.asEquivalence_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : D) : F.asEquivalence.counitIso.hom.app X = (F.objObjPreimageIso X).hom
CategoryTheory.Functor.asEquivalence_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : D) : F.asEquivalence.counitIso.inv.app X = (F.objObjPreimageIso X).inv
CategoryTheory.Equivalence.counitIso_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) = h
CategoryTheory.Equivalence.unitIso_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (CategoryTheory.CategoryStruct.comp (e.unitInv.app X) h) = h
CategoryTheory.Equivalence.counitInv_app_functor 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)
CategoryTheory.Equivalence.counit_app_functor 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
CategoryTheory.Equivalence.unitInv_app_inverse 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)
CategoryTheory.Equivalence.unit_app_inverse 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
CategoryTheory.Equivalence.counitIso_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counit.app Y) (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h) = h
CategoryTheory.Equivalence.unitIso_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : C} (h : e.inverse.obj (e.functor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp (e.unit.app X) h) = h
CategoryTheory.Functor.asEquivalence_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) : F.asEquivalence.unitIso.hom.app X = F.preimage (F.objObjPreimageIso (F.obj X)).inv
CategoryTheory.Functor.asEquivalence_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) : F.asEquivalence.unitIso.inv.app X = F.preimage (F.objObjPreimageIso (F.obj X)).hom
CategoryTheory.Equivalence.cancel_counitInv_right 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counitInv.app Y) ↔ f = f'
CategoryTheory.Equivalence.cancel_counit_left 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.counit.app Y) f = CategoryTheory.CategoryStruct.comp (e.counit.app Y) f' ↔ f = f'
CategoryTheory.Equivalence.cancel_unitInv_left 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f' ↔ f = f'
CategoryTheory.Equivalence.cancel_unit_right 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (e.unit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unit.app Y) ↔ f = f'
CategoryTheory.Equivalence.counitIso_hom_inv_id_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.counit.app Y) (e.counitInv.app Y) = CategoryTheory.CategoryStruct.id (e.functor.obj (e.inverse.obj Y))
CategoryTheory.Equivalence.unitIso_inv_hom_id_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (e.unit.app X) = CategoryTheory.CategoryStruct.id (e.inverse.obj (e.functor.obj X))
CategoryTheory.Equivalence.ext 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {x y : C ≌ D} (functor : x.functor = y.functor) (inverse : x.inverse = y.inverse) (unitIso : x.unitIso ≍ y.unitIso) (counitIso : x.counitIso ≍ y.counitIso) : x = y
CategoryTheory.Equivalence.ext_iff 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {x y : C ≌ D} : x = y ↔ x.functor = y.functor ∧ x.inverse = y.inverse ∧ x.unitIso ≍ y.unitIso ∧ x.counitIso ≍ y.counitIso
CategoryTheory.Equivalence.funInvIdAssoc_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
CategoryTheory.Equivalence.funInvIdAssoc_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)
CategoryTheory.Equivalence.invFunIdAssoc_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
CategoryTheory.Equivalence.invFunIdAssoc_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)
CategoryTheory.Equivalence.counitInv_functor_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
CategoryTheory.Equivalence.functor_unit_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
CategoryTheory.Equivalence.inverse_counitInv_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
CategoryTheory.Equivalence.unit_inverse_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
CategoryTheory.Equivalence.mk'' 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (counitIso.inv.app (functor.obj X)) (functor.map (unitIso.inv.app X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : C ≌ D
CategoryTheory.Equivalence.mk' 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X) := by cat_disch) : C ≌ D
CategoryTheory.Equivalence.counitInv_naturality 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.functor.map (e.inverse.map f)) = CategoryTheory.CategoryStruct.comp f (e.counitInv.app X)
CategoryTheory.Equivalence.counit_naturality 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (e.counit.app Y) = CategoryTheory.CategoryStruct.comp (e.counit.app X) f
CategoryTheory.Equivalence.unitInv_naturality 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (e.unitInv.app X) = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f
CategoryTheory.Equivalence.unit_naturality 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.inverse.map (e.functor.map f)) = CategoryTheory.CategoryStruct.comp f (e.unit.app Y)
CategoryTheory.Equivalence.cancel_counitInv_left 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : e.functor.obj (e.inverse.obj Y) ⟶ X) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) f = CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) f' ↔ f = f'
CategoryTheory.Equivalence.cancel_counit_right 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : CategoryTheory.CategoryStruct.comp f (e.counit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counit.app Y) ↔ f = f'
CategoryTheory.Equivalence.cancel_unitInv_right 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : CategoryTheory.CategoryStruct.comp f (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unitInv.app Y) ↔ f = f'
CategoryTheory.Equivalence.cancel_unit_left 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : e.inverse.obj (e.functor.obj Y) ⟶ X) : CategoryTheory.CategoryStruct.comp (e.unit.app Y) f = CategoryTheory.CategoryStruct.comp (e.unit.app Y) f' ↔ f = f'
CategoryTheory.Equivalence.counitInv_functor_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) = h
CategoryTheory.Equivalence.functor_unit_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) = h
CategoryTheory.Equivalence.inverse_counitInv_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) = h
CategoryTheory.Equivalence.unit_inverse_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) = h
CategoryTheory.Equivalence.adjointify_η_ε_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (CategoryTheory.CategoryStruct.comp (ε.hom.app (F.obj X)) h) = h
CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)
CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
CategoryTheory.Equivalence.changeInverse_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))
CategoryTheory.Equivalence.changeInverse_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)
CategoryTheory.Equivalence.adjointify_η_ε 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Equivalence.fun_inv_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : e.functor.map (e.inverse.map f) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
CategoryTheory.Equivalence.inv_fun_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) : e.inverse.map (e.functor.map f) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))
CategoryTheory.Equivalence.counitInv_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : Y ⟶ X) {Z : D} (h : e.functor.obj (e.inverse.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app X) h)
CategoryTheory.Equivalence.counitIso_functor_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app (e.functor.obj X)) (e.functor.map (e.unitIso.inv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
CategoryTheory.Equivalence.counit_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : X ⟶ Y) {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.Equivalence.functor_unitIso_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)
CategoryTheory.Equivalence.unitInv_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : Y ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app X) h) = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.Equivalence.unit_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h)
CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
CategoryTheory.Equivalence.changeInverse_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
CategoryTheory.Equivalence.changeInverse_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
CategoryTheory.Equivalence.cancel_counitInv_right_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.counitInv.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.counitInv.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
CategoryTheory.Equivalence.cancel_unit_right_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.unit.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.unit.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
CategoryTheory.Equivalence.fun_inv_map_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h))
CategoryTheory.Equivalence.inv_fun_map_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h))
CategoryTheory.Equivalence.Equivalence_mk'_counit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counit = counit_iso.hom
CategoryTheory.Equivalence.Equivalence_mk'_counitInv 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv
CategoryTheory.Equivalence.Equivalence_mk'_unit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unit = unit_iso.hom
CategoryTheory.Equivalence.Equivalence_mk'_unitInv 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unitInv = unit_iso.inv
CategoryTheory.Functor.inv_fun_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X Y : C) (f : X ⟶ Y) : F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))
CategoryTheory.Iso.inverseCompIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
CategoryTheory.Iso.inverseCompIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))
CategoryTheory.Iso.isoInverseComp_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))
CategoryTheory.Iso.isoInverseComp_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
CategoryTheory.Iso.compInverseIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))
CategoryTheory.Iso.compInverseIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
CategoryTheory.Iso.isoCompInverse_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))
CategoryTheory.Iso.isoCompInverse_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj X))
CategoryTheory.Functor.fun_inv_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X Y : D) (f : X ⟶ Y) : F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))
CategoryTheory.Equivalence.cancel_counitInv_right_assoc' 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.counitInv.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.counitInv.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
CategoryTheory.Equivalence.cancel_unit_right_assoc' 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.unit.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.unit.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.comp (G'.unitIso.hom.app (G.inverse.obj X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.inv.app (G.inverse.obj X))) (G'.inverse.map (G.counitIso.hom.app X)))
CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.comp (G'.inverse.map (G.counitIso.inv.app X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.hom.app (G.inverse.obj X))) (G'.unitIso.inv.app (G.inverse.obj X)))
CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.hom.app X = CategoryTheory.CategoryStruct.comp (G'.counitIso.inv.app (G.functor.obj X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.inv.app (G.functor.obj X))) (G'.functor.map (G.unitIso.inv.app X)))
CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.inv.app X = CategoryTheory.CategoryStruct.comp (G'.functor.map (G.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.hom.app (G.functor.obj X))) (G'.counitIso.hom.app (G.functor.obj X)))
CategoryTheory.Equivalence.trans_counitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).counitIso = ((f.inverse.comp e.inverse).associator e.functor f.functor).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (f.inverse.associator e.inverse e.functor ≪≫ f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor) f.functor ≪≫ f.counitIso
CategoryTheory.Equivalence.trans_unitIso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).unitIso = e.unitIso ≪≫ CategoryTheory.Functor.isoWhiskerRight (e.functor.rightUnitor.symm ≪≫ e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm) e.inverse ≪≫ (e.functor.comp f.functor).associator f.inverse e.inverse
CategoryTheory.Equivalence.congrLeft_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor D E) : e.congrLeft.counitIso.hom.app X = (e.invFunIdAssoc X).hom
CategoryTheory.Equivalence.congrLeft_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor D E) : e.congrLeft.counitIso.inv.app X = (e.invFunIdAssoc X).inv
CategoryTheory.Equivalence.congrLeft_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor C E) : e.congrLeft.unitIso.hom.app X = (e.funInvIdAssoc X).inv
CategoryTheory.Equivalence.congrLeft_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor C E) : e.congrLeft.unitIso.inv.app X = (e.funInvIdAssoc X).hom
CategoryTheory.Equivalence.congrRight_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E D) : e.congrRight.counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (X.associator e.inverse e.functor).hom (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.hom) X.rightUnitor.hom)
CategoryTheory.Equivalence.congrRight_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E C) : e.congrRight.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (X.associator e.functor e.inverse).inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.inv) X.rightUnitor.hom)
CategoryTheory.Equivalence.congrRight_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E D) : e.congrRight.counitIso.inv.app X = CategoryTheory.CategoryStruct.comp X.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.inv) (X.associator e.inverse e.functor).inv)
CategoryTheory.Equivalence.congrRight_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E C) : e.congrRight.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp X.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.hom) (X.associator e.functor e.inverse).hom)
CategoryTheory.Functor.unopId 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id Cᵒᵖ).unop ≅ CategoryTheory.Functor.id C
CategoryTheory.Functor.opId 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).op ≅ CategoryTheory.Functor.id Cᵒᵖ
CategoryTheory.Functor.leftOpId 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id Cᵒᵖ).leftOp ≅ CategoryTheory.unopUnop C
CategoryTheory.Functor.rightOpId 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id Cᵒᵖ).rightOp ≅ CategoryTheory.opOp C
CategoryTheory.Functor.unopId_hom_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.unopId C).hom.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Functor.unopId_inv_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.unopId C).inv.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.opOpEquivalence_unitIso 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.opOpEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖᵒᵖ)
CategoryTheory.Functor.opId_hom_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) : (CategoryTheory.Functor.opId C).hom.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Functor.opId_inv_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) : (CategoryTheory.Functor.opId C).inv.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Functor.leftOpId_hom_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.Functor.leftOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
CategoryTheory.Functor.leftOpId_inv_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.Functor.leftOpId C).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
CategoryTheory.Equivalence.op_counitIso 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.op.counitIso = (CategoryTheory.NatIso.op e.counitIso).symm
CategoryTheory.Equivalence.op_unitIso 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.op.unitIso = (CategoryTheory.NatIso.op e.unitIso).symm
CategoryTheory.Functor.rightOpId_hom_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.rightOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
CategoryTheory.Functor.rightOpId_inv_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.rightOpId C).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
CategoryTheory.Equivalence.unop_counitIso 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm
CategoryTheory.Equivalence.unop_unitIso 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm
CategoryTheory.Functor.opUnopEquiv_unitIso 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.Functor.opUnopEquiv C D).unitIso = CategoryTheory.NatIso.ofComponents (fun F => (Opposite.unop F).opUnopIso.op) ⋯
CategoryTheory.Functor.opUnopEquiv_counitIso 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.Functor.opUnopEquiv C D).counitIso = CategoryTheory.NatIso.ofComponents (fun F => F.unopOpIso) ⋯
CategoryTheory.NatIso.unop_leftUnitor 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} : CategoryTheory.NatIso.unop F.leftUnitor = F.unop.leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.unopId C).symm F.unop ≪≫ ((CategoryTheory.Functor.id Cᵒᵖ).unopComp F).symm
CategoryTheory.NatIso.unop_rightUnitor 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} : CategoryTheory.NatIso.unop F.rightUnitor = F.unop.rightUnitor.symm ≪≫ F.unop.isoWhiskerLeft (CategoryTheory.Functor.unopId D).symm ≪≫ (F.unopComp (CategoryTheory.Functor.id Dᵒᵖ)).symm
CategoryTheory.NatIso.op_leftUnitor 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : CategoryTheory.NatIso.op F.leftUnitor = F.op.leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.opId C).symm F.op ≪≫ ((CategoryTheory.Functor.id C).opComp F).symm
CategoryTheory.NatIso.op_rightUnitor 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : CategoryTheory.NatIso.op F.rightUnitor = F.op.rightUnitor.symm ≪≫ F.op.isoWhiskerLeft (CategoryTheory.Functor.opId D).symm ≪≫ (F.opComp (CategoryTheory.Functor.id D)).symm
CategoryTheory.Equivalence.leftOp_counitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.op X)).unop
CategoryTheory.Equivalence.leftOp_counitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.op X)).unop
CategoryTheory.Equivalence.leftOp_unitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.unop X)).op
CategoryTheory.Equivalence.leftOp_unitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.unop X)).op
CategoryTheory.Equivalence.rightOp_unitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.op X)).unop
CategoryTheory.Equivalence.rightOp_unitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.op X)).unop
CategoryTheory.Equivalence.rightOp_counitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.unop X)).op
CategoryTheory.Equivalence.rightOp_counitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.unop X)).op
CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op
CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.inv.app X = (Opposite.unop X).rightOpLeftOpIso.inv.op
CategoryTheory.Equivalence.induced_counitIso 📋 Mathlib.CategoryTheory.EqToHom
{D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) : (CategoryTheory.Equivalence.induced e).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
CategoryTheory.Equivalence.induced_unitIso 📋 Mathlib.CategoryTheory.EqToHom
{D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) : (CategoryTheory.Equivalence.induced e).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
CategoryTheory.Functor.constCompEvaluationObj 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) : (CategoryTheory.Functor.const C).comp ((CategoryTheory.evaluation C D).obj X) ≅ CategoryTheory.Functor.id D
CategoryTheory.Prod.symmetry 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.Prod.swap C D).comp (CategoryTheory.Prod.swap D C) ≅ CategoryTheory.Functor.id (C × D)
CategoryTheory.Functor.diag_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Functor.diag C).map f = CategoryTheory.Prod.mkHom f f
CategoryTheory.Prod.braiding_unitIso 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.Prod.braiding C D).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × D))
CategoryTheory.Prod.symmetry_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.symmetry C D).hom.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Prod.symmetry_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.symmetry C D).inv.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Equivalence.prod_counitIso 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).counitIso = CategoryTheory.NatIso.prod E₁.counitIso E₂.counitIso
CategoryTheory.Equivalence.prod_unitIso 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso
CategoryTheory.functorProdFunctorEquivCounitIso 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : (CategoryTheory.functorProdToProdFunctor A B C).comp (CategoryTheory.prodFunctorToFunctorProd A B C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor A (B × C))
CategoryTheory.Functor.constCompEvaluationObj_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) (X✝ : D) : (CategoryTheory.Functor.constCompEvaluationObj D X).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝
CategoryTheory.Functor.constCompEvaluationObj_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) (X✝ : D) : (CategoryTheory.Functor.constCompEvaluationObj D X).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝
CategoryTheory.functorProdFunctorEquivUnitIso 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : CategoryTheory.Functor.id (CategoryTheory.Functor A B × CategoryTheory.Functor A C) ≅ (CategoryTheory.prodFunctorToFunctorProd A B C).comp (CategoryTheory.functorProdToProdFunctor A B C)
CategoryTheory.functorProdFunctorEquiv_counitIso 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : (CategoryTheory.functorProdFunctorEquiv A B C).counitIso = CategoryTheory.functorProdFunctorEquivCounitIso A B C
CategoryTheory.prodOpEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (CategoryTheory.prodOpEquiv C).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.prodOpEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (CategoryTheory.prodOpEquiv C).unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.functorProdFunctorEquiv_unitIso 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : (CategoryTheory.functorProdFunctorEquiv A B C).unitIso = CategoryTheory.functorProdFunctorEquivUnitIso A B C
CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).hom.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X✝).1) (CategoryTheory.CategoryStruct.id (X.obj X✝).2)
CategoryTheory.functorProdFunctorEquivCounitIso_inv_app_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).inv.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X✝).1) (CategoryTheory.CategoryStruct.id (X.obj X✝).2)
CategoryTheory.functorProdFunctorEquivUnitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A B × CategoryTheory.Functor A C) : (CategoryTheory.functorProdFunctorEquivUnitIso A B C).hom.app X = CategoryTheory.Prod.mkHom (X.1.prod'CompFst X.2).inv (X.1.prod'CompSnd X.2).inv
CategoryTheory.functorProdFunctorEquivUnitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A B × CategoryTheory.Functor A C) : (CategoryTheory.functorProdFunctorEquivUnitIso A B C).inv.app X = CategoryTheory.Prod.mkHom (X.1.prod'CompFst X.2).hom (X.1.prod'CompSnd X.2).hom

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59