Loogle!

Result

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

• 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.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.ι_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.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.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.ι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.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.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.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.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.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.toEssImage_obj_obj 📋 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.toEssImage.obj X).obj = F.obj X
• 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.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.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.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.instPreservesFiniteColimitsObjFunctorExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : CategoryTheory.Limits.PreservesFiniteColimits F.obj
• CategoryTheory.instPreservesFiniteColimitsObjFunctorRightExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ᵣ D) : CategoryTheory.Limits.PreservesFiniteColimits F.obj
• CategoryTheory.instPreservesFiniteLimitsObjFunctorExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : CategoryTheory.Limits.PreservesFiniteLimits F.obj
• CategoryTheory.instPreservesFiniteLimitsObjFunctorLeftExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₗ D) : CategoryTheory.Limits.PreservesFiniteLimits F.obj
• CategoryTheory.LeftExactFunctor.of_fst 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : (CategoryTheory.LeftExactFunctor.of F).obj = F
• CategoryTheory.RightExactFunctor.of_fst 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.RightExactFunctor.of F).obj = F
• CategoryTheory.ExactFunctor.of_fst 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.ExactFunctor.of F).obj = F
• CategoryTheory.ExactFunctor.forget_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : (CategoryTheory.ExactFunctor.forget C D).obj F = F.obj
• CategoryTheory.LeftExactFunctor.forget_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₗ D) : (CategoryTheory.LeftExactFunctor.forget C D).obj F = F.obj
• CategoryTheory.RightExactFunctor.forget_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ᵣ D) : (CategoryTheory.RightExactFunctor.forget C D).obj F = F.obj
• CategoryTheory.LeftExactFunctor.ofExact_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : (CategoryTheory.LeftExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }
• CategoryTheory.RightExactFunctor.ofExact_obj 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : (CategoryTheory.RightExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }
• 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.instAdditiveObjFunctorAdditiveFunctor 📋 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 : C ⥤+ D) : F.obj.Additive
• CategoryTheory.instAdditiveObjFunctorAdditiveFunctor_1 📋 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 : C ⥤+ D) : F.obj.Additive
• CategoryTheory.AdditiveFunctor.of_fst 📋 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 C D) [F.Additive] : (CategoryTheory.AdditiveFunctor.of F).obj = F
• CategoryTheory.AdditiveFunctor.of_obj 📋 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 C D) [F.Additive] : (CategoryTheory.AdditiveFunctor.of F).obj = F
• CategoryTheory.AdditiveFunctor.forget_obj 📋 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 : C ⥤+ D) : (CategoryTheory.AdditiveFunctor.forget C D).obj F = F.obj
• CategoryTheory.AdditiveFunctor.ofExact_obj_fst 📋 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 : C ⥤ₑ D) : ((CategoryTheory.AdditiveFunctor.ofExact C D).obj F).obj = F.obj
• CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst 📋 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 : C ⥤ₗ D) : ((CategoryTheory.AdditiveFunctor.ofLeftExact C D).obj F).obj = F.obj
• CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst 📋 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 : C ⥤ᵣ D) : ((CategoryTheory.AdditiveFunctor.ofRightExact C D).obj F).obj = F.obj
• 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
• instFiniteTypeCarrierObjCommAlgCat 📋 Mathlib.Algebra.Category.CommAlgCat.FiniteType
  (R : Type u) [CommRing R] (A : FGAlgCat R) : Algebra.FiniteType R ↑A.obj
• Algebra.FiniteType.exists_fgAlgCatSkeleton 📋 Mathlib.Algebra.Category.CommAlgCat.FiniteType
  (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A] [h : Algebra.FiniteType R A] : ∃ P, Nonempty (A ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R P).obj)
• RingHom.FiniteType.exists_smallRepr 📋 Mathlib.Algebra.Category.CommAlgCat.FiniteType
  (R : Type u) [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} (hf : f.FiniteType) : ∃ T e, f = e.toRingHom.comp (algebraMap R ↑(FGAlgCatSkeleton.eval R T).obj)
• 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.Functor.EssImageSubcategory.tensor_obj 📋 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] (X Y : F.EssImageSubcategory) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = CategoryTheory.MonoidalCategoryStruct.tensorObj 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.toUnit_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] (X : F.EssImageSubcategory) : CategoryTheory.SemiCartesianMonoidalCategory.toUnit X = CategoryTheory.ObjectProperty.homMk (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X.obj)
• 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.EssImageSubcategory.associator_hom_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] (X Y Z : F.EssImageSubcategory) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom
• CategoryTheory.Functor.EssImageSubcategory.associator_inv_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] (X Y Z : F.EssImageSubcategory) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv
• CategoryTheory.Functor.mapAddGrpFunctor_obj 📋 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 : C ⥤ₗ D) : CategoryTheory.Functor.mapAddGrpFunctor.obj F = F.obj.mapAddGrp
• CategoryTheory.Functor.mapGrpFunctor_obj 📋 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 : C ⥤ₗ D) : CategoryTheory.Functor.mapGrpFunctor.obj F = F.obj.mapGrp
• 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.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.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.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.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.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.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.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.obj_carrier 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] (M : FGModuleCat R) : ↑M.obj = ↑M
• instFiniteCarrier 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] (M : FGModuleCat R) : Module.Finite R ↑M
• FGModuleCat.instFiniteCarrier 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [Ring R] (V : FGModuleCat R) : Module.Finite R ↑V
• FGModuleCat.tensorUnit_obj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat R)).obj = CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)
• FGModuleCat.FGModuleCatDual_coe 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V : FGModuleCat K) : ↑(FGModuleCat.FGModuleCatDual K V) = Module.Dual K ↑V
• FGModuleCat.tensorObj_obj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] (M N : FGModuleCat R) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).obj = CategoryTheory.MonoidalCategoryStruct.tensorObj M.obj N.obj
• FGModuleCat.isoToLinearEquiv 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] {V W : FGModuleCat R} (i : V ≅ W) : ↑V ≃ₗ[R] ↑W
• 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
• FGModuleCat.hom_ext 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] {V W : FGModuleCat R} {f g : V ⟶ W} (h : ModuleCat.Hom.hom f.hom = ModuleCat.Hom.hom g.hom) : f = g
• FGModuleCat.hom_ext_iff 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] {V W : FGModuleCat R} {f g : V ⟶ W} : f = g ↔ ModuleCat.Hom.hom f.hom = ModuleCat.Hom.hom g.hom
• LinearMap.comp_id_fgModuleCat 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u_1} [Ring R] {G : FGModuleCat R} {H : Type v} [AddCommGroup H] [Module R H] (f : ↑G →ₗ[R] H) : f ∘ₗ ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id G).hom = f
• LinearMap.id_fgModuleCat_comp 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u_1} [Ring R] {G : Type v} [AddCommGroup G] [Module R G] {H : FGModuleCat R} (f : G →ₗ[R] ↑H) : ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id H).hom ∘ₗ f = f
• FGModuleCat.FGModuleCatDual_obj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V : FGModuleCat K) : (FGModuleCat.FGModuleCatDual K V).obj = ModuleCat.of K (Module.Dual K ↑V)
• FGModuleCat.hom_hom_comp 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [Ring R] {A B C : FGModuleCat R} (f : A ⟶ B) (g : B ⟶ C) : ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = ModuleCat.Hom.hom g.hom ∘ₗ ModuleCat.Hom.hom f.hom
• FGModuleCat.instFiniteHomModuleCatObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V W : FGModuleCat K) : Module.Finite K (V.obj ⟶ W.obj)
• LinearEquiv.toFGModuleCatIso_hom 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) : e.toFGModuleCatIso.hom = CategoryTheory.ConcreteCategory.ofHom ↑e
• LinearEquiv.toFGModuleCatIso_inv 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  {R : Type u} [Ring R] {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) : e.toFGModuleCatIso.inv = CategoryTheory.ConcreteCategory.ofHom ↑e.symm
• FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [Ring R] : (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).Full
• FGModuleCat.ihom_obj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V W : FGModuleCat K) : (V ⟹ W) = FGModuleCat.of K (V.obj ⟶ W.obj)
• FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] : (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).Additive
• FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] : CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R))
• FGModuleCat.FGModuleCatEvaluation_apply 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V) : (CategoryTheory.ConcreteCategory.hom (FGModuleCat.FGModuleCatEvaluation K V).hom) (f ⊗ₜ[K] x) = f.toFun x
• FGModuleCat.FGModuleCatCoevaluation_apply_one 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V : FGModuleCat K) : (CategoryTheory.ConcreteCategory.hom (FGModuleCat.FGModuleCatCoevaluation K V).hom) 1 = ∑ i, (Module.Basis.ofVectorSpace K ↑V) i ⊗ₜ[K] (Module.Basis.ofVectorSpace K ↑V).coord i
• FGModuleCat.Iso.conj_eq_conj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] {V W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V) : i.conj f = FGModuleCat.ofHom ((FGModuleCat.isoToLinearEquiv i).conj (ModuleCat.Hom.hom f.hom))
• FGModuleCat.Iso.conj_hom_eq_conj 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (R : Type u) [CommRing R] {V W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V) : ModuleCat.Hom.hom (i.conj f).hom = (FGModuleCat.isoToLinearEquiv i).conj (ModuleCat.Hom.hom f.hom)
• FGModuleCat.FGModuleCatEvaluation_apply' 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V) : (ModuleCat.Hom.hom (FGModuleCat.FGModuleCatEvaluation K V).hom) (f ⊗ₜ[K] x) = f.toFun x
• FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Colimits
  {k : Type u} [Ring k] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• FGModuleCat.instCreatesColimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Colimits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• FGModuleCat.forget₂CreatesColimit 📋 Mathlib.Algebra.Category.FGModuleCat.Colimits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] (F : CategoryTheory.Functor J (FGModuleCat k)) : CategoryTheory.CreatesColimit F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Colimits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] (F : CategoryTheory.Functor J (FGModuleCat k)) : Module.Finite k ↑(CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
• FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {k : Type u} [Ring k] [IsNoetherianRing k] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• FGModuleCat.instCreatesLimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] [IsNoetherianRing k] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• FGModuleCat.forget₂CreatesLimit 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] [IsNoetherianRing k] (F : CategoryTheory.Functor J (FGModuleCat k)) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] [IsNoetherianRing k] (F : CategoryTheory.Functor J (FGModuleCat k)) : Module.Finite k ↑(CategoryTheory.Limits.limit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
• CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : i.EssImageSubcategory) : CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)
• CategoryTheory.equivEssImageOfReflective_counitIso 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.counitIso = CategoryTheory.Functor.fullyFaithfulCancelRight i.essImage.ι (CategoryTheory.NatIso.ofComponents (fun X => (CategoryTheory.asIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)).symm) ⋯)
• CategoryTheory.MonoOver.arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X) : f.obj.left ⟶ X
• CategoryTheory.MonoOver.mono 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X) : CategoryTheory.Mono f.arrow
• CategoryTheory.MonoOver.mk_coe 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [CategoryTheory.Mono f] : (CategoryTheory.MonoOver.mk f).obj.left = A
• CategoryTheory.MonoOver.mono_obj_hom 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.MonoOver X) : CategoryTheory.Mono S.obj.hom
• CategoryTheory.MonoOver.mk_obj 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [hf : CategoryTheory.Mono f] : (CategoryTheory.MonoOver.mk f).obj = CategoryTheory.Over.mk f
• CategoryTheory.MonoOver.mkArrowIso 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X) : CategoryTheory.MonoOver.mk f.arrow ≅ f
• CategoryTheory.MonoOver.forget_obj_left 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f : CategoryTheory.MonoOver X} : ((CategoryTheory.MonoOver.forget X).obj f).left = f.obj.left
• CategoryTheory.MonoOver.mk_arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [CategoryTheory.Mono f] : (CategoryTheory.MonoOver.mk f).arrow = f
• CategoryTheory.MonoOver.imageMonoOver_arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : (CategoryTheory.MonoOver.imageMonoOver f).arrow = CategoryTheory.Limits.image.ι f
• CategoryTheory.MonoOver.map_obj_left 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (g : CategoryTheory.MonoOver X) : ((CategoryTheory.MonoOver.map f).obj g).obj.left = g.obj.left
• CategoryTheory.MonoOver.pullback_obj_left 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : CategoryTheory.MonoOver Y) : ((CategoryTheory.MonoOver.pullback f).obj g).obj.left = CategoryTheory.Limits.pullback g.arrow f
• CategoryTheory.MonoOver.homMk 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (h : f.obj.left ⟶ g.obj.left) (w : CategoryTheory.CategoryStruct.comp h g.arrow = f.arrow := by aesop_cat) : f ⟶ g
• CategoryTheory.MonoOver.map_obj_arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (g : CategoryTheory.MonoOver X) : ((CategoryTheory.MonoOver.map f).obj g).arrow = CategoryTheory.CategoryStruct.comp g.arrow f
• CategoryTheory.MonoOver.instIsIsoLeftHomFullSubcategoryOverIsMono 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {A B : CategoryTheory.MonoOver X} (f : A ⟶ B) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom)
• CategoryTheory.MonoOver.isIso_iff_isIso_hom_left 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {A B : CategoryTheory.MonoOver X} (f : A ⟶ B) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom)
• CategoryTheory.MonoOver.pullbackObjIsoOfIsPullback 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : Y ⟶ X) (S : CategoryTheory.MonoOver X) (T : CategoryTheory.MonoOver Y) (f' : T.obj.left ⟶ S.obj.left) (h : CategoryTheory.IsPullback f' T.arrow S.arrow f) : (CategoryTheory.MonoOver.pullback f).obj S ≅ T
• CategoryTheory.MonoOver.w 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (k : f ⟶ g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k.hom) g.arrow = f.arrow
• CategoryTheory.MonoOver.isoMk 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (h : f.obj.left ≅ g.obj.left) (w : CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow := by cat_disch) : f ≅ g
• CategoryTheory.MonoOver.lift_obj_obj 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : D} (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)) (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) (X✝ : CategoryTheory.MonoOver Y) : ((CategoryTheory.MonoOver.lift F h).obj X✝).obj = F.obj X✝.obj
• CategoryTheory.MonoOver.w_assoc 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (k : f ⟶ g) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k.hom) (CategoryTheory.CategoryStruct.comp g.arrow h) = CategoryTheory.CategoryStruct.comp f.arrow h
• CategoryTheory.MonoOver.pullback_obj_arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : CategoryTheory.MonoOver Y) : ((CategoryTheory.MonoOver.pullback f).obj g).arrow = CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget Y).obj g).hom f
• CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) : CategoryTheory.Limits.StrongEpiMonoFactorisation (CategoryTheory.Limits.Sigma.desc fun i => (F.obj i).arrow)
• CategoryTheory.MonoOver.isoMk_hom 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (h : f.obj.left ≅ g.obj.left) (w : CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow := by cat_disch) : (CategoryTheory.MonoOver.isoMk h w).hom = CategoryTheory.MonoOver.homMk h.hom w
• CategoryTheory.MonoOver.isoMk_inv 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (h : f.obj.left ≅ g.obj.left) (w : CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow := by cat_disch) : (CategoryTheory.MonoOver.isoMk h w).inv = CategoryTheory.MonoOver.homMk h.inv ⋯
• CategoryTheory.MonoOver.mkArrowIso_hom_hom_left 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X) : f.mkArrowIso.hom.hom.left = CategoryTheory.CategoryStruct.id f.obj.left
• CategoryTheory.MonoOver.mkArrowIso_inv_hom_left 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X) : f.mkArrowIso.inv.hom.left = CategoryTheory.CategoryStruct.id f.obj.left
• CategoryTheory.MonoOver.lift_obj_arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : D} (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)) (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) (f : CategoryTheory.MonoOver Y) : ((CategoryTheory.MonoOver.lift F h).obj f).arrow = (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom
• CategoryTheory.MonoOver.lift_map_hom 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : D} (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)) (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) {X✝ Y✝ : CategoryTheory.MonoOver Y} (f : X✝ ⟶ Y✝) : ((CategoryTheory.MonoOver.lift F h).map f).hom = F.map f.hom
• CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.CommSq (CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.Over.Hom.left (c.ι.app i).hom) (CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc F).e c.pt.arrow (CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc F).m
• CategoryTheory.MonoOver.liftStructOfHasStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) (c : CategoryTheory.Limits.Cocone F) : ⋯.LiftStruct
• CategoryTheory.MonoOver.congr_unitIso 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : (CategoryTheory.MonoOver.congr X e).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.unitIso.app Y.obj.left) ⋯) ⋯
• CategoryTheory.MonoOver.congr_counitIso 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : (CategoryTheory.MonoOver.congr X e).counitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.counitIso.app Y.obj.left) ⋯) ⋯
• CategoryTheory.Subobject.representative_coe 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y : CategoryTheory.Subobject X) : (CategoryTheory.Subobject.representative.obj Y).obj.left = CategoryTheory.Subobject.underlying.obj Y
• CategoryTheory.Subobject.representative_arrow 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y : CategoryTheory.Subobject X) : (CategoryTheory.Subobject.representative.obj Y).arrow = Y.arrow
• CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {P Q : CategoryTheory.MonoOver X} (f : P ⟶ Q) : CategoryTheory.Subobject.mk P.obj.hom ≤ CategoryTheory.Subobject.mk Q.obj.hom
• CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {P Q : CategoryTheory.MonoOver X} (f : P ⟶ Q) : CategoryTheory.IsIso f ↔ CategoryTheory.Subobject.mk P.obj.hom = CategoryTheory.Subobject.mk Q.obj.hom
• CategoryTheory.MonoOver.isIso_hom_left_iff_subobjectMk_eq 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {P Q : CategoryTheory.MonoOver X} (f : P ⟶ Q) : CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom) ↔ CategoryTheory.Subobject.mk P.obj.hom = CategoryTheory.Subobject.mk Q.obj.hom
• CategoryTheory.MonoOver.factorThru 📋 Mathlib.CategoryTheory.Subobject.FactorThru
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.MonoOver Y) (f : X ⟶ Y) (h : P.Factors f) : X ⟶ P.obj.left
• CategoryTheory.MonoOver.top_left 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : ⊤.obj.left = X
• CategoryTheory.MonoOver.bot_left 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (X : C) : ⊥.obj.left = ⊥_ C
• CategoryTheory.MonoOver.botCoeIsoZero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] {B : C} : ⊥.obj.left ≅ 0

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 69fae59