Loogle!

Result

Found 939 declarations mentioning CategoryTheory.ObjectProperty.FullSubcategory. Of these, only the first 200 are shown.

• CategoryTheory.ObjectProperty.FullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : Type u
• CategoryTheory.ObjectProperty.FullSubcategory.category 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.Category.{v, u} P.FullSubcategory
• CategoryTheory.ObjectProperty.FullSubcategory.obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (self : P.FullSubcategory) : C
• CategoryTheory.ObjectProperty.FullSubcategory.mk 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (obj : C) (property : P obj) : P.FullSubcategory
• CategoryTheory.ObjectProperty.FullSubcategory.property 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (self : P.FullSubcategory) : P self.obj
• CategoryTheory.ObjectProperty.instNonemptyFullSubcategoryOfNonempty 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : Nonempty P.FullSubcategory
• CategoryTheory.ObjectProperty.ι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.Functor P.FullSubcategory C
• CategoryTheory.ObjectProperty.faithful_ι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.Faithful
• CategoryTheory.ObjectProperty.full_ι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.Full
• CategoryTheory.ObjectProperty.fullyFaithfulι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.FullyFaithful
• CategoryTheory.ObjectProperty.prop_ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory) : P (P.ι.obj X)
• CategoryTheory.ObjectProperty.ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : P.FullSubcategory} : P.ι.obj X = X.obj
• CategoryTheory.ObjectProperty.FullSubcategory.ext 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {x y : P.FullSubcategory} (obj : x.obj = y.obj) : x = y
• CategoryTheory.ObjectProperty.lift 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : CategoryTheory.Functor C P.FullSubcategory
• CategoryTheory.ObjectProperty.FullSubcategory.ext_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {x y : P.FullSubcategory} : x = y ↔ x.obj = y.obj
• CategoryTheory.ObjectProperty.isoMk 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : X ≅ Y
• CategoryTheory.ObjectProperty.ιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : CategoryTheory.Functor P.FullSubcategory P'.FullSubcategory
• CategoryTheory.ObjectProperty.faithful_ιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).Faithful
• CategoryTheory.ObjectProperty.full_ιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).Full
• CategoryTheory.ObjectProperty.fullyFaithfulιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).FullyFaithful
• CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Faithful] : (P.lift F hF).Faithful
• CategoryTheory.ObjectProperty.instFullFullSubcategoryLift 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Full] : (P.lift F hF).Full
• CategoryTheory.ObjectProperty.homMk 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : X ⟶ Y
• CategoryTheory.ObjectProperty.lift_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : ((P.lift F hF).obj X).obj = F.obj X
• CategoryTheory.ObjectProperty.homMk_surjective 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} : Function.Surjective CategoryTheory.ObjectProperty.homMk
• CategoryTheory.ObjectProperty.liftCompιIso 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : (P.lift F hF).comp P.ι ≅ F
• CategoryTheory.ObjectProperty.ιOfLE_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') (X : P.FullSubcategory) : ((CategoryTheory.ObjectProperty.ιOfLE h).obj X).obj = X.obj
• CategoryTheory.ObjectProperty.FullSubcategory.id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.ι_obj_lift_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : P.ι.obj ((P.lift F hF).obj X) = F.obj X
• CategoryTheory.ObjectProperty.homMk_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : (CategoryTheory.ObjectProperty.homMk f).hom = f
• CategoryTheory.ObjectProperty.instIsIsoHomFullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom
• CategoryTheory.ObjectProperty.isIso_hom_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) : CategoryTheory.IsIso f.hom ↔ CategoryTheory.IsIso f
• CategoryTheory.ObjectProperty.ιOfLECompιIso 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).comp P'.ι ≅ P.ι
• CategoryTheory.ObjectProperty.isoMk_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).hom = CategoryTheory.ObjectProperty.homMk e.hom
• CategoryTheory.ObjectProperty.isoMk_inv 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).inv = CategoryTheory.ObjectProperty.homMk e.inv
• CategoryTheory.ObjectProperty.ι_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} {f : X ⟶ Y} : P.ι.map f = f.hom
• CategoryTheory.ObjectProperty.liftCompιOfLEIso 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) {Q : CategoryTheory.ObjectProperty D} (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (h : P ≤ Q) : (P.lift F hF).comp (CategoryTheory.ObjectProperty.ιOfLE h) ≅ Q.lift F ⋯
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.hom e.inv.hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.hom e.hom.hom = CategoryTheory.CategoryStruct.id Y.obj
• CategoryTheory.ObjectProperty.hom_ext 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g
• CategoryTheory.ObjectProperty.hom_inv 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (CategoryTheory.inv f).hom = CategoryTheory.inv f.hom
• CategoryTheory.ObjectProperty.hom_ext_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : X.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.hom (CategoryTheory.CategoryStruct.comp e.inv.hom h) = h
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : Y.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.hom (CategoryTheory.CategoryStruct.comp e.hom.hom h) = h
• CategoryTheory.ObjectProperty.lift_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (P.lift F hF).map f = CategoryTheory.ObjectProperty.homMk (F.map f)
• CategoryTheory.ObjectProperty.FullSubcategory.comp_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.ObjectProperty.ιOfLE_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') {X✝ Y✝ : P.FullSubcategory} (f : X✝ ⟶ Y✝) : (CategoryTheory.ObjectProperty.ιOfLE h).map f = CategoryTheory.ObjectProperty.homMk f.hom
• CategoryTheory.ObjectProperty.ι_obj_lift_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C} (f : X ⟶ Y) : P.ι.map ((P.lift F hF).map f) = F.map f
• CategoryTheory.ObjectProperty.FullSubcategory.comp_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
• CategoryTheory.FullSubcategory.concreteCategory 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_2} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ConcreteCategory P.FullSubcategory fun X Y => FC X.obj Y.obj
• CategoryTheory.ObjectProperty.FullSubcategory.concreteCategory 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_2} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ConcreteCategory P.FullSubcategory fun X Y => FC X.obj Y.obj
• CategoryTheory.Functor.essImage_ι_comp 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) : (P.ι.comp F).essImage = P.map F
• CategoryTheory.Functor.toEssImage_map_hom 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (F.toEssImage.map f).hom = F.map f
• CategoryTheory.Functor.essImage_ext 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y) (h : F.essImage.ι.map f = F.essImage.ι.map g) : f = g
• CategoryTheory.Functor.toEssImageCompι_hom_app 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.toEssImageCompι.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.toEssImageCompι_inv_app 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.toEssImageCompι.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J) : (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).hom.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).hom.hom
• CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J) : (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).inv.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).inv.hom
• CategoryTheory.Functor.essImage.liftFunctor_map 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) {i j : J} (f : i ⟶ j) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).map f = F.preimage (CategoryTheory.CategoryStruct.comp (F.toEssImage.objObjPreimageIso { obj := G.obj i, property := ⋯ }).hom.hom (CategoryTheory.CategoryStruct.comp (G.map f) (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv.hom))
• CategoryTheory.ObjectProperty.fullSubcategoryCongr 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : P.FullSubcategory ≌ P'.FullSubcategory
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).functor = CategoryTheory.ObjectProperty.ιOfLE ⋯
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).inverse = CategoryTheory.ObjectProperty.ιOfLE ⋯
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.FullSubcategory)
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_counitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.ObjectProperty.ιOfLE ⋯).comp (CategoryTheory.ObjectProperty.ιOfLE ⋯))
• CategoryTheory.ObjectProperty.eqToHom_hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (h : X = Y) : (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.FullSubcategory.hasForget₂ 📋 Mathlib.CategoryTheory.ConcreteCategory.Forget
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.HasForget₂ P.FullSubcategory C
• CategoryTheory.ObjectProperty.FullSubcategory.hasForget₂ 📋 Mathlib.CategoryTheory.ConcreteCategory.Forget
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.HasForget₂ P.FullSubcategory C
• CategoryTheory.locallySmall_fullSubcategory 📋 Mathlib.CategoryTheory.EssentiallySmall
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.LocallySmall.{w, v, u} P.FullSubcategory
• CategoryTheory.essentiallySmall_fullSubcategory_mem 📋 Mathlib.CategoryTheory.EssentiallySmall
  (C : Type u) [CategoryTheory.Category.{v, u} C] (s : Set C) [Small.{w, u} ↑s] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.EssentiallySmall.{w, v, u} (CategoryTheory.ObjectProperty.FullSubcategory fun x => x ∈ s)
• CategoryTheory.ObjectProperty.instHasZeroMorphismsFullSubcategory 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.Limits.HasZeroMorphisms P.FullSubcategory
• CategoryTheory.ObjectProperty.homMk_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory) : CategoryTheory.ObjectProperty.homMk 0 = 0
• CategoryTheory.ObjectProperty.zero_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory) : CategoryTheory.InducedCategory.Hom.hom 0 = 0
• CategoryTheory.Preadditive.fullSubcategory 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Z : CategoryTheory.ObjectProperty C) : CategoryTheory.Preadditive Z.FullSubcategory
• CategoryTheory.Linear.fullSubcategory 📋 Mathlib.CategoryTheory.Linear.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (Z : CategoryTheory.ObjectProperty C) : CategoryTheory.Linear R Z.FullSubcategory
• CategoryTheory.ObjectProperty.ι_map_top 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : ⊤.map P.ι = P.isoClosure
• CategoryTheory.ExactFunctor.forget_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) : (CategoryTheory.ExactFunctor.forget C D).map α = α.hom
• CategoryTheory.LeftExactFunctor.forget_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : C ⥤ₗ D} (α : F ⟶ G) : (CategoryTheory.LeftExactFunctor.forget C D).map α = α.hom
• CategoryTheory.RightExactFunctor.forget_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : C ⥤ᵣ D} (α : F ⟶ G) : (CategoryTheory.RightExactFunctor.forget C D).map α = α.hom
• CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : C ⥤ₑ D) (X : D ⥤ₑ E) : (((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).obj X).obj = F.obj.comp X.obj
• CategoryTheory.ExactFunctor.whiskeringRight_obj_obj_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : D ⥤ₑ E) (X : C ⥤ₑ D) : (((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).obj X).obj = X.obj.comp F.obj
• CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : C ⥤ₗ D) (X : D ⥤ₗ E) : (((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).obj X).obj = F.obj.comp X.obj
• CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : D ⥤ₗ E) (X : C ⥤ₗ D) : (((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).obj X).obj = X.obj.comp F.obj
• CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : C ⥤ᵣ D) (X : D ⥤ᵣ E) : (((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).obj X).obj = F.obj.comp X.obj
• CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : D ⥤ᵣ E) (X : C ⥤ᵣ D) : (((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).obj X).obj = X.obj.comp F.obj
• CategoryTheory.LeftExactFunctor.ofExact_map_hom 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((CategoryTheory.LeftExactFunctor.ofExact C D).map α).hom = α.hom
• CategoryTheory.RightExactFunctor.ofExact_map_hom 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((CategoryTheory.RightExactFunctor.ofExact C D).map α).hom = α.hom
• CategoryTheory.ExactFunctor.whiskeringLeft_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : C ⥤ₑ D) {X✝ Y✝ : D ⥤ₑ E} (f : X✝ ⟶ Y✝) : ((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (F.obj.whiskerLeft f.hom)
• CategoryTheory.ExactFunctor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : D ⥤ₑ E) {X✝ Y✝ : C ⥤ₑ D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
• CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : C ⥤ₗ D) {X✝ Y✝ : D ⥤ₗ E} (f : X✝ ⟶ Y✝) : ((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (F.obj.whiskerLeft f.hom)
• CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : D ⥤ₗ E) {X✝ Y✝ : C ⥤ₗ D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
• CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : C ⥤ᵣ D) {X✝ Y✝ : D ⥤ᵣ E} (f : X✝ ⟶ Y✝) : ((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (F.obj.whiskerLeft f.hom)
• CategoryTheory.RightExactFunctor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 : D ⥤ᵣ E) {X✝ Y✝ : C ⥤ᵣ D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
• CategoryTheory.ExactFunctor.whiskeringLeft_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 G : C ⥤ₑ D} (η : F ⟶ G) (H : D ⥤ₑ E) : ((CategoryTheory.ExactFunctor.whiskeringLeft C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringLeft C D E).map η.hom).app H.obj)
• CategoryTheory.ExactFunctor.whiskeringRight_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 G : D ⥤ₑ E} (η : F ⟶ G) (H : C ⥤ₑ D) : ((CategoryTheory.ExactFunctor.whiskeringRight C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
• CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 G : C ⥤ₗ D} (η : F ⟶ G) (H : D ⥤ₗ E) : ((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringLeft C D E).map η.hom).app H.obj)
• CategoryTheory.LeftExactFunctor.whiskeringRight_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 G : D ⥤ₗ E} (η : F ⟶ G) (H : C ⥤ₗ D) : ((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
• CategoryTheory.RightExactFunctor.whiskeringLeft_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 G : C ⥤ᵣ D} (η : F ⟶ G) (H : D ⥤ᵣ E) : ((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringLeft C D E).map η.hom).app H.obj)
• CategoryTheory.RightExactFunctor.whiskeringRight_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (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 G : D ⥤ᵣ E} (η : F ⟶ G) (H : C ⥤ᵣ D) : ((CategoryTheory.RightExactFunctor.whiskeringRight C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
• CategoryTheory.Functor.fullSubcategoryInclusion_additive 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (Z : CategoryTheory.ObjectProperty C) : Z.ι.Additive
• CategoryTheory.Functor.instAdditiveFullSubcategoryLift 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor D C) [F.Additive] (P : CategoryTheory.ObjectProperty C) (hF : ∀ (X : D), P (F.obj X)) : (P.lift F hF).Additive
• CategoryTheory.AdditiveFunctor.forget_map 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F G : C ⥤+ D) (α : F ⟶ G) : (CategoryTheory.AdditiveFunctor.forget C D).map α = α.hom
• CategoryTheory.AdditiveFunctor.ofExact_map_hom 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((CategoryTheory.AdditiveFunctor.ofExact C D).map α).hom = α.hom
• CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ₗ D} (α : F ⟶ G) : ((CategoryTheory.AdditiveFunctor.ofLeftExact C D).map α).hom = α.hom
• CategoryTheory.AdditiveFunctor.ofRightExact_map_hom 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ᵣ D} (α : F ⟶ G) : ((CategoryTheory.AdditiveFunctor.ofRightExact C D).map α).hom = α.hom
• CategoryTheory.MonoidalCategory.fullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) (tensorUnit : P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (tensorObj : ∀ (X Y : C), P X → P Y → P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) : CategoryTheory.MonoidalCategory P.FullSubcategory
• CategoryTheory.Functor.fullSubcategoryInclusionLinear 📋 Mathlib.CategoryTheory.Linear.LinearFunctor
  (R : Type u_1) [Semiring R] {C : Type u_4} [CategoryTheory.Category.{v_3, u_4} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (Z : CategoryTheory.ObjectProperty C) : CategoryTheory.Functor.Linear R Z.ι
• CategoryTheory.ObjectProperty.opEquivalence 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ
• CategoryTheory.ObjectProperty.opEquivalence_inverse 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.inverse = P.op.lift P.ι.op ⋯
• CategoryTheory.ObjectProperty.opEquivalence_functor 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.functor = (P.lift P.op.ι.leftOp ⋯).rightOp
• CategoryTheory.ObjectProperty.opEquivalence_unitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.op.FullSubcategory)
• CategoryTheory.ObjectProperty.opEquivalence_counitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.counitIso = CategoryTheory.Iso.refl ((P.op.lift P.ι.op ⋯).comp (P.lift P.op.ι.leftOp ⋯).rightOp)
• CategoryTheory.ObjectProperty.topEquivalence 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  (C : Type u) [CategoryTheory.Category.{v, u} C] : ⊤.FullSubcategory ≌ C
• 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.Equivalence.congrFullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : P.FullSubcategory ≌ Q.FullSubcategory
• CategoryTheory.ObjectProperty.essSurj_ι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).EssSurj ↔ Q ≤ P.isoClosure
• 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.ObjectProperty.topEquivalence_functor 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.ObjectProperty.topEquivalence C).functor = ⊤.ι
• CategoryTheory.ObjectProperty.topEquivalence_inverse 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.ObjectProperty.topEquivalence C).inverse = ⊤.lift (CategoryTheory.Functor.id C) ⋯
• CategoryTheory.Equivalence.congrFullSubcategory_functor 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).functor = Q.lift (P.ι.comp e.functor) ⋯
• CategoryTheory.Equivalence.congrFullSubcategory_inverse 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).inverse = P.lift (Q.ι.comp e.inverse) ⋯
• CategoryTheory.ObjectProperty.topEquivalence_counitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.ObjectProperty.topEquivalence C).counitIso = CategoryTheory.Iso.refl ((⊤.lift (CategoryTheory.Functor.id C) ⋯).comp ⊤.ι)
• CategoryTheory.ObjectProperty.topEquivalence_unitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.ObjectProperty.topEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id ⊤.FullSubcategory)
• CategoryTheory.Equivalence.congrFullSubcategory_counitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).counitIso = (Q.fullyFaithfulι.whiskeringRight Q.FullSubcategory).preimageIso (Q.ι.isoWhiskerLeft e.counitIso)
• CategoryTheory.Equivalence.congrFullSubcategory_unitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).unitIso = (P.fullyFaithfulι.whiskeringRight P.FullSubcategory).preimageIso (P.ι.isoWhiskerLeft e.unitIso)
• CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall 📋 Mathlib.CategoryTheory.ObjectProperty.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.Small.{w, v, u} P] : Small.{w, u} P.FullSubcategory
• CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall 📋 Mathlib.CategoryTheory.ObjectProperty.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] : CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory
• CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 📋 Mathlib.CategoryTheory.ObjectProperty.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] : CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory
• CategoryTheory.ObjectProperty.exists_equivalence_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.LocallySmall.{w', v, u} C] : (∃ J x, Nonempty (P.FullSubcategory ≌ J)) ↔ CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
• CategoryTheory.ObjectProperty.initial_ι 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) (h : ∀ (d : C), ¬P d → CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow P.ι d)) : P.ι.Initial
• CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (p : P.LimitOfShape J X) : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X P.ι)
• CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_obj 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (p : P.LimitOfShape J X) (j : J) : p.toStructuredArrow.obj j = CategoryTheory.StructuredArrow.mk (p.π.app j)
• CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (p : P.LimitOfShape J X) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : p.toStructuredArrow.map f = CategoryTheory.StructuredArrow.homMk (CategoryTheory.ObjectProperty.homMk (p.diag.map f)) ⋯
• CategoryTheory.ObjectProperty.instHasZeroObjectFullSubcategoryOfContainsZero 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] : CategoryTheory.Limits.HasZeroObject P.FullSubcategory
• CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow P.ι X)
• CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_obj 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) (j : J) : p.toCostructuredArrow.obj j = CategoryTheory.CostructuredArrow.mk (p.ι.app j)
• CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : p.toCostructuredArrow.map f = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.ObjectProperty.homMk (p.diag.map f)) ⋯
• CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J P.FullSubcategory
• CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J P.FullSubcategory
• CategoryTheory.Limits.createsColimitsOfShapeFullSubcategoryInclusion 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.CreatesColimitsOfShape J P.ι
• CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.CreatesLimitsOfShape J P.ι
• CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type w) [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasColimitsOfShape J P.FullSubcategory] [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.PreservesColimitsOfShape J P.ι] : P.IsClosedUnderColimitsOfShape J
• CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type w) [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasLimitsOfShape J P.FullSubcategory] [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfShape J P.ι] : P.IsClosedUnderLimitsOfShape J
• CategoryTheory.Limits.hasColimit_of_closedUnderColimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape J] (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasColimit (F.comp P.ι)] : CategoryTheory.Limits.HasColimit F
• CategoryTheory.Limits.hasLimit_of_closedUnderLimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasLimit (F.comp P.ι)] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape J] (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasColimit (F.comp P.ι)] : CategoryTheory.CreatesColimit F P.ι
• CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  (J : Type w) [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasLimit (F.comp P.ι)] : CategoryTheory.CreatesLimit F P.ι
• CategoryTheory.Limits.createsColimitFullSubcategoryInclusion 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasColimit (F.comp P.ι)] (h : P (CategoryTheory.Limits.colimit (F.comp P.ι))) : CategoryTheory.CreatesColimit F P.ι
• CategoryTheory.Limits.createsLimitFullSubcategoryInclusion 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasLimit (F.comp P.ι)] (h : P (CategoryTheory.Limits.limit (F.comp P.ι))) : CategoryTheory.CreatesLimit F P.ι
• CategoryTheory.Limits.createsColimitFullSubcategoryInclusion' 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (F : CategoryTheory.Functor J P.FullSubcategory) {c : CategoryTheory.Limits.Cocone (F.comp P.ι)} (hc : CategoryTheory.Limits.IsColimit c) (h : P c.pt) : CategoryTheory.CreatesColimit F P.ι
• CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (F : CategoryTheory.Functor J P.FullSubcategory) {c : CategoryTheory.Limits.Cone (F.comp P.ι)} (hc : CategoryTheory.Limits.IsLimit c) (h : P c.pt) : CategoryTheory.CreatesLimit F P.ι
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] : CategoryTheory.CartesianMonoidalCategory P.FullSubcategory
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory).obj = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y : P.FullSubcategory) : (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y).hom = CategoryTheory.SemiCartesianMonoidalCategory.fst X.obj Y.obj
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y : P.FullSubcategory) : (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd X.obj Y.obj
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty P.FullSubcategory)) : (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.lift s).hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit s.pt.obj
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X x✝ x✝¹ : P.FullSubcategory) (f : x✝ ⟶ x✝¹) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.obj f.hom
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] {X₁✝ X₂✝ : P.FullSubcategory} (f : X₁✝ ⟶ X₂✝) (X : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.obj
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] {X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.obj).hom
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.obj).inv
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj).hom
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj).inv
• CategoryTheory.Functor.EssImageSubcategory.lift_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.Limits.PreservesFiniteProducts F] {T X Y : F.EssImageSubcategory} (f : T ⟶ X) (g : T ⟶ Y) : CategoryTheory.CartesianMonoidalCategory.lift f g = CategoryTheory.ObjectProperty.homMk (CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom)
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y : P.FullSubcategory) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)) : ((CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y).lift t).hom = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.Limits.BinaryFan.fst t).hom (CategoryTheory.Limits.BinaryFan.snd t).hom
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y Z : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y Z : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv
• CategoryTheory.Functor.mapAddGrpFunctor_map_app 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F G : C ⥤ₗ D} (α : F ⟶ G) (A : CategoryTheory.AddGrp C) : (CategoryTheory.Functor.mapAddGrpFunctor.map α).app A = CategoryTheory.AddGrp.homMk'' (α.hom.app A.X) ⋯ ⋯
• CategoryTheory.Functor.mapGrpFunctor_map_app 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F G : C ⥤ₗ D} (α : F ⟶ G) (A : CategoryTheory.Grp C) : (CategoryTheory.Functor.mapGrpFunctor.map α).app A = CategoryTheory.Grp.homMk'' (α.hom.app A.X) ⋯ ⋯
• CategoryTheory.ObjectProperty.fullMonoidalSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : CategoryTheory.MonoidalCategory P.FullSubcategory
• CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : CategoryTheory.MonoidalCategoryStruct P.FullSubcategory
• CategoryTheory.ObjectProperty.fullBraidedSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory P.FullSubcategory
• CategoryTheory.ObjectProperty.fullSymmetricSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory P.FullSubcategory
• CategoryTheory.ObjectProperty.monoidalι 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : P.ι.Monoidal
• CategoryTheory.ObjectProperty.fullMonoidalClosedSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.MonoidalClosed C] [P.IsMonoidalClosed] : CategoryTheory.MonoidalClosed P.FullSubcategory
• CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.MonoidalPreadditive P.FullSubcategory
• CategoryTheory.ObjectProperty.tensorUnit_obj 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory).obj = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
• CategoryTheory.ObjectProperty.instBraidedFullSubcategoryι 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.BraidedCategory C] : P.ι.Braided
• CategoryTheory.ObjectProperty.tensorObj_obj 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X Y : P.FullSubcategory) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj
• CategoryTheory.ObjectProperty.instMonoidalFullSubcategoryιOfLE 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).Monoidal
• CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] : CategoryTheory.MonoidalLinear R P.FullSubcategory
• CategoryTheory.ObjectProperty.instBraidedFullSubcategoryιOfLE 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsMonoidal] [CategoryTheory.BraidedCategory C] {P' : CategoryTheory.ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).Braided
• CategoryTheory.ObjectProperty.ihom_obj 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.MonoidalClosed C] [P.IsMonoidalClosed] (X Y : P.FullSubcategory) : (X ⟹ Y).obj = (X.obj ⟹ Y.obj)
• CategoryTheory.ObjectProperty.ι_ε 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : CategoryTheory.Functor.LaxMonoidal.ε P.ι = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• CategoryTheory.ObjectProperty.ι_η 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : CategoryTheory.Functor.LaxMonoidal.ε P.ι = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• CategoryTheory.ObjectProperty.leftUnitor_def 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X : P.FullSubcategory) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = P.isoMk (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.obj)
• CategoryTheory.ObjectProperty.rightUnitor_def 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X : P.FullSubcategory) : CategoryTheory.MonoidalCategoryStruct.rightUnitor X = P.isoMk (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj)
• CategoryTheory.ObjectProperty.ι_μ 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X Y : P.FullSubcategory) : CategoryTheory.Functor.LaxMonoidal.μ P.ι X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (P.ι.obj X) (P.ι.obj Y))
• CategoryTheory.ObjectProperty.ι_δ 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X Y : P.FullSubcategory) : CategoryTheory.Functor.OplaxMonoidal.δ P.ι X Y = CategoryTheory.CategoryStruct.id (P.ι.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• CategoryTheory.ObjectProperty.whiskerLeft_def 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X x✝ x✝¹ : P.FullSubcategory) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.obj f.hom)
• CategoryTheory.ObjectProperty.whiskerRight_def 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] {X₁✝ X₂✝ : P.FullSubcategory} (f : X₁✝ ⟶ X₂✝) (Y : P.FullSubcategory) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.obj)
• CategoryTheory.ObjectProperty.ιOfLE_ε 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P') : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.ObjectProperty.ιOfLE h) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit P'.FullSubcategory)
• CategoryTheory.ObjectProperty.ιOfLE_η 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P') : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.ObjectProperty.ιOfLE h) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ObjectProperty.ιOfLE h).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory))
• CategoryTheory.ObjectProperty.tensorHom_def 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] {X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom)
• CategoryTheory.ObjectProperty.associator_def 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] (X Y Z : P.FullSubcategory) : CategoryTheory.MonoidalCategoryStruct.associator X Y Z = P.isoMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj)
• CategoryTheory.ObjectProperty.ιOfLE_δ 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P') (X Y : P.FullSubcategory) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.ObjectProperty.ιOfLE h) X Y = CategoryTheory.CategoryStruct.id ((CategoryTheory.ObjectProperty.ιOfLE h).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• CategoryTheory.ObjectProperty.ιOfLE_μ 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P') (X Y : P.FullSubcategory) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.ObjectProperty.ιOfLE h) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.ObjectProperty.ιOfLE h).obj X) ((CategoryTheory.ObjectProperty.ιOfLE h).obj Y))
• CategoryTheory.ObjectProperty.ihom_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.MonoidalClosed C] [P.IsMonoidalClosed] (X : P.FullSubcategory) {Y Z : P.FullSubcategory} (f : Y ⟶ Z) : ((CategoryTheory.ihom X).map f).hom = (CategoryTheory.ihom X.obj).map f.hom
• FGModuleCat.hom_hom_id 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [Ring R] (A : FGModuleCat R) : ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id A).hom = LinearMap.id

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