Loogle!
Result
Found 309 declarations mentioning CategoryTheory.Functor.IsEquivalence. Of these, only the first 200 are shown.
- CategoryTheory.Functor.isEquivalence_refl 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.Functor.id C).IsEquivalence - CategoryTheory.Functor.IsEquivalence 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop - CategoryTheory.Equivalence.isEquivalence_functor 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ≌ D) : F.functor.IsEquivalence - CategoryTheory.Equivalence.isEquivalence_inverse 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ≌ D) : F.inverse.IsEquivalence - CategoryTheory.Functor.asEquivalence 📋 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] : C ≌ D - CategoryTheory.Functor.inv 📋 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] : CategoryTheory.Functor D C - CategoryTheory.Functor.IsEquivalence.essSurj 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.IsEquivalence] : F.EssSurj - CategoryTheory.Functor.IsEquivalence.faithful 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.IsEquivalence] : F.Faithful - CategoryTheory.Functor.IsEquivalence.full 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.IsEquivalence] : F.Full - CategoryTheory.Functor.isEquivalence_inv 📋 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] : F.inv.IsEquivalence - CategoryTheory.Functor.asEquivalence_functor 📋 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] : F.asEquivalence.functor = F - CategoryTheory.Functor.isEquivalence_of_iso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence - 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} (faithful : F.Faithful := by infer_instance) (full : F.Full := by infer_instance) (essSurj : F.EssSurj := by infer_instance) : F.IsEquivalence - CategoryTheory.Functor.asEquivalence_inverse 📋 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] : F.asEquivalence.inverse = F.inv - CategoryTheory.Functor.isEquivalence_iff_of_iso 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : F.IsEquivalence ↔ G.IsEquivalence - CategoryTheory.Functor.isEquivalence_of_comp_left 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).IsEquivalence] : G.IsEquivalence - CategoryTheory.Functor.isEquivalence_of_comp_right 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] [(F.comp G).IsEquivalence] : F.IsEquivalence - CategoryTheory.Functor.isEquivalence_trans 📋 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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.IsEquivalence] : (F.comp G).IsEquivalence - CategoryTheory.Equivalence.fullyFaithfulToEssImage 📋 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.Full] [F.Faithful] : F.toEssImage.IsEquivalence - 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.inducedFunctorOfEquiv 📋 Mathlib.CategoryTheory.Equivalence
{D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) : (CategoryTheory.inducedFunctor ⇑e).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft 📋 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 D) [F.IsEquivalence] : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight 📋 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 D) [F.IsEquivalence] : ((CategoryTheory.Functor.whiskeringRight E C D).obj F).IsEquivalence - 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.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.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.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.instIsEquivalenceOppositeOpOp 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.opOp C).IsEquivalence - CategoryTheory.instIsEquivalenceOppositeUnopUnop 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.unopUnop C).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceOppositeOp 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.IsEquivalence] : F.op.IsEquivalence - CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} [F.IsEquivalence] : F.leftOp.IsEquivalence - CategoryTheory.Functor.instIsEquivalenceOppositeRightOp 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} [F.IsEquivalence] : F.rightOp.IsEquivalence - CategoryTheory.Prod.swapIsEquivalence 📋 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).IsEquivalence - CategoryTheory.Equivalence.instIsEquivalenceForallPi 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) [∀ (i : I), (F i).IsEquivalence] : (CategoryTheory.Functor.pi F).IsEquivalence - CategoryTheory.prod.leftUnitor_isEquivalence 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitor C).IsEquivalence - CategoryTheory.prod.rightUnitor_isEquivalence 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitor C).IsEquivalence - CategoryTheory.Comma.isEquivalence_preLeft 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [F.IsEquivalence] : (CategoryTheory.Comma.preLeft F L R).IsEquivalence - CategoryTheory.Comma.isEquivalence_preRight 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (L : CategoryTheory.Functor A T) [F.IsEquivalence] : (CategoryTheory.Comma.preRight L F R).IsEquivalence - CategoryTheory.Comma.isEquivalence_post 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) [F.IsEquivalence] : (CategoryTheory.Comma.post L R F).IsEquivalence - CategoryTheory.Comma.isEquivalenceMap 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.Comma.map α β).IsEquivalence - CategoryTheory.Functor.isEquivalence_mapArrow 📋 Mathlib.CategoryTheory.Comma.Arrow
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : F.mapArrow.IsEquivalence - CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence 📋 Mathlib.CategoryTheory.MorphismProperty.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : (P.map F).inverseImage F = P - CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence 📋 Mathlib.CategoryTheory.MorphismProperty.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (P : CategoryTheory.MorphismProperty D) [P.RespectsIso] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : (P.inverseImage F).map F = P - CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.IsEquivalence] : F.IsLeftAdjoint - CategoryTheory.Functor.isRightAdjoint_of_isEquivalence 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.IsEquivalence] : F.IsRightAdjoint - CategoryTheory.Functor.adjunction 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [E.IsEquivalence] : E ⊣ E.inv - CategoryTheory.Functor.isLeftAdjoint_comp_iff_left 📋 Mathlib.CategoryTheory.Adjunction.Basic
{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 D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] : (F.comp G).IsLeftAdjoint ↔ F.IsLeftAdjoint - CategoryTheory.Functor.isLeftAdjoint_comp_iff_right 📋 Mathlib.CategoryTheory.Adjunction.Basic
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] : (F.comp G).IsLeftAdjoint ↔ G.IsLeftAdjoint - CategoryTheory.Functor.isRightAdjoint_comp_iff_left 📋 Mathlib.CategoryTheory.Adjunction.Basic
{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 D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] : (F.comp G).IsRightAdjoint ↔ F.IsRightAdjoint - CategoryTheory.Functor.isRightAdjoint_comp_iff_right 📋 Mathlib.CategoryTheory.Adjunction.Basic
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] : (F.comp G).IsRightAdjoint ↔ G.IsRightAdjoint - CategoryTheory.Functor.isEquivalence_of_isRightAdjoint 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [G.IsRightAdjoint] [∀ (X : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).unit.app X)] [∀ (Y : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).counit.app Y)] : G.IsEquivalence - CategoryTheory.Functor.mapCoconeInv 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} [H.IsEquivalence] (c : CategoryTheory.Limits.Cocone (F.comp H)) : CategoryTheory.Limits.Cocone F - CategoryTheory.Functor.mapConeInv 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} [H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)) : CategoryTheory.Limits.Cone F - CategoryTheory.Functor.mapCoconeInvMapCocone 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cocone F) : H.mapCoconeInv (H.mapCocone c) ≅ c - CategoryTheory.Functor.mapConeInvMapCone 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cone F) : H.mapConeInv (H.mapCone c) ≅ c - CategoryTheory.Functor.mapCoconeMapCoconeInv 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cocone (F.comp H)) : H.mapCocone (H.mapCoconeInv c) ≅ c - CategoryTheory.Functor.mapConeMapConeInv 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)) : H.mapCone (H.mapConeInv c) ≅ c - CategoryTheory.fromSkeleton.isEquivalence 📋 Mathlib.CategoryTheory.Skeletal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.fromSkeleton C).IsEquivalence - CategoryTheory.IsSkeletonOf.eqv 📋 Mathlib.CategoryTheory.Skeletal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.IsSkeletonOf C D F) : F.IsEquivalence - CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence 📋 Mathlib.CategoryTheory.Skeletal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] : (CategoryTheory.ThinSkeleton.fromThinSkeleton C).IsEquivalence - CategoryTheory.IsSkeletonOf.mk 📋 Mathlib.CategoryTheory.Skeletal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor D C} (skel : CategoryTheory.Skeletal D) (eqv : F.IsEquivalence := by infer_instance) : CategoryTheory.IsSkeletonOf C D F - CategoryTheory.ShrinkHoms.instIsEquivalenceFunctor 📋 Mathlib.CategoryTheory.EssentiallySmall
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : (CategoryTheory.ShrinkHoms.functor C).IsEquivalence - CategoryTheory.ShrinkHoms.instIsEquivalenceInverse 📋 Mathlib.CategoryTheory.EssentiallySmall
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : (CategoryTheory.ShrinkHoms.inverse C).IsEquivalence - CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence 📋 Mathlib.CategoryTheory.Functor.EpiMono
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] [CategoryTheory.SplitEpiCategory C] : CategoryTheory.SplitEpiCategory D - CategoryTheory.Functor.splitMonoCategoryImpOfIsEquivalence 📋 Mathlib.CategoryTheory.Functor.EpiMono
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] [CategoryTheory.SplitMonoCategory C] : CategoryTheory.SplitMonoCategory D - CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence 📋 Mathlib.CategoryTheory.Functor.EpiMono
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A B : C} [F.IsEquivalence] (f : A ⟶ B) [_h : CategoryTheory.StrongEpi f] : CategoryTheory.StrongEpi (F.map f) - CategoryTheory.Adjunction.strongMono_map_of_isEquivalence 📋 Mathlib.CategoryTheory.Functor.EpiMono
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A B : C} [F.IsEquivalence] (f : B ⟶ A) [_h : CategoryTheory.StrongMono f] : CategoryTheory.StrongMono (F.map f) - CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence 📋 Mathlib.CategoryTheory.Functor.EpiMono
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A B : C} (f : A ⟶ B) [F.IsEquivalence] : CategoryTheory.StrongEpi (F.map f) ↔ CategoryTheory.StrongEpi f - CategoryTheory.Functor.strongMono_map_iff_strongMono_of_isEquivalence 📋 Mathlib.CategoryTheory.Functor.EpiMono
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A B : C} (f : B ⟶ A) [F.IsEquivalence] : CategoryTheory.StrongMono (F.map f) ↔ CategoryTheory.StrongMono f - CategoryTheory.CostructuredArrow.isEquivalence_pre 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (S : D) [F.IsEquivalence] : (CategoryTheory.CostructuredArrow.pre F G S).IsEquivalence - CategoryTheory.StructuredArrow.isEquivalence_pre 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [F.IsEquivalence] : (CategoryTheory.StructuredArrow.pre S F G).IsEquivalence - CategoryTheory.CostructuredArrow.isEquivalence_post 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful] : (CategoryTheory.CostructuredArrow.post F G S).IsEquivalence - CategoryTheory.StructuredArrow.isEquivalence_post 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful] : (CategoryTheory.StructuredArrow.post S F G).IsEquivalence - CategoryTheory.CostructuredArrow.isEquivalenceMap₂ 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V) [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.CostructuredArrow.map₂ α β).IsEquivalence - CategoryTheory.StructuredArrow.isEquivalenceMap₂ 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L) (β : R.comp G ⟶ F.comp R') [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.StructuredArrow.map₂ α β).IsEquivalence - CategoryTheory.Over.instIsEquivalenceMapOfIsIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} [CategoryTheory.IsIso f] : (CategoryTheory.Over.map f).IsEquivalence - CategoryTheory.Under.instIsEquivalenceMapOfIsIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} [CategoryTheory.IsIso f] : (CategoryTheory.Under.map f).IsEquivalence - CategoryTheory.CostructuredArrow.isEquivalence_toOver 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) [F.IsEquivalence] : (CategoryTheory.CostructuredArrow.toOver F X).IsEquivalence - CategoryTheory.StructuredArrow.isEquivalence_toUnder 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) [F.IsEquivalence] : (CategoryTheory.StructuredArrow.toUnder X F).IsEquivalence - CategoryTheory.Over.instIsEquivalenceObjPost 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor T D) [F.IsEquivalence] : (CategoryTheory.Over.post F).IsEquivalence - CategoryTheory.Under.instIsEquivalenceObjPost 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor T D) [F.IsEquivalence] : (CategoryTheory.Under.post F).IsEquivalence - CategoryTheory.MorphismProperty.instHasFactorizationInverseImageOfIsEquivalenceOfRespectsIso 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (W₁ W₂ : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor D C) [F.IsEquivalence] [W₁.RespectsIso] [W₂.RespectsIso] [W₁.HasFactorization W₂] : (W₁.inverseImage F).HasFactorization (W₂.inverseImage F) - CategoryTheory.MorphismProperty.MapFactorizationData.ofIsEquivalence 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {W₁ W₂ : CategoryTheory.MorphismProperty C} {F : CategoryTheory.Functor D C} [F.IsEquivalence] [W₁.RespectsIso] [W₂.RespectsIso] {X Y : D} {f : X ⟶ Y} (h : W₁.MapFactorizationData W₂ (F.map f)) : (W₁.inverseImage F).MapFactorizationData (W₂.inverseImage F) f - CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] [h : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] : CategoryTheory.Limits.HasStrongEpiMonoFactorisations D - CategoryTheory.Limits.compNatIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : (CategoryTheory.Limits.parallelPair f 0).comp F ≅ CategoryTheory.Limits.parallelPair (F.map f) 0 - AlgCat.instIsEquivalenceRestrictScalarsToRingHom 📋 Mathlib.Algebra.Category.AlgCat.Basic
{R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) : (AlgCat.restrictScalars e.toRingHom).IsEquivalence - AlgCat.instIsEquivalenceRestrictScalarsToRingHomSymm 📋 Mathlib.Algebra.Category.AlgCat.Basic
{R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) : (AlgCat.restrictScalars e.symm.toRingHom).IsEquivalence - AlgCat.instIsEquivalenceIntRingCatForget₂AlgHomCarrierRingHomCarrier 📋 Mathlib.Algebra.Category.AlgCat.Basic
: (CategoryTheory.forget₂ (AlgCat ℤ) RingCat).IsEquivalence - CategoryTheory.Types.instIsEquivalenceForgetTypeFun 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
: (CategoryTheory.forget (Type u)).IsEquivalence - CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.IsEquivalence] : L.IsEquivalence - CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.IsEquivalence] : R.IsEquivalence - CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.IsEquivalence] : CategoryTheory.IsIso h.counit - CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.IsEquivalence] : CategoryTheory.IsIso h.counit - CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.IsEquivalence] : CategoryTheory.IsIso h.unit - CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.IsEquivalence] : CategoryTheory.IsIso h.unit - ModuleCat.forget₂AddCommGroupIsEquivalence 📋 Mathlib.Algebra.Category.Grp.ZModuleEquivalence
: (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).IsEquivalence - ModuleCat.restrictScalars_isEquivalence_of_ringEquiv 📋 Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
{R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) : (ModuleCat.restrictScalars e.toRingHom).IsEquivalence - CategoryTheory.Adjunction.has_colimits_of_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D] : CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C - CategoryTheory.Adjunction.has_limits_of_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] : CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D - CategoryTheory.Adjunction.isEquivalencePreservesLimits 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [E.IsEquivalence] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E - CategoryTheory.Adjunction.isEquivalence_preservesColimits 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [E.IsEquivalence] : CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} E - CategoryTheory.Functor.createsColimitsOfIsEquivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (H : CategoryTheory.Functor D C) [H.IsEquivalence] : CategoryTheory.CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H - CategoryTheory.Functor.createsLimitsOfIsEquivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (H : CategoryTheory.Functor D C) [H.IsEquivalence] : CategoryTheory.CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H - CategoryTheory.Functor.reflectsColimits_of_isEquivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [E.IsEquivalence] : CategoryTheory.Limits.ReflectsColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E - CategoryTheory.Functor.reflectsLimits_of_isEquivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [E.IsEquivalence] : CategoryTheory.Limits.ReflectsLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E - CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimitsOfShape J D] : CategoryTheory.Limits.HasColimitsOfShape J C - CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J D - CategoryTheory.Adjunction.hasColimit_comp_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimit K] : CategoryTheory.Limits.HasColimit (K.comp E) - CategoryTheory.Adjunction.hasColimit_of_comp_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimit (K.comp E)] : CategoryTheory.Limits.HasColimit K - CategoryTheory.Adjunction.hasLimit_comp_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimit K] : CategoryTheory.Limits.HasLimit (K.comp E) - CategoryTheory.Adjunction.hasLimit_of_comp_equivalence 📋 Mathlib.CategoryTheory.Adjunction.Limits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimit (K.comp E)] : CategoryTheory.Limits.HasLimit K - CategoryTheory.hasInitial_of_equivalence 📋 Mathlib.CategoryTheory.Limits.Shapes.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : CategoryTheory.Functor D C) [e.IsEquivalence] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasInitial D - CategoryTheory.hasTerminal_of_equivalence 📋 Mathlib.CategoryTheory.Limits.Shapes.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : CategoryTheory.Functor D C) [e.IsEquivalence] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasTerminal D - CategoryTheory.ObjectProperty.instIsEquivalenceFullSubcategoryIsoClosureιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} : (CategoryTheory.ObjectProperty.ιOfLE ⋯).IsEquivalence - CategoryTheory.ObjectProperty.isEquivalence_ι 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (h : P = ⊤) : P.ι.IsEquivalence - CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q) : (CategoryTheory.ObjectProperty.ιOfLE h).IsEquivalence ↔ Q ≤ P.isoClosure - CategoryTheory.Functor.final_comp_equivalence 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.Final] [G.IsEquivalence] : (F.comp G).Final - CategoryTheory.Functor.final_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.Final] : (F.comp G).Final - CategoryTheory.Functor.final_of_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).Final] : G.Final - CategoryTheory.Functor.initial_comp_equivalence 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.Initial] [G.IsEquivalence] : (F.comp G).Initial - CategoryTheory.Functor.initial_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.Initial] : (F.comp G).Initial - CategoryTheory.Functor.initial_of_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).Initial] : G.Initial - CategoryTheory.Functor.final_iff_comp_equivalence 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] : F.Final ↔ (F.comp G).Final - CategoryTheory.Functor.final_iff_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] : G.Final ↔ (F.comp G).Final - CategoryTheory.Functor.initial_iff_comp_equivalence 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] : F.Initial ↔ (F.comp G).Initial - CategoryTheory.Functor.initial_iff_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
{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 D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] : G.Initial ↔ (F.comp G).Initial - CategoryTheory.MonoidalClosed.ofEquiv 📋 Mathlib.CategoryTheory.Monoidal.Closed.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] : CategoryTheory.MonoidalClosed C - CategoryTheory.MonoidalClosed.ofEquiv_curry_def 📋 Mathlib.CategoryTheory.Monoidal.Closed.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.MonoidalClosed.curry f = (adj.homEquiv Y (F.obj X ⟹ F.obj Z)) (CategoryTheory.MonoidalClosed.curry ((adj.toEquivalence.symm.toAdjunction.homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y) f))) - CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def 📋 Mathlib.CategoryTheory.Monoidal.Closed.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : Y ⟶ X ⟹ Z) : CategoryTheory.MonoidalClosed.uncurry f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y) ((adj.toEquivalence.symm.toAdjunction.homEquiv ((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm (CategoryTheory.MonoidalClosed.uncurry ((adj.homEquiv Y (F.obj X ⟹ adj.toEquivalence.symm.inverse.obj Z)).symm f))) - CategoryTheory.equivalenceReflectsNormalEpi 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] {X Y : C} {f : X ⟶ Y} (hf : CategoryTheory.NormalEpi (F.map f)) : CategoryTheory.NormalEpi f - CategoryTheory.equivalenceReflectsNormalMono 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] {X Y : C} {f : X ⟶ Y} (hf : CategoryTheory.NormalMono (F.map f)) : CategoryTheory.NormalMono f - FGModuleRepr.instIsEquivalenceFGModuleCatEmbed 📋 Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
(R : Type u) [Ring R] : (FGModuleRepr.embed R).IsEquivalence - instIsEquivalenceFGModuleCatUlift 📋 Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
(R : Type u) [Ring R] : (FGModuleCat.ulift R).IsEquivalence - CategoryTheory.EnoughInjectives.of_equivalence 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (e : CategoryTheory.Functor C D) [e.IsEquivalence] [CategoryTheory.EnoughInjectives D] : CategoryTheory.EnoughInjectives C - CategoryTheory.Subobject.instIsEquivalenceMonoOverRepresentative 📋 Mathlib.CategoryTheory.Subobject.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.Subobject.representative.IsEquivalence - CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁ 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H) : L'.HasLeftKanExtension F ↔ L.HasLeftKanExtension F - CategoryTheory.Functor.hasRightExtension_iff_postcomp₁ 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H) : L'.HasRightKanExtension F ↔ L.HasRightKanExtension F - CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence' 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (L : CategoryTheory.Functor C D) (α : F₀ ⟶ L.comp F₁) [L.IsEquivalence] [CategoryTheory.IsIso α] : F₁.IsLeftKanExtension α - CategoryTheory.Functor.isRightKanExtensionAlongEquivalence' 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (L : CategoryTheory.Functor C D) (α : L.comp F₁ ⟶ F₀) [L.IsEquivalence] [CategoryTheory.IsIso α] : F₁.IsRightKanExtension α - CategoryTheory.Functor.isLeftKanExtension_iff_precomp 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (F' : CategoryTheory.Functor D H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (α : F ⟶ L.comp F') : F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (CategoryTheory.CategoryStruct.comp (G.whiskerLeft α) (G.associator L F').inv) - CategoryTheory.Functor.isLeftKanExtension_postcompose₂_iff 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {H' : Type u_4} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_4, u_4} H'] [CategoryTheory.Category.{v_5, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F ⟶ L.comp F') (G : CategoryTheory.Functor H H') [G.IsEquivalence] : (F'.comp G).IsLeftKanExtension (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G) (L.associator F' G).hom) ↔ F'.IsLeftKanExtension α - CategoryTheory.Functor.isRightKanExtension_iff_precomp 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (F' : CategoryTheory.Functor D H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (α : L.comp F' ⟶ F) : F'.IsRightKanExtension α ↔ F'.IsRightKanExtension (CategoryTheory.CategoryStruct.comp (G.associator L F').hom (G.whiskerLeft α)) - CategoryTheory.Functor.isRightKanExtension_postcompose₂_iff 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {H' : Type u_4} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_4, u_4} H'] [CategoryTheory.Category.{v_5, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (β : L.comp F' ⟶ F) (G : CategoryTheory.Functor H H') [G.IsEquivalence] : (F'.comp G).IsRightKanExtension (CategoryTheory.CategoryStruct.comp (L.associator F' G).inv (CategoryTheory.Functor.whiskerRight β G)) ↔ F'.IsRightKanExtension β - CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPostcompose₂ 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') [G.IsEquivalence] : (CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPostcompose₂ 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') [G.IsEquivalence] : (CategoryTheory.Functor.RightExtension.postcompose₂ L F G).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPrecomp 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] : (CategoryTheory.Functor.LeftExtension.precomp L F G).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPrecomp 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] : (CategoryTheory.Functor.RightExtension.precomp L F G).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (f : L' ⟶ L.comp G) [CategoryTheory.IsIso f] (F : CategoryTheory.Functor C H) : (CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (f : L.comp G ⟶ L') [CategoryTheory.IsIso f] (F : CategoryTheory.Functor C H) : (CategoryTheory.Functor.RightExtension.postcomp₁ G f F).IsEquivalence - CategoryTheory.Functor.isRightKanExtension_iff_postcomp₁ 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') {F : CategoryTheory.Functor C H} {F' : CategoryTheory.Functor D' H} (α : L'.comp F' ⟶ F) : F'.IsRightKanExtension α ↔ (G.comp F').IsRightKanExtension (CategoryTheory.CategoryStruct.comp (L.associator G F').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e.hom F') α)) - CategoryTheory.Functor.isLeftKanExtension_iff_postcomp₁ 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') {F : CategoryTheory.Functor C H} {F' : CategoryTheory.Functor D' H} (α : F ⟶ L'.comp F') : F'.IsLeftKanExtension α ↔ (G.comp F').IsLeftKanExtension (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e.inv F') (L.associator G F').hom)) - CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquiv 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (e : L.LeftExtension F) : CategoryTheory.StructuredArrow.IsUniversal e ≃ CategoryTheory.StructuredArrow.IsUniversal ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj e) - CategoryTheory.Functor.RightExtension.isUniversalPrecompEquiv 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (e : L.RightExtension F) : CategoryTheory.CostructuredArrow.IsUniversal e ≃ CategoryTheory.CostructuredArrow.IsUniversal ((CategoryTheory.Functor.RightExtension.precomp L F G).obj e) - CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H) (ex : L'.LeftExtension F) : CategoryTheory.StructuredArrow.IsUniversal ex ≃ CategoryTheory.StructuredArrow.IsUniversal ((CategoryTheory.Functor.LeftExtension.postcomp₁ G e.inv F).obj ex) - CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H) (ex : L'.RightExtension F) : CategoryTheory.CostructuredArrow.IsUniversal ex ≃ CategoryTheory.CostructuredArrow.IsUniversal ((CategoryTheory.Functor.RightExtension.postcomp₁ G e.hom F).obj ex) - CategoryTheory.Functor.isRightKanExtension_iff_precomp_equivalence 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {F₁' : CategoryTheory.Functor D H} {L₁ : CategoryTheory.Functor C D} {F₁ : CategoryTheory.Functor C H} (α₁ : L₁.comp F₁' ⟶ F₁) {F₂' : CategoryTheory.Functor D' H} {L₂ : CategoryTheory.Functor C' D'} {F₂ : CategoryTheory.Functor C' H} (α₂ : L₂.comp F₂' ⟶ F₂) {G : CategoryTheory.Functor C C'} {G' : CategoryTheory.Functor D D'} [G.IsEquivalence] [G'.IsEquivalence] (iso : G.comp L₂ ≅ L₁.comp G') (e : F₁ ≅ G.comp F₂) (e' : G'.comp F₂' ≅ F₁') (h : α₁ = CategoryTheory.CategoryStruct.comp (L₁.whiskerLeft e'.inv) (CategoryTheory.CategoryStruct.comp (L₁.associator G' F₂').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight iso.inv F₂') (CategoryTheory.CategoryStruct.comp (G.associator L₂ F₂').hom (CategoryTheory.CategoryStruct.comp (G.whiskerLeft α₂) e.inv)))) := by cat_disch) : F₂'.IsRightKanExtension α₂ ↔ F₁'.IsRightKanExtension α₁ - CategoryTheory.Functor.isLeftKanExtension_iff_precomp_equivalence 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] {F₁' : CategoryTheory.Functor D H} {L₁ : CategoryTheory.Functor C D} {F₁ : CategoryTheory.Functor C H} (α₁ : F₁ ⟶ L₁.comp F₁') {F₂' : CategoryTheory.Functor D' H} {L₂ : CategoryTheory.Functor C' D'} {F₂ : CategoryTheory.Functor C' H} (α₂ : F₂ ⟶ L₂.comp F₂') {G : CategoryTheory.Functor C C'} {G' : CategoryTheory.Functor D D'} [G.IsEquivalence] [G'.IsEquivalence] (iso : G.comp L₂ ≅ L₁.comp G') (e : F₁ ≅ G.comp F₂) (e' : G'.comp F₂' ≅ F₁') (h : α₁ = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp (G.whiskerLeft α₂) (CategoryTheory.CategoryStruct.comp (G.associator L₂ F₂').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight iso.hom F₂') (CategoryTheory.CategoryStruct.comp (L₁.associator G' F₂').hom (L₁.whiskerLeft e'.hom))))) := by cat_disch) : F₂'.IsLeftKanExtension α₂ ↔ F₁'.IsLeftKanExtension α₁ - CategoryTheory.abelianOfEquivalence 📋 Mathlib.CategoryTheory.Abelian.Transfer
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : CategoryTheory.Abelian C - CategoryTheory.ComonadicLeftAdjoint.mk 📋 Mathlib.CategoryTheory.Monad.Adjunction
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} (R : CategoryTheory.Functor D C) (adj : L ⊣ R) (eqv : (CategoryTheory.Comonad.comparison adj).IsEquivalence) : CategoryTheory.ComonadicLeftAdjoint L - CategoryTheory.MonadicRightAdjoint.mk 📋 Mathlib.CategoryTheory.Monad.Adjunction
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} (L : CategoryTheory.Functor C D) (adj : L ⊣ R) (eqv : (CategoryTheory.Monad.comparison adj).IsEquivalence) : CategoryTheory.MonadicRightAdjoint R - CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R)).IsEquivalence - CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [CategoryTheory.ComonadicLeftAdjoint L] : (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction L)).IsEquivalence - CategoryTheory.ComonadicLeftAdjoint.eqv 📋 Mathlib.CategoryTheory.Monad.Adjunction
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {L : CategoryTheory.Functor C D} [self : CategoryTheory.ComonadicLeftAdjoint L] : (CategoryTheory.Comonad.comparison CategoryTheory.ComonadicLeftAdjoint.adj).IsEquivalence - CategoryTheory.MonadicRightAdjoint.eqv 📋 Mathlib.CategoryTheory.Monad.Adjunction
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {R : CategoryTheory.Functor D C} [self : CategoryTheory.MonadicRightAdjoint R] : (CategoryTheory.Monad.comparison CategoryTheory.MonadicRightAdjoint.adj).IsEquivalence - CategoryTheory.instIsEquivalenceShiftFunctor 📋 Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i : A) : (CategoryTheory.shiftFunctor C i).IsEquivalence - CategoryTheory.Functor.instIsEquivalenceQuotientHomRelLift 📋 Mathlib.CategoryTheory.Quotient
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.Full] [L.EssSurj] : (CategoryTheory.Quotient.lift L.homRel L ⋯).IsEquivalence - CategoryTheory.Pretriangulated.instIsEquivalenceTriangleInvRotate 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : (CategoryTheory.Pretriangulated.invRotate C).IsEquivalence - CategoryTheory.Pretriangulated.instIsEquivalenceTriangleRotate 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : (CategoryTheory.Pretriangulated.rotate C).IsEquivalence - CategoryTheory.Localization.instIsEquivalenceLocalizationLift 📋 Mathlib.CategoryTheory.Localization.Predicate
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {W : CategoryTheory.MorphismProperty C} [L.IsLocalization W] : (CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence - CategoryTheory.Functor.IsLocalization.isEquivalence 📋 Mathlib.CategoryTheory.Localization.Predicate
{C : Type u_1} {D : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} [self : L.IsLocalization W] : (CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence - CategoryTheory.Functor.IsLocalization.mk 📋 Mathlib.CategoryTheory.Localization.Predicate
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} (inverts : W.IsInvertedBy L) (isEquivalence : (CategoryTheory.Localization.Construction.lift L inverts).IsEquivalence) : L.IsLocalization W - CategoryTheory.Functor.IsLocalization.instCompOfIsEquivalence 📋 Mathlib.CategoryTheory.Localization.Predicate
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor D E) [F.IsEquivalence] [L.IsLocalization W] : (L.comp F).IsLocalization W - CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor 📋 Mathlib.CategoryTheory.Localization.Predicate
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [CategoryTheory.Category.{v_3, u_3} E] [L.IsLocalization W] : (CategoryTheory.Localization.whiskeringLeftFunctor L W E).IsEquivalence - CategoryTheory.Functor.IsLocalization.of_isEquivalence 📋 Mathlib.CategoryTheory.Localization.Predicate
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) (hW : W ≤ CategoryTheory.MorphismProperty.isomorphisms C) [L.IsEquivalence] : L.IsLocalization W - CategoryTheory.Localization.isEquivalence 📋 Mathlib.CategoryTheory.Localization.Equivalence
{C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂) (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G'] (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂) : G'.IsEquivalence - CategoryTheory.LocalizerMorphism.instIsEquivalenceFunctorId 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] (W₁ : CategoryTheory.MorphismProperty C₁) : (CategoryTheory.LocalizerMorphism.id W₁).functor.IsEquivalence - CategoryTheory.LocalizerMorphism.inv 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] : CategoryTheory.LocalizerMorphism W₂ W₁ - CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_isInduced 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] : Φ.IsLocalizedEquivalence - CategoryTheory.LocalizerMorphism.instIsInducedInv 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] : Φ.inv.IsInduced - CategoryTheory.LocalizerMorphism.instIsEquivalenceFunctorInv 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] : Φ.inv.functor.IsEquivalence - CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence] : (Φ.localizedFunctor L₁ L₂).IsEquivalence - CategoryTheory.LocalizerMorphism.inv_functor 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso] : Φ.inv.functor = Φ.functor.inv - CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C₁} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} [self : Φ.IsLocalizedEquivalence] : (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence - CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} (isEquivalence : (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence) : Φ.IsLocalizedEquivalence - CategoryTheory.LocalizerMorphism.isEquivalence 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [h : Φ.IsLocalizedEquivalence] [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] : G.IsEquivalence - CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk' 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] [G.IsEquivalence] : Φ.IsLocalizedEquivalence - CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] (h : W₂ ≤ W₁.map Φ.functor) : Φ.IsLocalizedEquivalence - CategoryTheory.LocalizerMorphism.isEquivalence_imp 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [CategoryTheory.Category.{v₄', u₄'} D₁'] [CategoryTheory.Category.{v₅', u₅'} D₂'] (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'] [G.IsEquivalence] : G'.IsEquivalence - CategoryTheory.LocalizerMorphism.isEquivalence_iff 📋 Mathlib.CategoryTheory.Localization.LocalizerMorphism
{C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [CategoryTheory.Category.{v₄', u₄'} D₁'] [CategoryTheory.Category.{v₅', u₅'} D₂'] (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'] : G.IsEquivalence ↔ G'.IsEquivalence - HomologicalComplex.instIsEquivalenceOppositeSymmOpFunctor 📋 Mathlib.Algebra.Homology.Opposite
{ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.opFunctor V c).IsEquivalence - HomologicalComplex.instIsEquivalenceOppositeSymmOpInverse 📋 Mathlib.Algebra.Homology.Opposite
{ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.opInverse V c).IsEquivalence - HomologicalComplex.instIsEquivalenceOppositeSymmUnopFunctor 📋 Mathlib.Algebra.Homology.Opposite
{ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.unopFunctor V c).IsEquivalence - HomologicalComplex.instIsEquivalenceSymmOppositeUnopInverse 📋 Mathlib.Algebra.Homology.Opposite
{ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.unopInverse V c).IsEquivalence - CategoryTheory.prod.associatorIsEquivalence 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.prod.associator C D E).IsEquivalence - CategoryTheory.prod.inverseAssociatorIsEquivalence 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.prod.inverseAssociator C D E).IsEquivalence - CategoryTheory.IsVanKampenColimit.mapCocone_iff 📋 Mathlib.CategoryTheory.Limits.VanKampen
{J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} [G.IsEquivalence] : CategoryTheory.IsVanKampenColimit (G.mapCocone c) ↔ CategoryTheory.IsVanKampenColimit c - CategoryTheory.Functor.IsDenseSubsite.hasWeakSheafify_of_isEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.HasWeakSheafify K A - CategoryTheory.Functor.IsDenseSubsite.hasSheafify_of_isEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasSheafify K A
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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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 ce5dd8c