Loogle!

Result

Found 1502 declarations mentioning Quiver.Hom.op. Of these, only the first 200 are shown.

• Quiver.Hom.op 📋 Mathlib.Combinatorics.Quiver.Basic
  {V : Type u_1} [Quiver V] {X Y : V} (f : X ⟶ Y) : Opposite.op Y ⟶ Opposite.op X
• Quiver.Hom.op_inj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [Quiver C] {X Y : C} : Function.Injective Quiver.Hom.op
• CategoryTheory.op_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : C} : (CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)
• Quiver.Hom.unop_op 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [Quiver C] {X Y : C} (f : X ⟶ Y) : f.op.unop = f
• CategoryTheory.isIso_of_op 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f.op] : CategoryTheory.IsIso f
• CategoryTheory.isIso_op 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.op
• CategoryTheory.isIso_op_iff 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso f.op ↔ CategoryTheory.IsIso f
• CategoryTheory.op_id_unop 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : Cᵒᵖ} : (CategoryTheory.CategoryStruct.id (Opposite.unop X)).op = CategoryTheory.CategoryStruct.id X
• Quiver.Hom.op_unop 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [Quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f
• CategoryTheory.Iso.op_hom 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : α.op.hom = α.hom.op
• CategoryTheory.Iso.op_inv 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : α.op.inv = α.inv.op
• CategoryTheory.op_comp 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (CategoryTheory.CategoryStruct.comp f g).op = CategoryTheory.CategoryStruct.comp g.op f.op
• CategoryTheory.op_inv 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (CategoryTheory.inv f).op = CategoryTheory.inv f.op
• CategoryTheory.opOp_map 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.opOp C).map f = f.op.op
• CategoryTheory.op_comp_unop 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp g.unop f.unop).op = CategoryTheory.CategoryStruct.comp f g
• CategoryTheory.Functor.op_map 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : F.op.map f = (F.map f.unop).op
• CategoryTheory.Functor.rightOp_map 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : F.rightOp.map f = (F.map f.op).op
• CategoryTheory.op_comp_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {Z' : Cᵒᵖ} {h : Opposite.op X ⟶ Z'} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).op h = CategoryTheory.CategoryStruct.comp g.op (CategoryTheory.CategoryStruct.comp f.op h)
• CategoryTheory.NatTrans.op_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : Cᵒᵖ) : (CategoryTheory.NatTrans.op α).app X = (α.app (Opposite.unop X)).op
• CategoryTheory.Functor.rightOp_map_unop 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {X Y : C} (f : X ⟶ Y) : (F.rightOp.map f).unop = F.map f.op
• CategoryTheory.Functor.unop_map 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : F.unop.map f = (F.map f.op).unop
• CategoryTheory.NatTrans.rightOp_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (x✝ : C) : (CategoryTheory.NatTrans.rightOp α).app x✝ = (α.app (Opposite.op x✝)).op
• CategoryTheory.NatTrans.removeUnop_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F.unop ⟶ G.unop) (X : Cᵒᵖ) : (CategoryTheory.NatTrans.removeUnop α).app X = (α.app (Opposite.unop X)).op
• CategoryTheory.NatTrans.removeLeftOp_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (α : F.leftOp ⟶ G.leftOp) (X : C) : (CategoryTheory.NatTrans.removeLeftOp α).app X = (α.app (Opposite.op X)).op
• CategoryTheory.opEquiv_symm_apply 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ) (g : Opposite.unop B ⟶ Opposite.unop A) : (CategoryTheory.opEquiv A B).symm g = g.op
• CategoryTheory.Functor.opHom_map_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : (CategoryTheory.Functor C D)ᵒᵖ} (α : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((CategoryTheory.Functor.opHom C D).map α).app X = (α.unop.app (Opposite.unop X)).op
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).op
• CategoryTheory.Equivalence.leftOp_inverse_map 📋 Mathlib.CategoryTheory.Opposites
  {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.leftOp.inverse.map f = (e.inverse.map f.op).op
• CategoryTheory.Functor.leftOpRightOpEquiv_inverse_map 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor C Dᵒᵖ} (η : X✝ ⟶ Y✝) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op
• CategoryTheory.Functor.opInv_map 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : X✝ ⟶ Y✝) : (CategoryTheory.Functor.opInv C D).map α = Quiver.Hom.op { app := fun X => (α.app (Opposite.op X)).unop, naturality := ⋯ }
• CategoryTheory.Equivalence.rightOp_functor_map 📋 Mathlib.CategoryTheory.Opposites
  {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.rightOp.functor.map f = (e.functor.map f.op).op
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ} (η : X✝ ⟶ Y✝) (x✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.map η).app x✝ = (η.unop.app (Opposite.op x✝)).op
• 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_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.eqToHom_op 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y) : (CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom ⋯
• CategoryTheory.prodOpEquiv_functor_map 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {X✝ Y✝ : (C × D)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.prodOpEquiv C).functor.map f = CategoryTheory.Prod.mkHom f.unop.1.op f.unop.2.op
• CategoryTheory.prodOpEquiv_counitIso_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).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.prodOpEquiv_counitIso_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).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Groupoid.invEquivalence_functor_map 📋 Mathlib.CategoryTheory.Groupoid
  (C : Type u) [CategoryTheory.Groupoid C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) : (CategoryTheory.Groupoid.invEquivalence C).functor.map f = (CategoryTheory.Groupoid.inv f).op
• CategoryTheory.Groupoid.invEquivalence_unitIso 📋 Mathlib.CategoryTheory.Groupoid
  (C : Type u) [CategoryTheory.Groupoid C] : (CategoryTheory.Groupoid.invEquivalence C).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).obj x)) ⋯
• CategoryTheory.Groupoid.invEquivalence_counitIso 📋 Mathlib.CategoryTheory.Groupoid
  (C : Type u) [CategoryTheory.Groupoid C] : (CategoryTheory.Groupoid.invEquivalence C).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := Opposite.unop, map := fun {x y} f => CategoryTheory.Groupoid.inv f.unop, map_id := ⋯, map_comp := ⋯ }.comp { obj := Opposite.op, map := fun {x x_1} f => (CategoryTheory.Groupoid.inv f).op, map_id := ⋯, map_comp := ⋯ }).obj x)) ⋯
• CategoryTheory.CommSq.op 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CategoryTheory.CommSq f g h i) : CategoryTheory.CommSq i.op h.op g.op f.op
• CategoryTheory.CommSq.LiftStruct.op 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (l : sq.LiftStruct) : ⋯.LiftStruct
• CategoryTheory.CommSq.HasLift.iff_op 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) : sq.HasLift ↔ ⋯.HasLift
• CategoryTheory.CommSq.LiftStruct.opEquiv 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) : sq.LiftStruct ≃ ⋯.LiftStruct
• CategoryTheory.CommSq.LiftStruct.op_l 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (l : sq.LiftStruct) : l.op.l = l.l.op
• CategoryTheory.CommSq.LiftStruct.opEquiv_apply 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : sq.LiftStruct) : (CategoryTheory.CommSq.LiftStruct.opEquiv sq) l = l.op
• CategoryTheory.CommSq.LiftStruct.opEquiv_symm_apply 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : ⋯.LiftStruct) : (CategoryTheory.CommSq.LiftStruct.opEquiv sq).symm l = l.unop
• CategoryTheory.CommSq.LiftStruct.unopEquiv_symm_apply 📋 Mathlib.CategoryTheory.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : ⋯.LiftStruct) : (CategoryTheory.CommSq.LiftStruct.unopEquiv sq).symm l = l.op
• CategoryTheory.instIsSplitEpiOppositeOpOfIsSplitMono 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] : CategoryTheory.IsSplitEpi f.op
• CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitMono 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsSplitEpi f] : CategoryTheory.IsSplitMono f.op
• CategoryTheory.op_epi_of_mono 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) [CategoryTheory.Mono f] : CategoryTheory.Epi f.op
• CategoryTheory.op_mono_of_epi 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : B ⟶ A) [CategoryTheory.Epi f] : CategoryTheory.Mono f.op
• CategoryTheory.SplitEpi.op 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (h : CategoryTheory.SplitEpi f) : CategoryTheory.SplitMono f.op
• CategoryTheory.SplitMono.op 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (h : CategoryTheory.SplitMono f) : CategoryTheory.SplitEpi f.op
• CategoryTheory.op_epi_iff 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi f.op ↔ CategoryTheory.Mono f
• CategoryTheory.op_mono_iff 📋 Mathlib.CategoryTheory.EpiMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : CategoryTheory.Mono f.op ↔ CategoryTheory.Epi f
• CategoryTheory.isIso_iff_isIso_coyoneda_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.coyoneda.map f.op).app c)
• CategoryTheory.yonedaEquiv_symm_app_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x
• CategoryTheory.Coyoneda.fullyFaithful_preimage 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) : CategoryTheory.Coyoneda.fullyFaithful.preimage f = Quiver.Hom.op ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.unop X))) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))
• CategoryTheory.Functor.RepresentableBy.homEquiv_eq 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y) : e.homEquiv f = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (e.homEquiv (CategoryTheory.CategoryStruct.id Y))
• CategoryTheory.Functor.RepresentableBy.homEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (self : F.RepresentableBy Y) {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y) : self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (self.homEquiv g)
• CategoryTheory.Functor.RepresentableBy.mk 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)) (homEquiv_comp : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), homEquiv (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g) := by cat_disch) : F.RepresentableBy Y
• CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (Opposite.op X')) (f : X ⟶ X') : CategoryTheory.CategoryStruct.comp f (e.homEquiv.symm x) = e.homEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x)
• CategoryTheory.Functor.reprW_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [F.IsRepresentable] (X : Cᵒᵖ) (f : Opposite.unop X ⟶ F.reprX) : (CategoryTheory.ConcreteCategory.hom (F.reprW.hom.app X)) f = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) F.reprx
• CategoryTheory.Functor.uliftYonedaReprXIso_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max v v₁))) [F.IsRepresentable] (X : Cᵒᵖ) (f : ULift.{v, v₁} (Opposite.unop X ⟶ F.reprX)) : (CategoryTheory.ConcreteCategory.hom (F.uliftYonedaReprXIso.hom.app X)) f = (CategoryTheory.ConcreteCategory.hom (F.map f.down.op)) F.reprx
• CategoryTheory.coyonedaEquiv_coyoneda_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
• CategoryTheory.uliftYonedaEquiv_symm_apply_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) : (CategoryTheory.uliftYonedaEquiv.symm x).app Y = TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map y.down.op)) x
• CategoryTheory.yonedaEquiv_symm_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) : (CategoryTheory.yonedaEquiv.symm x).app Y = TypeCat.ofHom fun f => (CategoryTheory.ConcreteCategory.hom (F.map (Quiver.Hom.op f))) x
• CategoryTheory.coyonedaPairing_map 📋 Mathlib.CategoryTheory.Yoneda
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.coyonedaPairing C).obj P) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaPairing C).map α)) β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)
• CategoryTheory.coyonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
• CategoryTheory.coyonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type v₁)} (t : F.obj X) : CategoryTheory.coyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)
• CategoryTheory.map_yonedaEquiv 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.map g.op)) (CategoryTheory.yonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) g
• CategoryTheory.uliftCoyonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type (max w v₁))} (f : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.uliftCoyonedaEquiv f) = CategoryTheory.uliftCoyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map g.op) f)
• CategoryTheory.uliftCoyonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type (max w v₁))} (t : F.obj X) : CategoryTheory.uliftCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f.op) (CategoryTheory.uliftCoyonedaEquiv.symm t)
• CategoryTheory.uliftCoyonedaEquiv_symm_map_assoc 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type (max w v₁))} (t : F.obj X) {Z : CategoryTheory.Functor C (Type (max w v₁))} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f.op) (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyonedaEquiv.symm t) h)
• CategoryTheory.yonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.map g.op)) (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
• CategoryTheory.yonedaEquiv_symm_naturality_left 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (x : F.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) (CategoryTheory.yonedaEquiv.symm x) = CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x)
• CategoryTheory.Limits.coconeOfConeLeftOp_ι_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) (X : J) : (CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app X = (c.π.app (Opposite.op X)).op
• CategoryTheory.Limits.coneOfCoconeLeftOp_π_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) (X : J) : (CategoryTheory.Limits.coneOfCoconeLeftOp c).π.app X = (c.ι.app (Opposite.op X)).op
• CategoryTheory.Limits.coconeOpEquiv_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {Y✝ X✝ : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y✝ ⟶ X✝) : (CategoryTheory.Limits.coconeOpEquiv.functor.map f).hom = f.unop.hom.op
• CategoryTheory.Limits.coneOpEquiv_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X✝ Y✝ : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.coneOpEquiv.functor.map f).hom = f.unop.hom.op
• CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} {X✝ Y✝ : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.coconeRightOpOfConeEquiv.functor.map f).hom = f.unop.hom.op
• CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} {Y✝ X✝ : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y✝ ⟶ X✝) : (CategoryTheory.Limits.coneRightOpOfCoconeEquiv.functor.map f).hom = f.unop.hom.op
• CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_map 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} {X✝ Y✝ : CategoryTheory.Limits.Cocone F.leftOp} (f : X✝ ⟶ Y✝) : CategoryTheory.Limits.coconeLeftOpOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
• CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_map 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} {Y✝ X✝ : CategoryTheory.Limits.Cone F.leftOp} (f : Y✝ ⟶ X✝) : CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
• CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_map 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {X✝ Y✝ : CategoryTheory.Limits.Cocone F.unop} (f : X✝ ⟶ Y✝) : CategoryTheory.Limits.coconeUnopOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
• CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_map 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {Y✝ X✝ : CategoryTheory.Limits.Cone F.unop} (f : Y✝ ⟶ X✝) : CategoryTheory.Limits.coneUnopOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
• CategoryTheory.Limits.coneOpEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.coneOpEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op c.unop, map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => (Opposite.unop c).op, map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} : CategoryTheory.Limits.coconeLeftOpOfConeEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeLeftOp c), map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.coconeLeftOpOfCone (Opposite.unop c), map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} : CategoryTheory.Limits.coconeRightOpOfConeEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeRightOp c), map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.coconeRightOpOfCone (Opposite.unop c), map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} : CategoryTheory.Limits.coconeUnopOfConeEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeUnop c), map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.coconeUnopOfCone (Opposite.unop c), map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coconeOpEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.coconeOpEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op c.unop, map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => (Opposite.unop c).op, map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} : CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeLeftOp c), map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.coneLeftOpOfCocone (Opposite.unop c), map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} : CategoryTheory.Limits.coneRightOpOfCoconeEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeRightOp c), map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.coneRightOpOfCocone (Opposite.unop c), map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} : CategoryTheory.Limits.coneUnopOfCoconeEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeUnop c), map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.coneUnopOfCocone (Opposite.unop c), map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.orderDualEquivalence_functor_map 📋 Mathlib.CategoryTheory.Category.Preorder
  (X : Type u) [Preorder X] {X✝ Y✝ : Xᵒᵈ} (f : X✝ ⟶ Y✝) : (CategoryTheory.orderDualEquivalence X).functor.map f = (CategoryTheory.homOfLE ⋯).op
• CategoryTheory.eqToHom_comp_homOfLE_op 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc).op = (CategoryTheory.homOfLE ⋯).op
• CategoryTheory.homOfLE_op_comp_eqToHom 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.eqToHom hbc) = (CategoryTheory.homOfLE ⋯).op
• CategoryTheory.eqToHom_comp_homOfLE_op_assoc 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) {Z : Xᵒᵖ} (h : Opposite.op c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hbc).op h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯).op h
• CategoryTheory.homOfLE_op_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) {Z : Xᵒᵖ} (h : Opposite.op c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hbc) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯).op h
• CategoryTheory.orderDualEquivalence_counitIso 📋 Mathlib.CategoryTheory.Category.Preorder
  (X : Type u) [Preorder X] : (CategoryTheory.orderDualEquivalence X).counitIso = CategoryTheory.Iso.refl ({ obj := fun x => OrderDual.toDual (Opposite.unop x), map := fun {X_1 Y} f => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun x => Opposite.op (OrderDual.ofDual x), map := fun {X_1 Y} f => (CategoryTheory.homOfLE ⋯).op, map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Retract.op_i 📋 Mathlib.CategoryTheory.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : h.op.i = h.r.op
• CategoryTheory.Retract.op_r 📋 Mathlib.CategoryTheory.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : h.op.r = h.i.op
• CategoryTheory.RetractArrow.op 📋 Mathlib.CategoryTheory.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.RetractArrow f.op g.op
• CategoryTheory.RetractArrow.op_i 📋 Mathlib.CategoryTheory.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : h.op.i = CategoryTheory.Arrow.homMk (CategoryTheory.Arrow.Hom.right h.r).op (CategoryTheory.Arrow.Hom.left h.r).op ⋯
• CategoryTheory.RetractArrow.op_r 📋 Mathlib.CategoryTheory.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : h.op.r = CategoryTheory.Arrow.homMk (CategoryTheory.Arrow.Hom.right h.i).op (CategoryTheory.Arrow.Hom.left h.i).op ⋯
• CategoryTheory.HasLiftingProperty.op 📋 Mathlib.CategoryTheory.LiftingProperties.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} (h : CategoryTheory.HasLiftingProperty i p) : CategoryTheory.HasLiftingProperty p.op i.op
• CategoryTheory.HasLiftingProperty.iff_op 📋 Mathlib.CategoryTheory.LiftingProperties.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} : CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.op i.op
• CategoryTheory.CostructuredArrow.toStructuredArrow_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.CostructuredArrow F d)ᵒᵖ) : (CategoryTheory.CostructuredArrow.toStructuredArrow F d).obj X = CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.op
• CategoryTheory.StructuredArrow.toCostructuredArrow_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.StructuredArrow d F)ᵒᵖ) : (CategoryTheory.StructuredArrow.toCostructuredArrow F d).obj X = CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.op
• CategoryTheory.StructuredArrow.toCostructuredArrow_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) {X✝ Y✝ : (CategoryTheory.StructuredArrow d F)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.StructuredArrow.toCostructuredArrow F d).map f = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f.unop).op ⋯
• CategoryTheory.CostructuredArrow.toStructuredArrow_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (d : D) {X✝ Y✝ : (CategoryTheory.CostructuredArrow F d)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.toStructuredArrow F d).map f = CategoryTheory.StructuredArrow.homMk f.unop.left.op ⋯
• CategoryTheory.Over.opEquivOpUnder_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : (CategoryTheory.Under X)ᵒᵖ) : (CategoryTheory.Over.opEquivOpUnder X).inverse.obj Y = CategoryTheory.Over.mk (Opposite.unop Y).hom.op
• CategoryTheory.Under.opEquivOpOver_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : (CategoryTheory.Over X)ᵒᵖ) : (CategoryTheory.Under.opEquivOpOver X).inverse.obj Y = CategoryTheory.Under.mk (Opposite.unop Y).hom.op
• CategoryTheory.Over.opEquivOpUnder_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : (CategoryTheory.Under X)ᵒᵖ} (f : Z ⟶ Y) : (CategoryTheory.Over.opEquivOpUnder X).inverse.map f = CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f.unop).op ⋯
• CategoryTheory.Under.opEquivOpOver_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : (CategoryTheory.Over X)ᵒᵖ} (f : Z ⟶ Y) : (CategoryTheory.Under.opEquivOpOver X).inverse.map f = CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f.unop).op ⋯
• CategoryTheory.Over.opEquivOpUnder_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Over.opEquivOpUnder X).counitIso = CategoryTheory.Iso.refl ({ obj := fun Y => CategoryTheory.Over.mk (Opposite.unop Y).hom.op, map := fun {Z Y} f => CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f.unop).op ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun Y => Opposite.op (CategoryTheory.Under.mk Y.hom.unop), map := fun {Z Y} f => Opposite.op (CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f).unop ⋯), map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Under.opEquivOpOver_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Under.opEquivOpOver X).counitIso = CategoryTheory.Iso.refl ({ obj := fun Y => CategoryTheory.Under.mk (Opposite.unop Y).hom.op, map := fun {Z Y} f => CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f.unop).op ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun Y => Opposite.op (CategoryTheory.Over.mk Y.hom.unop), map := fun {Z Y} f => Opposite.op (CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f).unop ⋯), map_id := ⋯, map_comp := ⋯ })
• CategoryTheory.Limits.BinaryCofan.op_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).op = CategoryTheory.Limits.BinaryFan.mk ι₁.op ι₂.op
• CategoryTheory.Limits.BinaryFan.op_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).op = CategoryTheory.Limits.BinaryCofan.mk π₁.op π₂.op
• CategoryTheory.Limits.walkingParallelPairOp_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  : CategoryTheory.Limits.walkingParallelPairOp.map CategoryTheory.Limits.WalkingParallelPairHom.left = Quiver.Hom.op CategoryTheory.Limits.WalkingParallelPairHom.left
• CategoryTheory.Limits.walkingParallelPairOp_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  : CategoryTheory.Limits.walkingParallelPairOp.map CategoryTheory.Limits.WalkingParallelPairHom.right = Quiver.Hom.op CategoryTheory.Limits.WalkingParallelPairHom.right
• CategoryTheory.MorphismProperty.MapFactorizationData.op 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f) : W₂.op.MapFactorizationData W₁.op f.op
• CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} : W₁.MapFactorizationData W₂ f ≃ W₂.op.MapFactorizationData W₁.op f.op
• CategoryTheory.MorphismProperty.MapFactorizationData.op_Z 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f) : (CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ hf).Z = Opposite.op hf.Z
• CategoryTheory.MorphismProperty.MapFactorizationData.op_i 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f) : (CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ hf).i = hf.p.op
• CategoryTheory.MorphismProperty.MapFactorizationData.op_p 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f) : (CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ hf).p = hf.i.op
• CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv_apply 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} (φ : W₁.MapFactorizationData W₂ f) : CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv φ = CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ φ
• CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv_symm_apply 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} (φ : W₂.op.MapFactorizationData W₁.op f.op) : CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv.symm φ = φ.unop
• CategoryTheory.Limits.op_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) : Quiver.Hom.op 0 = 0
• CategoryTheory.Limits.BinaryBicone.op_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.fst = b.inl.op
• CategoryTheory.Limits.BinaryBicone.op_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.inl = b.fst.op
• CategoryTheory.Limits.BinaryBicone.op_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.inr = b.snd.op
• CategoryTheory.Limits.BinaryBicone.op_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.snd = b.inr.op
• CategoryTheory.Limits.biprod.opIso_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom CategoryTheory.Limits.biprod.fst = CategoryTheory.Limits.biprod.inl.op
• CategoryTheory.Limits.biprod.opIso_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.inr.op
• CategoryTheory.Limits.biprod.inl_opIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.opIso P Q).inv = CategoryTheory.Limits.biprod.fst.op
• CategoryTheory.Limits.biprod.inr_opIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.opIso P Q).inv = CategoryTheory.Limits.biprod.snd.op
• CategoryTheory.Limits.biprod.fst_op_opIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst.op (CategoryTheory.Limits.biprod.opIso P Q).hom = CategoryTheory.Limits.biprod.inl
• CategoryTheory.Limits.biprod.opIso_inv_inl_op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv CategoryTheory.Limits.biprod.inl.op = CategoryTheory.Limits.biprod.fst
• CategoryTheory.Limits.biprod.opIso_inv_inr_op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv CategoryTheory.Limits.biprod.inr.op = CategoryTheory.Limits.biprod.snd
• CategoryTheory.Limits.biprod.snd_op_opIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op (CategoryTheory.Limits.biprod.opIso P Q).hom = CategoryTheory.Limits.biprod.inr
• CategoryTheory.Limits.biprod.inl_opIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op (P ⊞ Q) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst.op h
• CategoryTheory.Limits.biprod.inr_opIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op (P ⊞ Q) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op h
• CategoryTheory.Limits.biprod.opIso_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl.op h
• CategoryTheory.Limits.biprod.opIso_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr.op h
• CategoryTheory.Limits.biprod.fst_op_opIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⊞ Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst.op (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
• CategoryTheory.Limits.biprod.opIso_inv_inl_op_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl.op h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h
• CategoryTheory.Limits.biprod.opIso_inv_inr_op_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr.op h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h
• CategoryTheory.Limits.biprod.snd_op_opIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⊞ Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
• CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (c.π.app (Opposite.op 0)))
• CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} (hF : ∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.limitCone F).π.app (Opposite.op 0)))
• CategoryTheory.shrinkCoyonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) {P : CategoryTheory.Functor C (Type w)} (t : P.obj X) : CategoryTheory.shrinkCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (P.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyoneda.{w, v, u}.map f.op) (CategoryTheory.shrinkCoyonedaEquiv.symm t)
• CategoryTheory.shrinkYonedaObjObjEquiv_symm_comp 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) : CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.obj X).map g.op)) (CategoryTheory.shrinkYonedaObjObjEquiv.symm f)
• CategoryTheory.shrinkCoyonedaEquiv_symm_map_assoc 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) {P : CategoryTheory.Functor C (Type w)} (t : P.obj X) {Z : CategoryTheory.Functor C (Type w)} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (P.map f)) t)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyoneda.{w, v, u}.map f.op) (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaEquiv.symm t) h)
• CategoryTheory.shrinkYonedaEquiv_naturality 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (P.map g.op)) (CategoryTheory.shrinkYonedaEquiv f) = CategoryTheory.shrinkYonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYoneda.{w, v, u}.map g) f)
• CategoryTheory.shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X : C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (s : P.obj (Opposite.op X)) {Y : C} (f : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaEquiv.symm s).app (Opposite.op Y))) (CategoryTheory.shrinkYonedaObjObjEquiv.symm f) = (CategoryTheory.ConcreteCategory.hom (P.map f.op)) s
• CategoryTheory.map_shrinkYonedaEquiv 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (P.map g.op)) (CategoryTheory.shrinkYonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) (CategoryTheory.shrinkYonedaObjObjEquiv.symm g)
• CategoryTheory.Limits.coneOfSectionCompYoneda_π_app 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) : (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).π.app j = Quiver.Hom.op (↑s j)
• CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_2} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget C)] {F : CategoryTheory.Functor ℕᵒᵖ C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (c.π.app (Opposite.op 0)))
• CategoryTheory.op_whiskerLeft 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).op = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.op X) f.op
• CategoryTheory.op_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).op = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.op (Opposite.op Z)
• CategoryTheory.op_tensorHom 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).op = CategoryTheory.MonoidalCategoryStruct.tensorHom f.op g.op
• CategoryTheory.op_hom_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.op = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.op X)).inv
• CategoryTheory.op_hom_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.op = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.op X)).inv
• CategoryTheory.op_inv_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.op = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.op X)).hom
• CategoryTheory.op_inv_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.op = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.op X)).hom
• CategoryTheory.op_tensor_op 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom f.op g.op = (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).op
• CategoryTheory.op_hom_associator 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.op = (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).inv
• CategoryTheory.op_inv_associator 📋 Mathlib.CategoryTheory.Monoidal.Opposite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.op = (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).hom
• CategoryTheory.op_hom_braiding 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).hom.op = (β_ (Opposite.op Y) (Opposite.op X)).hom
• CategoryTheory.op_inv_braiding 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).inv.op = (β_ (Opposite.op Y) (Opposite.op X)).inv
• CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
• CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
• CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
• CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
• CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
• CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
• CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
• CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c)) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
• CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
• CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c)) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
• CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeUnopOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
• CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeUnopOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
• CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom (CategoryTheory.Limits.colimit.ι F j).op = CategoryTheory.Limits.limit.π F.op (Opposite.op j)
• CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).op (CategoryTheory.Limits.colimitOpIsoOpLimit F).inv = CategoryTheory.Limits.colimit.ι F.op (Opposite.op j)
• CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv (CategoryTheory.Limits.limit.π F.op j) = (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).op
• CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.op j) (CategoryTheory.Limits.colimitOpIsoOpLimit F).hom = (CategoryTheory.Limits.limit.π F (Opposite.unop j)).op
• CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv (CategoryTheory.Limits.limit.π F.rightOp j) = (CategoryTheory.Limits.colimit.ι F (Opposite.op j)).op
• CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasLimit F] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.rightOp j) (CategoryTheory.Limits.colimitRightOpIsoUnopLimit F).hom = (CategoryTheory.Limits.limit.π F (Opposite.op j)).op
• CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom (CategoryTheory.Limits.colimit.ι F j).op = CategoryTheory.Limits.limit.π F.rightOp (Opposite.unop j)
• CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).op (CategoryTheory.Limits.colimitRightOpIsoUnopLimit F).inv = CategoryTheory.Limits.colimit.ι F.rightOp (Opposite.unop j)
• CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] (j : J) {Z : Cᵒᵖ} (h : Opposite.op (F.obj j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j).op h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.op (Opposite.op j)) h

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

5. 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