Loogle!

Result

Found 791 declarations mentioning CategoryTheory.InducedCategory.Hom.hom. Of these, only the first 200 are shown.

CategoryTheory.InducedCategory.Hom.hom 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (self : X.Hom Y) : F X ⟶ F Y
CategoryTheory.InducedCategory.id_hom 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} (X : CategoryTheory.InducedCategory D F) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)
CategoryTheory.InducedCategory.homMk_hom 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (f : F X ⟶ F Y) : (CategoryTheory.InducedCategory.homMk f).hom = f
CategoryTheory.InducedCategory.Hom.ext 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v, u₂} D} {F : C → D} {X Y : CategoryTheory.InducedCategory D F} {x y : X.Hom Y} (hom : x.hom = y.hom) : x = y
CategoryTheory.InducedCategory.Hom.ext_iff 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v, u₂} D} {F : C → D} {X Y : CategoryTheory.InducedCategory D F} {x y : X.Hom Y} : x = y ↔ x.hom = y.hom
CategoryTheory.inducedFunctor_map 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) {X✝ Y✝ : CategoryTheory.InducedCategory D F} (f : X✝ ⟶ Y✝) : (CategoryTheory.inducedFunctor F).map f = f.hom
CategoryTheory.InducedCategory.comp_hom 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X✝ Y✝ Z✝ : CategoryTheory.InducedCategory D F} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.InducedCategory.hom_ext 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g
CategoryTheory.InducedCategory.hom_ext_iff 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom
CategoryTheory.InducedCategory.comp_hom_assoc 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X✝ Y✝ Z✝ : CategoryTheory.InducedCategory D F} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : D} (h : F Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
CategoryTheory.InducedCategory.homEquiv_apply 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y) : CategoryTheory.InducedCategory.homEquiv f = f.hom
CategoryTheory.InducedCategory.homEquiv_symm_apply_hom 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (f : F X ⟶ F Y) : (CategoryTheory.InducedCategory.homEquiv.symm f).hom = f
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.ι_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.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.InducedCategory.eqToHom_hom 📋 Mathlib.CategoryTheory.EqToHom
{C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (h : X = Y) : (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
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.InducedCategory.endEquiv_apply 📋 Mathlib.CategoryTheory.Endomorphism
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C} {X : CategoryTheory.InducedCategory C F} (f : X ⟶ X) : CategoryTheory.InducedCategory.endEquiv f = f.hom
CategoryTheory.InducedCategory.endEquiv_symm_apply_hom 📋 Mathlib.CategoryTheory.Endomorphism
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C} {X : CategoryTheory.InducedCategory C F} (f : F X ⟶ F X) : (CategoryTheory.InducedCategory.endEquiv.symm f).hom = f
CategoryTheory.fromSkeleton_map 📋 Mathlib.CategoryTheory.Skeletal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : CategoryTheory.InducedCategory C Quotient.out} (f : X✝ ⟶ Y✝) : (CategoryTheory.fromSkeleton C).map f = f.hom
CategoryTheory.Skeleton.comp_hom 📋 Mathlib.CategoryTheory.Skeletal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.Skeleton C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.toSkeletonFunctor_map_hom 📋 Mathlib.CategoryTheory.Skeletal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : ((CategoryTheory.toSkeletonFunctor C).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.fromSkeletonToSkeletonIso X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.fromSkeletonToSkeletonIso Y).inv)
CategoryTheory.Skeleton.comp_hom_assoc 📋 Mathlib.CategoryTheory.Skeletal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.Skeleton C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Quotient.out Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
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.InducedCategory.homAddEquiv_apply 📋 Mathlib.CategoryTheory.Preadditive.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} {F : D → C} {X Y : CategoryTheory.InducedCategory C F} (f : X ⟶ Y) : CategoryTheory.InducedCategory.homAddEquiv f = f.hom
CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom 📋 Mathlib.CategoryTheory.Preadditive.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} {F : D → C} {X Y : CategoryTheory.InducedCategory C F} (f : F X ⟶ F Y) : (CategoryTheory.InducedCategory.homAddEquiv.symm f).hom = f
CategoryTheory.InducedCategory.homLinearEquiv_apply 📋 Mathlib.CategoryTheory.Linear.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {D : Type u'} {F : D → C} {X Y : CategoryTheory.InducedCategory C F} (a✝ : X ⟶ Y) : CategoryTheory.InducedCategory.homLinearEquiv a✝ = a✝.hom
CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom 📋 Mathlib.CategoryTheory.Linear.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {D : Type u'} {F : D → C} {X Y : CategoryTheory.InducedCategory C F} (a✝ : F X ⟶ F Y) : (CategoryTheory.InducedCategory.homLinearEquiv.symm a✝).hom = a✝
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.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.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.LaxBraidedFunctor.id_hom 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) : (CategoryTheory.CategoryStruct.id F).hom.hom = CategoryTheory.CategoryStruct.id F.toLaxMonoidalFunctor.toFunctor
CategoryTheory.LaxBraidedFunctor.homMk_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G : CategoryTheory.LaxBraidedFunctor C D} (f : F.toFunctor ⟶ G.toFunctor) [CategoryTheory.NatTrans.IsMonoidal f] : (CategoryTheory.LaxBraidedFunctor.homMk f).hom.hom = f
CategoryTheory.LaxBraidedFunctor.forget_map 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {X✝ Y✝ : CategoryTheory.InducedCategory (CategoryTheory.LaxMonoidalFunctor C D) CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor} (f : X✝ ⟶ Y✝) : CategoryTheory.LaxBraidedFunctor.forget.map f = f.hom
CategoryTheory.LaxBraidedFunctor.hom_ext 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G : CategoryTheory.LaxBraidedFunctor C D} {α β : F ⟶ G} (h : α.hom.hom = β.hom.hom) : α = β
CategoryTheory.LaxBraidedFunctor.hom_ext_iff 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G : CategoryTheory.LaxBraidedFunctor C D} {α β : F ⟶ G} : α = β ↔ α.hom.hom = β.hom.hom
CategoryTheory.LaxBraidedFunctor.comp_hom 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G H : CategoryTheory.LaxBraidedFunctor C D} (α : F ⟶ G) (β : G ⟶ H) : (CategoryTheory.CategoryStruct.comp α β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
CategoryTheory.LaxBraidedFunctor.comp_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G H : CategoryTheory.LaxBraidedFunctor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : CategoryTheory.LaxMonoidalFunctor C D} (h : H.toLaxMonoidalFunctor ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β).hom h = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp β.hom h)
CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by cat_disch) (unit : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by cat_disch) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y) (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by cat_disch) (X : C) : (CategoryTheory.LaxBraidedFunctor.isoOfComponents e ⋯ unit tensor).hom.hom.hom.app X = (e X).hom
CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Braided.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by cat_disch) (unit : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by cat_disch) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y) (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by cat_disch) (X : C) : (CategoryTheory.LaxBraidedFunctor.isoOfComponents e ⋯ unit tensor).inv.hom.hom.app X = (e X).inv
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.AddGrp.id_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.AddGrp C) : (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.Grp.id_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.AddGrp.instIsIsoHomHomMon 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.AddGrp C} {f : G ⟶ H} [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom.hom
CategoryTheory.Grp.instIsIsoHomHomMon 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.Grp C} {f : G ⟶ H} [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom.hom
CategoryTheory.AddGrp.ofHom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj A] [CategoryTheory.AddGrpObj B] (f : A ⟶ B) [CategoryTheory.IsAddMonHom f] : (CategoryTheory.AddGrp.ofHom f).hom.hom = f
CategoryTheory.Grp.ofHom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.GrpObj A] [CategoryTheory.GrpObj B] (f : A ⟶ B) [CategoryTheory.IsMonHom f] : (CategoryTheory.Grp.ofHom f).hom.hom = f
CategoryTheory.AddGrp.id' 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.AddGrp C) : (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.toAddMon
CategoryTheory.Grp.id' 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.toMon
CategoryTheory.AddGrp.homMk_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X) [CategoryTheory.IsAddMonHom f] : (CategoryTheory.AddGrp.homMk f).hom.hom = f
CategoryTheory.Grp.homMk_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.Grp C} (f : A.X ⟶ B.X) [CategoryTheory.IsMonHom f] : (CategoryTheory.Grp.homMk f).hom.hom = f
CategoryTheory.AddGrp.homMk'_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f : A.toAddMon ⟶ B.toAddMon) : (CategoryTheory.AddGrp.homMk' f).hom = f
CategoryTheory.Grp.homMk'_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.Grp C} (f : A.toMon ⟶ B.toMon) : (CategoryTheory.Grp.homMk' f).hom = f
CategoryTheory.AddGrp.hom_ext 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f g : A ⟶ B) (h : f.hom.hom = g.hom.hom) : f = g
CategoryTheory.Grp.hom_ext 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.Grp C} (f g : A ⟶ B) (h : f.hom.hom = g.hom.hom) : f = g
CategoryTheory.AddGrp.hom_ext_iff 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} {f g : A ⟶ B} : f = g ↔ f.hom.hom = g.hom.hom
CategoryTheory.Grp.hom_ext_iff 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.Grp C} {f g : A ⟶ B} : f = g ↔ f.hom.hom = g.hom.hom
CategoryTheory.AddGrp.forget_map 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X✝ Y✝ : CategoryTheory.AddGrp C} (f : X✝ ⟶ Y✝) : (CategoryTheory.AddGrp.forget C).map f = f.hom.hom
CategoryTheory.AddGrp.mkIso'_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [CategoryTheory.AddGrpObj G] [CategoryTheory.AddGrpObj H] [CategoryTheory.IsAddMonHom e.hom] : (CategoryTheory.AddGrp.mkIso' e).hom.hom.hom = e.hom
CategoryTheory.AddGrp.mkIso'_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [CategoryTheory.AddGrpObj G] [CategoryTheory.AddGrpObj H] [CategoryTheory.IsAddMonHom e.hom] : (CategoryTheory.AddGrp.mkIso' e).inv.hom.hom = e.inv
CategoryTheory.Grp.forget_map 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X✝ Y✝ : CategoryTheory.Grp C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grp.forget C).map f = f.hom.hom
CategoryTheory.Grp.mkIso'_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] [CategoryTheory.IsMonHom e.hom] : (CategoryTheory.Grp.mkIso' e).hom.hom.hom = e.hom
CategoryTheory.Grp.mkIso'_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] [CategoryTheory.IsMonHom e.hom] : (CategoryTheory.Grp.mkIso' e).inv.hom.hom = e.inv
CategoryTheory.AddGrp.comp' 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A₁ A₂ A₃ : CategoryTheory.AddGrp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.Grp.comp' 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A₁ A₂ A₃ : CategoryTheory.Grp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.AddGrp.zero_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (G H : CategoryTheory.AddGrp C) : CategoryTheory.InducedCategory.Hom.hom 0 = 0
CategoryTheory.Grp.zero_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (G H : CategoryTheory.Grp C) : CategoryTheory.InducedCategory.Hom.hom 0 = 0
CategoryTheory.AddGrp.fst_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C) : (CategoryTheory.SemiCartesianMonoidalCategory.fst G H).hom.hom = CategoryTheory.SemiCartesianMonoidalCategory.fst G.X H.X
CategoryTheory.AddGrp.snd_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C) : (CategoryTheory.SemiCartesianMonoidalCategory.snd G H).hom.hom = CategoryTheory.SemiCartesianMonoidalCategory.snd G.X H.X
CategoryTheory.Grp.fst_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C) : (CategoryTheory.SemiCartesianMonoidalCategory.fst G H).hom.hom = CategoryTheory.SemiCartesianMonoidalCategory.fst G.X H.X
CategoryTheory.Grp.snd_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C) : (CategoryTheory.SemiCartesianMonoidalCategory.snd G H).hom.hom = CategoryTheory.SemiCartesianMonoidalCategory.snd G.X H.X
CategoryTheory.AddGrp.forget₂AddMon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f : A ⟶ B) : ((CategoryTheory.AddGrp.forget₂Mon C).map f).hom = f.hom.hom
CategoryTheory.Grp.forget₂Mon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.Grp C} (f : A ⟶ B) : ((CategoryTheory.Grp.forget₂Mon C).map f).hom = f.hom.hom
CategoryTheory.AddGrp.leftUnitor_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).hom.hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).hom
CategoryTheory.AddGrp.leftUnitor_neg_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).inv.hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).inv
CategoryTheory.AddGrp.rightUnitor_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).hom.hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).hom
CategoryTheory.AddGrp.rightUnitor_neg_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).inv.hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).inv
CategoryTheory.Grp.leftUnitor_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).hom.hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).hom
CategoryTheory.Grp.leftUnitor_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).inv.hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).inv
CategoryTheory.Grp.rightUnitor_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).hom.hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).hom
CategoryTheory.Grp.rightUnitor_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).inv.hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).inv
CategoryTheory.AddGrp.comp_hom_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {R S T : CategoryTheory.AddGrp C} (f : R ⟶ S) (g : S ⟶ T) {Z : C} (h : T.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom.hom h = CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp g.hom.hom h)
CategoryTheory.Grp.comp_hom_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {R S T : CategoryTheory.Grp C} (f : R ⟶ S) (g : S ⟶ T) {Z : C} (h : T.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom.hom h = CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp g.hom.hom h)
CategoryTheory.AddGrp.comp_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {R S T : CategoryTheory.AddGrp C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom
CategoryTheory.Grp.comp_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {R S T : CategoryTheory.Grp C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom
CategoryTheory.AddGrp.whiskerLeft_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C} (f : G ⟶ H) (I : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I).hom.hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom.hom I.X
CategoryTheory.AddGrp.whiskerRight_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C) {H I : CategoryTheory.AddGrp C} (f : H ⟶ I) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f).hom.hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.X f.hom.hom
CategoryTheory.Grp.whiskerLeft_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} (f : G ⟶ H) (I : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I).hom.hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom.hom I.X
CategoryTheory.Grp.whiskerRight_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C) {H I : CategoryTheory.Grp C} (f : H ⟶ I) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f).hom.hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.X f.hom.hom
CategoryTheory.AddGrp.lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H₁ H₂ : CategoryTheory.AddGrp C} (f : G ⟶ H₁) (g : G ⟶ H₂) : (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
CategoryTheory.Grp.lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H₁ H₂ : CategoryTheory.Grp C} (f : G ⟶ H₁) (g : G ⟶ H₂) : (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
CategoryTheory.AddGrp.braiding_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C) : (β_ G H).hom.hom.hom = (β_ G.X H.X).hom
CategoryTheory.AddGrp.braiding_neg_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C) : (β_ G H).inv.hom.hom = (β_ G.X H.X).inv
CategoryTheory.Grp.braiding_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C) : (β_ G H).hom.hom.hom = (β_ G.X H.X).hom
CategoryTheory.Grp.braiding_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C) : (β_ G H).inv.hom.hom = (β_ G.X H.X).inv
CategoryTheory.AddGrp.comp'_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A₁ A₂ A₃ : CategoryTheory.AddGrp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) {Z : CategoryTheory.AddMon C} (h : A₃.toAddMon ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
CategoryTheory.Grp.comp'_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A₁ A₂ A₃ : CategoryTheory.Grp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) {Z : CategoryTheory.Mon C} (h : A₃.toMon ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
CategoryTheory.AddGrp.homMk''_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.AddMonObj.add := by cat_disch) : (CategoryTheory.AddGrp.homMk'' f zero_f add_f).hom.hom = f
CategoryTheory.Grp.homMk''_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.Grp C} (f : A.X ⟶ B.X) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul := by cat_disch) : (CategoryTheory.Grp.homMk'' f one_f mul_f).hom.hom = f
CategoryTheory.Functor.mapAddGrpNatTrans_app_hom_hom 📋 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 F' : CategoryTheory.Functor C D} [F.Monoidal] [F'.Monoidal] (f : F ⟶ F') (X : CategoryTheory.AddGrp C) : ((CategoryTheory.Functor.mapAddGrpNatTrans f).app X).hom.hom = f.app X.X
CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom 📋 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 F' : CategoryTheory.Functor C D} [F.Monoidal] [F'.Monoidal] (f : F ⟶ F') (X : CategoryTheory.Grp C) : ((CategoryTheory.Functor.mapGrpNatTrans f).app X).hom.hom = f.app X.X
CategoryTheory.AddGrp.tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.AddGrp C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
CategoryTheory.Grp.tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.Grp C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
CategoryTheory.Functor.mapAddGrp_map_hom_hom 📋 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 : CategoryTheory.Functor C D) [F.Monoidal] {X✝ Y✝ : CategoryTheory.AddGrp C} (f : X✝ ⟶ Y✝) : (F.mapAddGrp.map f).hom.hom = F.map f.hom.hom
CategoryTheory.Functor.mapGrp_map_hom_hom 📋 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 : CategoryTheory.Functor C D) [F.Monoidal] {X✝ Y✝ : CategoryTheory.Grp C} (f : X✝ ⟶ Y✝) : (F.mapGrp.map f).hom.hom = F.map f.hom.hom
CategoryTheory.AddGrp.associator_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.associator G H I).hom.hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).hom
CategoryTheory.AddGrp.associator_neg_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.AddGrp C) : (CategoryTheory.MonoidalCategoryStruct.associator G H I).inv.hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).inv
CategoryTheory.Grp.associator_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.associator G H I).hom.hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).hom
CategoryTheory.Grp.associator_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.Grp C) : (CategoryTheory.MonoidalCategoryStruct.associator G H I).inv.hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).inv
CategoryTheory.Functor.mapAddGrpIdIso_hom_app_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : CategoryTheory.AddGrp C) : (CategoryTheory.Functor.mapAddGrpIdIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Functor.mapAddGrpIdIso_inv_app_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : CategoryTheory.AddGrp C) : (CategoryTheory.Functor.mapAddGrpIdIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : CategoryTheory.Grp C) : (CategoryTheory.Functor.mapGrpIdIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : CategoryTheory.Grp C) : (CategoryTheory.Functor.mapGrpIdIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Functor.mapAddGrpNatIso_hom_app_hom_hom 📋 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 F' : CategoryTheory.Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : CategoryTheory.AddGrp C) : ((CategoryTheory.Functor.mapAddGrpNatIso e).hom.app X).hom.hom = e.hom.app X.X
CategoryTheory.Functor.mapAddGrpNatIso_inv_app_hom_hom 📋 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 F' : CategoryTheory.Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : CategoryTheory.AddGrp C) : ((CategoryTheory.Functor.mapAddGrpNatIso e).inv.app X).hom.hom = e.inv.app X.X
CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom 📋 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 F' : CategoryTheory.Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : CategoryTheory.Grp C) : ((CategoryTheory.Functor.mapGrpNatIso e).hom.app X).hom.hom = e.hom.app X.X
CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom 📋 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 F' : CategoryTheory.Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : CategoryTheory.Grp C) : ((CategoryTheory.Functor.mapGrpNatIso e).inv.app X).hom.hom = e.inv.app X.X
CategoryTheory.AddGrp.mkIso_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.AddMonObj.add := by cat_disch) : (CategoryTheory.AddGrp.mkIso e zero_f add_f).hom.hom.hom = e.hom
CategoryTheory.AddGrp.mkIso_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.AddMonObj.add := by cat_disch) : (CategoryTheory.AddGrp.mkIso e zero_f add_f).inv.hom.hom = e.inv
CategoryTheory.Grp.mkIso_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.Grp C} (e : G.X ≅ H.X) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.MonObj.mul := by cat_disch) : (CategoryTheory.Grp.mkIso e one_f mul_f).hom.hom.hom = e.hom
CategoryTheory.Grp.mkIso_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.Grp C} (e : G.X ≅ H.X) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.MonObj.mul := by cat_disch) : (CategoryTheory.Grp.mkIso e one_f mul_f).inv.hom.hom = e.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.Functor.mapAddGrpCompIso_hom_app_hom_hom 📋 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] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.Monoidal] [G.Monoidal] (X : CategoryTheory.AddGrp C) : (CategoryTheory.Functor.mapAddGrpCompIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Functor.mapAddGrpCompIso_inv_app_hom_hom 📋 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] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.Monoidal] [G.Monoidal] (X : CategoryTheory.AddGrp C) : (CategoryTheory.Functor.mapAddGrpCompIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom 📋 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] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.Monoidal] [G.Monoidal] (X : CategoryTheory.Grp C) : (CategoryTheory.Functor.mapGrpCompIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom 📋 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] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.Monoidal] [G.Monoidal] (X : CategoryTheory.Grp C) : (CategoryTheory.Functor.mapGrpCompIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
commHopfAlgCatEquivCogrpCommAlgCat_unitIso_hom_app 📋 Mathlib.Algebra.Category.CommHopfAlgCat
(R : Type u) [CommRing R] (X : CommHopfAlgCat R) : (commHopfAlgCatEquivCogrpCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
commHopfAlgCatEquivCogrpCommAlgCat_counitIso_inv_app 📋 Mathlib.Algebra.Category.CommHopfAlgCat
(R : Type u) [CommRing R] (X : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commHopfAlgCatEquivCogrpCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
commHopfAlgCatEquivCogrpCommAlgCat_unitIso_inv_app 📋 Mathlib.Algebra.Category.CommHopfAlgCat
(R : Type u) [CommRing R] (X : CommHopfAlgCat R) : (commHopfAlgCatEquivCogrpCommAlgCat R).unitIso.inv.app X = CategoryTheory.CategoryStruct.id { X := ↑X, commRing := CommAlgCat.instCommRingObjForgetAlgHomCarrier, hopfAlgebra := instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite (Opposite.unop (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑X), grp := CommAlgCat.grpObjOpOf })).X }
commHopfAlgCatEquivCogrpCommAlgCat_counitIso_hom_app 📋 Mathlib.Algebra.Category.CommHopfAlgCat
(R : Type u) [CommRing R] (X : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commHopfAlgCatEquivCogrpCommAlgCat R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), grp := CommAlgCat.grpObjOpOf })
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.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
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.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.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
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.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.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.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_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

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision 69fae59