Loogle!

Result

Found 325 declarations mentioning CategoryTheory.Mon.X. Of these, only the first 200 are shown.

CategoryTheory.Mon.X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : CategoryTheory.Mon C) : C
CategoryTheory.Mon.mon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : CategoryTheory.Mon C) : CategoryTheory.MonObj self.X
CategoryTheory.Mon.trivial_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Mon.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).obj x✝ = A.X
CategoryTheory.Mon.forget_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (CategoryTheory.Mon.forget C).obj A = A.X
CategoryTheory.Mon.tensorUnit_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon C)).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
CategoryTheory.Mon.Hom.hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (self : M.Hom N) : M.X ⟶ N.X
CategoryTheory.Mon.hom_injective 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} : Function.Injective CategoryTheory.Mon.Hom.hom
CategoryTheory.Mon.id_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : M.id.hom = CategoryTheory.CategoryStruct.id M.X
CategoryTheory.Mon.Hom.isMonHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (self : M.Hom N) : CategoryTheory.IsMonHom self.hom
CategoryTheory.Mon.monMonoidalStruct_tensorObj_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).X = CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X
CategoryTheory.Mon.id_hom' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
CategoryTheory.Mon.Hom.mk 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (hom : M.X ⟶ N.X) [isMonHom_hom : CategoryTheory.IsMonHom hom] : M.Hom N
CategoryTheory.Mon.instIsMonHomHom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (f : M ⟶ N) : CategoryTheory.IsMonHom f.hom
CategoryTheory.Mon.instIsIsoHom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} {f : M ⟶ N} [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom
CategoryTheory.Mon.Hom.ext 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : CategoryTheory.Mon C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y
CategoryTheory.Mon.Hom.ext_iff 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : CategoryTheory.Mon C} {x y : M.Hom N} : x = y ↔ x.hom = y.hom
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).map x✝ = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.Functor.mapMon_obj_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.Mon C) : (F.mapMon.obj A).X = F.obj A.X
CategoryTheory.Mon.forget_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Mon.forget C).map f = f.hom
CategoryTheory.Functor.essImage_mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : CategoryTheory.Mon D} : F.mapMon.essImage M ↔ F.essImage M.X
CategoryTheory.Mon.tensorUnit_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Mon.comp_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : CategoryTheory.Mon C} (f : M.Hom N) (g : N.Hom O) : (CategoryTheory.Mon.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) = CategoryTheory.MonObj.one
CategoryTheory.Mon.instIsIsoHomOfMapForget 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((CategoryTheory.Mon.forget C).map f)] : CategoryTheory.IsIso f.hom
CategoryTheory.Mon.uniqueHomFromTrivial_default_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : default.hom = CategoryTheory.MonObj.one
CategoryTheory.Mon.Hom.ext' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} {f g : M ⟶ N} (w : f.hom = g.hom) : f = g
CategoryTheory.Mon.Hom.ext'_iff 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : (((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C)).obj F).X ≅ ((CategoryTheory.Functor.id (CategoryTheory.Mon C)).obj F).X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) X Y = CategoryTheory.MonObj.mul
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.obj A).obj x✝ = A.X
CategoryTheory.Mon.comp_hom' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N K : CategoryTheory.Mon C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.functor.obj F).X = F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Mon.tensorUnit_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonObj.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.obj A).map x✝ = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) = CategoryTheory.MonObj.one
CategoryTheory.Mon.whiskerLeft_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Mon C} (f : X ⟶ Y) (Z : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z.X
CategoryTheory.Mon.whiskerRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) {Y Z : CategoryTheory.Mon C} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
CategoryTheory.Mon.forget_δ 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Mon.forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
CategoryTheory.Mon.forget_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
CategoryTheory.Mon.comp_hom'_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N K : CategoryTheory.Mon C} (f : M ⟶ N) (g : N ⟶ K) {Z : C} (h : K.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
CategoryTheory.Functor.mapMon_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
CategoryTheory.Functor.id_mapMon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
CategoryTheory.Mon.leftUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom
CategoryTheory.Mon.leftUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv
CategoryTheory.Mon.rightUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom
CategoryTheory.Mon.rightUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (x✝ x✝¹ : CategoryTheory.Discrete PUnit.{w + 1}) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) x✝ x✝¹ = CategoryTheory.MonObj.mul
CategoryTheory.Functor.mapMon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) : (F.mapMon.map f).hom = F.map f.hom
CategoryTheory.Mon.one_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
CategoryTheory.Functor.mapMonNatTrans_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [CategoryTheory.NatTrans.IsMonoidal f] (X : CategoryTheory.Mon C) : ((CategoryTheory.Functor.mapMonNatTrans f).app X).hom = f.app X.X
CategoryTheory.Mon.tensorObj_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
CategoryTheory.Mon.tensor_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
CategoryTheory.Functor.mapMon_obj_mon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X) (F.map CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapMonIdIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonIdIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Functor.mapMonIdIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonIdIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.monMonoidalStruct_tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.Mon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
CategoryTheory.Mon.mul_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
CategoryTheory.Mon.Hom.mk' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (f : M.X ⟶ N.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) : M.Hom N
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).map f).hom.app x✝ = f.hom
CategoryTheory.Functor.id_mapMon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X X.X)) CategoryTheory.MonObj.mul
CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : CategoryTheory.Mon C} (f : F.mapMon.obj X ⟶ F.mapMon.obj Y) : (hF.mapMon.preimage f).hom = hF.preimage f.hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : CategoryTheory.MonObj.one = CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom = CategoryTheory.CategoryStruct.id F.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).inv = CategoryTheory.CategoryStruct.id F.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id F.X)
CategoryTheory.Mon.braiding_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.Mon C) : (β_ M N).hom.hom = (β_ M.X N.X).hom
CategoryTheory.Mon.braiding_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.Mon C) : (β_ M N).inv.hom = (β_ M.X N.X).inv
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.map f).hom.app x✝ = f.hom
CategoryTheory.Mon.mkIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (e : M.X ≅ N.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) : M ≅ N
CategoryTheory.Functor.mapMonNatIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.Mon C) : ((CategoryTheory.Functor.mapMonNatIso e).hom.app X).hom = e.hom.app X.X
CategoryTheory.Functor.mapMonNatIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.Mon C) : ((CategoryTheory.Functor.mapMonNatIso e).inv.app X).hom = e.inv.app X.X
CategoryTheory.Mon.associator_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom
CategoryTheory.Mon.associator_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv
CategoryTheory.Functor.comp_mapMon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G)) ((F.comp G).map CategoryTheory.MonObj.one)
CategoryTheory.Mon.tensorObj_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
CategoryTheory.Mon.tensor_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapMonFunctor_map_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor C D} (α : X✝ ⟶ Y✝) (A : CategoryTheory.Mon C) : (((CategoryTheory.Functor.mapMonFunctor C D).map α).app A).hom = α.hom.app A.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : CategoryTheory.IsMonHom (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : CategoryTheory.MonObj.mul = CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.id F.X)
CategoryTheory.Functor.comp_mapMon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X.X X.X) ((F.comp G).map CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapMonCompIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonCompIso.hom.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Functor.mapMonCompIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonCompIso.inv.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.functor.map α).hom = α.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Comon.MonOpOpToComonObjComon 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.ComonObj (Opposite.unop A.X)
CategoryTheory.Comon.ComonToMonOpOpObj_X 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Comon C) : A.ComonToMonOpOpObj.X = Opposite.op A.X
CategoryTheory.Comon.MonOpOpToComonObj_X 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : (CategoryTheory.Comon.MonOpOpToComonObj A).X = Opposite.unop A.X
CategoryTheory.Comon.MonOpOpToComonObj_comon_counit 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.ComonObj.counit = CategoryTheory.MonObj.one.unop
CategoryTheory.Comon.MonOpOpToComonObj_comon_comul 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.mul.unop
CategoryTheory.Comon.monoidal_tensorUnit_comon_counit 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Comon.MonOpOpToComon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comon.MonOpOpToComon C).map f).hom = f.unop.hom.unop
CategoryTheory.Comon.monoidal_tensorUnit_comon_comul 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.ComonObj.comul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
CategoryTheory.Comon.monoidal_whiskerLeft_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X x✝ x✝¹ : CategoryTheory.Comon C) (f : x✝ ⟶ x✝¹) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
CategoryTheory.Comon.monoidal_whiskerRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ X₂✝ : CategoryTheory.Comon C} (f : X₁✝ ⟶ X₂✝) (X : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.X
CategoryTheory.Comon.monoidal_tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.Comon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
CategoryTheory.Comon.monoidal_tensorObj_comon_comul 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Comon C) : CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.mul.unop
CategoryTheory.Comon.monoidal_associator_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop))
CategoryTheory.Comon.monoidal_associator_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop Z.X))
commBialgCatEquivComonCommAlgCat_functor_obj_unop_X 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (A : CommBialgCat R) : (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X = Opposite.op (CommAlgCat.of R ↑A)
commBialgCatEquivComonCommAlgCat_inverse_obj 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (A : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).inverse.obj A = CommBialgCat.of R ↑(Opposite.unop (Opposite.unop A).X)
instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A : CommBialgCat R} [Coalgebra.IsCocomm R ↑A] : CategoryTheory.IsCommMonObj (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X
commBialgCatEquivComonCommAlgCat_functor_map_unop_hom 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A ⟶ B) : ((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom = (CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)).op
commBialgCatEquivComonCommAlgCat_unitIso_hom_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : CommBialgCat R) : (commBialgCatEquivComonCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
commBialgCatEquivComonCommAlgCat_counitIso_inv_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A B : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B) : ↑(CommBialgCat.Hom.hom ((commBialgCatEquivComonCommAlgCat R).inverse.map f)) = CommAlgCat.Hom.hom f.unop.hom.unop
commBialgCatEquivComonCommAlgCat_unitIso_inv_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : CommBialgCat R) : (commBialgCatEquivComonCommAlgCat R).unitIso.inv.app X = CategoryTheory.CategoryStruct.id (CommBialgCat.of R ↑X)
commBialgCatEquivComonCommAlgCat_counitIso_hom_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), mon := CommAlgCat.monObjOpOf })
CategoryTheory.Mon.instMonObjOfIsCommMonObjX 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj M.X] : CategoryTheory.MonObj M
CategoryTheory.yonedaMon_obj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : CategoryTheory.Mon C) : CategoryTheory.yonedaMon.obj M = CategoryTheory.yonedaMonObj M.X
CategoryTheory.Mon.instIsCommMonObj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj M.X] : CategoryTheory.IsCommMonObj M
CategoryTheory.Mon.uniqueHomToTrivial_default_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (A : CategoryTheory.Mon D) : default.hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X
CategoryTheory.Mon.zero_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (M N : CategoryTheory.Mon D) : CategoryTheory.Mon.Hom.hom 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X) CategoryTheory.MonObj.one
CategoryTheory.Mon.hom_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon C) [CategoryTheory.IsCommMonObj M.X] : CategoryTheory.MonObj.one.hom = CategoryTheory.MonObj.one
CategoryTheory.Mon.hom_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon C) [CategoryTheory.IsCommMonObj M.X] : CategoryTheory.MonObj.mul.hom = CategoryTheory.MonObj.mul
CategoryTheory.Mon.fst_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : (CategoryTheory.SemiCartesianMonoidalCategory.fst M N).hom = CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X
CategoryTheory.Mon.snd_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : (CategoryTheory.SemiCartesianMonoidalCategory.snd M N).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X
CategoryTheory.Mon.lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N₁ N₂ : CategoryTheory.Mon C} (f : M ⟶ N₁) (g : M ⟶ N₂) : (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
CategoryTheory.yonedaMon_map_app 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (ψ : X✝ ⟶ Y✝) (x✝ : Cᵒᵖ) : (CategoryTheory.yonedaMon.map ψ).app x✝ = MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom ψ.hom (Opposite.unop x✝))
CategoryTheory.Mon.Hom.hom_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj N.X] : CategoryTheory.Mon.Hom.hom 1 = 1
CategoryTheory.Mon.Hom.hom_pow 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj N.X] (f : M ⟶ N) (n : ℕ) : (f ^ n).hom = f.hom ^ n
CategoryTheory.Mon.Hom.hom_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj N.X] (f g : M ⟶ N) : (f * g).hom = f.hom * g.hom
CategoryTheory.Hom.mulEquivCongrRight_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] (X : C) (a : ↑((CategoryTheory.yonedaMon.obj { X := M, mon := inst✝ }).obj (Opposite.op X))) : (CategoryTheory.Hom.mulEquivCongrRight e X) a = (MonCat.Hom.hom (MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom e.hom X))) a
CategoryTheory.Hom.mulEquivCongrRight_symm_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] (X : C) (a : ↑((CategoryTheory.yonedaMon.obj { X := N, mon := inst✝ }).obj (Opposite.op X))) : (CategoryTheory.Hom.mulEquivCongrRight e X).symm a = (MonCat.Hom.hom (MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom e.inv X))) a
CategoryTheory.Grp.toMon_X 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : A.toMon.X = A.X
CategoryTheory.Grp.forget₂Mon_obj_X 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : ((CategoryTheory.Grp.forget₂Mon C).obj A).X = 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.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.Grp.forget₂Mon_obj_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
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.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.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.Grp.forget₂Mon_obj_mul 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
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.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.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.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.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.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.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.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
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.CommMon.toMon_X 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C) : A.toMon.X = A.X
CategoryTheory.CommMon.forget₂Mon_obj_X 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C) : ((CategoryTheory.CommMon.forget₂Mon C).obj A).X = A.X
CategoryTheory.CommMon.id_hom 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C) : (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.CommMon.instIsIsoHomHomMon 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.CommMon C} {f : M ⟶ N} [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom.hom
CategoryTheory.CommMon.forget₂Mon_obj_one 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
CategoryTheory.CommMon.forget₂Mon_obj_mul 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C) : CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
CategoryTheory.CommMon.hom_ext 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} (f g : A ⟶ B) (h : f.hom.hom = g.hom.hom) : f = g
CategoryTheory.CommMon.hom_ext_iff 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} {f g : A ⟶ B} : f = g ↔ f.hom.hom = g.hom.hom
CategoryTheory.CommMon.forget₂Mon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} (f : A ⟶ B) : ((CategoryTheory.CommMon.forget₂Mon C).map f).hom = f.hom.hom
CategoryTheory.Functor.mapCommMon_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{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.Functor C D) [F.LaxBraided] (A : CategoryTheory.CommMon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
CategoryTheory.CommMon.comp_hom 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {R S T : CategoryTheory.CommMon C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom
CategoryTheory.Functor.mapCommMon_obj_mon_mul 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{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.Functor C D) [F.LaxBraided] (A : CategoryTheory.CommMon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X) (F.map CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{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 F' : CategoryTheory.Functor C D} [F.LaxBraided] [F'.LaxBraided] (f : F ⟶ F') [CategoryTheory.NatTrans.IsMonoidal f] (X : CategoryTheory.CommMon C) : ((CategoryTheory.Functor.mapCommMonNatTrans f).app X).hom.hom = f.app X.X
CategoryTheory.Functor.mapCommMon_map_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{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.Functor C D) [F.LaxBraided] {X✝ Y✝ : CategoryTheory.CommMon C} (f : X✝ ⟶ Y✝) : (F.mapCommMon.map f).hom.hom = F.map f.hom.hom
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CategoryTheory.CommMon C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{u + 1}) : ((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).map f).hom.hom.app x✝ = f.hom.hom
CategoryTheory.CommGrp.hom_ext 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommGrp C} (f g : A ⟶ B) (h : f.hom.hom.hom = g.hom.hom.hom) : f = g
CategoryTheory.CommGrp.hom_ext_iff 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommGrp C} {f g : A ⟶ B} : f = g ↔ f.hom.hom.hom = g.hom.hom.hom
CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp 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.CommGrp.mkIso e one_f mul_f).hom.hom.hom.hom = e.hom
CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp 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.CommGrp.mkIso e one_f mul_f).inv.hom.hom.hom = e.inv
CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.BraidedCategory D] {F F' : CategoryTheory.Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') (X : CategoryTheory.CommGrp C) : ((CategoryTheory.Functor.mapCommGrpNatTrans f).app X).hom.hom.hom = f.app X.X
CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C D) [F.Braided] {X✝ Y✝ : CategoryTheory.CommGrp C} (f : X✝ ⟶ Y✝) : (F.mapCommGrp.map f).hom.hom.hom = F.map f.hom.hom.hom
CategoryTheory.Over.monObjMkPullbackSnd_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [CategoryTheory.MonObj (CategoryTheory.Over.mk f)] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback g)) ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.one)
CategoryTheory.Over.monObjMkPullbackSnd_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [CategoryTheory.MonObj (CategoryTheory.Over.mk f)] : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback g) (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk f)) ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.mul)
AlgebraicGeometry.Scheme.monObjAsOverPullback_one 📋 Mathlib.AlgebraicGeometry.Pullbacks
{M S T : AlgebraicGeometry.Scheme} [M.Over S] {f : T ⟶ S} [CategoryTheory.MonObj (M.asOver S)] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback f)) ((CategoryTheory.Over.pullback f).map CategoryTheory.MonObj.one)
AlgebraicGeometry.Scheme.monObjAsOverPullback_mul 📋 Mathlib.AlgebraicGeometry.Pullbacks
{M S T : AlgebraicGeometry.Scheme} [M.Over S] {f : T ⟶ S} [CategoryTheory.MonObj (M.asOver S)] : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk (M ↘ S)) (CategoryTheory.Over.mk (M ↘ S))) ((CategoryTheory.Over.pullback f).map CategoryTheory.MonObj.mul)
CategoryTheory.Grp.hom_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (H : CategoryTheory.Grp C) [CategoryTheory.IsCommMonObj H.X] : CategoryTheory.MonObj.one.hom.hom = CategoryTheory.MonObj.one
CategoryTheory.Grp.hom_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (H : CategoryTheory.Grp C) [CategoryTheory.IsCommMonObj H.X] : CategoryTheory.MonObj.mul.hom.hom = CategoryTheory.MonObj.mul
CategoryTheory.Grp.Hom.hom_hom_inv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [CategoryTheory.IsCommMonObj H.X] (f : G ⟶ H) : f⁻¹.hom.hom = f.hom.hom⁻¹
CategoryTheory.Grp.Hom.hom_hom_zpow 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [CategoryTheory.IsCommMonObj H.X] (f : G ⟶ H) (n : ℤ) : (f ^ n).hom.hom = f.hom.hom ^ n
CategoryTheory.Grp.Hom.hom_hom_div 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [CategoryTheory.IsCommMonObj H.X] (f g : G ⟶ H) : (f / g).hom.hom = f.hom.hom / g.hom.hom
AlgebraicGeometry.essImage_bialgSpec 📋 Mathlib.AlgebraicGeometry.Group.Affine
{R : CommRingCat} {G : CategoryTheory.Mon (CategoryTheory.Over (AlgebraicGeometry.Spec R))} : (AlgebraicGeometry.bialgSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left
AlgebraicGeometry.one_def 📋 Mathlib.AlgebraicGeometry.Group.Affine
{R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.algSpec R)) ((AlgebraicGeometry.algSpec R).map CategoryTheory.MonObj.one)
CategoryTheory.Monad.toMon_X 📋 Mathlib.CategoryTheory.Monad.EquivMon
{C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : M.toMon.X = M.toFunctor
CategoryTheory.Monad.ofMon_obj 📋 Mathlib.CategoryTheory.Monad.EquivMon
{C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)) (X : C) : (CategoryTheory.Monad.ofMon M).obj X = M.X.obj X
CategoryTheory.Monad.ofMon_η 📋 Mathlib.CategoryTheory.Monad.EquivMon
{C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)) : (CategoryTheory.Monad.ofMon M).η = CategoryTheory.MonObj.one
CategoryTheory.Monad.ofMon_μ 📋 Mathlib.CategoryTheory.Monad.EquivMon
{C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)) : (CategoryTheory.Monad.ofMon M).μ = CategoryTheory.MonObj.mul
CategoryTheory.Monad.monToMonad_map_toNatTrans 📋 Mathlib.CategoryTheory.Monad.EquivMon
(C : Type u) [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Mon (CategoryTheory.Functor C C)} (f : X ⟶ Y) : ((CategoryTheory.Monad.monToMonad C).map f).toNatTrans = f.hom
CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monad.EquivMon
(C : Type u) [CategoryTheory.Category.{v, u} C] (x✝ : CategoryTheory.Mon (CategoryTheory.Functor C C)) : ((CategoryTheory.Monad.monadMonEquiv C).counitIso.inv.app x✝).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Mon (CategoryTheory.Functor C C))).obj x✝).X
CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monad.EquivMon
(C : Type u) [CategoryTheory.Category.{v, u} C] (x✝ : CategoryTheory.Mon (CategoryTheory.Functor C C)) : ((CategoryTheory.Monad.monadMonEquiv C).counitIso.hom.app x✝).hom = CategoryTheory.CategoryStruct.id (((CategoryTheory.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x✝).X
Bimod.regular_X 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (Bimod.regular A).X = A.X
Bimod.actLeft 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (self : Bimod A B) : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X self.X ⟶ self.X
Bimod.actRight 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (self : Bimod A B) : CategoryTheory.MonoidalCategoryStruct.tensorObj self.X B.X ⟶ self.X
Bimod.regular_actLeft 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (Bimod.regular A).actLeft = CategoryTheory.MonObj.mul
Bimod.regular_actRight 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (Bimod.regular A).actRight = CategoryTheory.MonObj.mul

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