Loogle!

Result

Found 173 declarations mentioning CategoryTheory.MonObj.one.

CategoryTheory.MonObj.one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {X : C} [self : CategoryTheory.MonObj X] : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X
CategoryTheory.MonObj.one_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Mon.trivial_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.MonObj.ofIso_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X : C} [CategoryTheory.MonObj M] (e : M ≅ X) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom
CategoryTheory.IsMonHom.one_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : C} {inst✝² : CategoryTheory.MonObj M} {inst✝³ : CategoryTheory.MonObj N} (f : M ⟶ N) [self : CategoryTheory.IsMonHom f] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one
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.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.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.IsMonHom.one_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : C} {inst✝² : CategoryTheory.MonObj M} {inst✝³ : CategoryTheory.MonObj N} (f : M ⟶ N) [self : CategoryTheory.IsMonHom f] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
CategoryTheory.MonObj.mul_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.MonObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) CategoryTheory.MonObj.mul = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
CategoryTheory.MonObj.one_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.MonObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) CategoryTheory.MonObj.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] : (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) CategoryTheory.MonObj.one) CategoryTheory.MonObj.mul
CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] : (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id M)) CategoryTheory.MonObj.mul
CategoryTheory.Functor.obj.η_def 📋 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 : C) [CategoryTheory.MonObj X] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.MonObj M] (f : X₁ ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f) CategoryTheory.MonObj.mul) = f
CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.MonObj M] (f : X₁ ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one) CategoryTheory.MonObj.mul) = f
CategoryTheory.Functor.FullyFaithful.monObj_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.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.MonObj (F.obj X)] : CategoryTheory.MonObj.one = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one)
CategoryTheory.MonObj.one_braiding 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) [CategoryTheory.MonObj X] [CategoryTheory.MonObj Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (β_ X Y).hom = CategoryTheory.MonObj.one
CategoryTheory.MonObj.mul_one_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom f
CategoryTheory.MonObj.one_mul_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom f
CategoryTheory.IsMonHom.mk 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] {f : M ⟶ N} (one_hom : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one := by cat_disch) (mul_hom : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul := by cat_disch) : CategoryTheory.IsMonHom f
CategoryTheory.MonObj.mul_one_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.MonObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h
CategoryTheory.MonObj.one_mul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.MonObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
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.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.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) = CategoryTheory.CategoryStruct.comp f h
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.Functor.obj.η_def_assoc 📋 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 : C) [CategoryTheory.MonObj X] {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.MonObj.one) h)
CategoryTheory.MonObj.tensorObj.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.MonObj.mul_one_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.MonObj.one_mul_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom (CategoryTheory.CategoryStruct.comp f h)
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.MonObj.one_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = CategoryTheory.MonObj.one
CategoryTheory.MonObj.one_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = CategoryTheory.MonObj.one
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.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_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.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.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.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.MonObj.Mon_tensor_mul_one 📋 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.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
CategoryTheory.MonObj.Mon_tensor_one_mul 📋 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.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
CategoryTheory.MonObj.one_associator 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N P : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] [CategoryTheory.MonObj P] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)) CategoryTheory.MonObj.one)) (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)))
CategoryTheory.Comon.ComonToMonOpOpObj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Comon C) : CategoryTheory.MonObj.one = CategoryTheory.ComonObj.counit.op
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
CommAlgCat.one_op_of_unop_hom 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A : Type u} [CommRing A] [Bialgebra R A] : CommAlgCat.Hom.hom CategoryTheory.MonObj.one.unop = Bialgebra.counitAlgHom R A
CategoryTheory.MonObj.instMonoOne 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (M : D) [CategoryTheory.MonObj M] : CategoryTheory.Mono CategoryTheory.MonObj.one
CategoryTheory.MonObj.instIsMonHomOne 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (M : D) [CategoryTheory.MonObj M] : CategoryTheory.IsMonHom CategoryTheory.MonObj.one
CategoryTheory.Hom.one_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [CategoryTheory.MonObj M] : 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one
CategoryTheory.MonObj.lift_comp_one_left 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.MonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.MonObj.one) g) CategoryTheory.MonObj.mul = g
CategoryTheory.MonObj.lift_comp_one_right 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.MonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.MonObj.one)) CategoryTheory.MonObj.mul = f
CategoryTheory.MonObj.lift_comp_one_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.MonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.MonObj.one) g) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp g h
CategoryTheory.MonObj.lift_comp_one_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.MonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.MonObj.one)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.MonObj.one_eq_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [CategoryTheory.MonObj M] : CategoryTheory.MonObj.one = 1
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.MonObj.ofRepresentableBy_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : CategoryTheory.MonObj.one = α.homEquiv'.symm 1
CategoryTheory.GrpObj.mulRight_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [CategoryTheory.GrpObj A] : CategoryTheory.GrpObj.mulRight CategoryTheory.MonObj.one = CategoryTheory.Iso.refl A
CategoryTheory.Grp.trivial_grp_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.GrpObj.ofIso_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] (e : G ≅ X) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom
CategoryTheory.GrpObj.left_inv 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.GrpObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.GrpObj.inv (CategoryTheory.CategoryStruct.id X)) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.right_inv 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.GrpObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.GrpObj.inv) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.lift_comp_inv_left 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.GrpObj B] (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv) f) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.lift_comp_inv_right 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.GrpObj B] (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv)) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
CategoryTheory.Grp.tensorUnit_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
CategoryTheory.GrpObj.lift_inv_comp_left 📋 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.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f) f) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.lift_inv_comp_right 📋 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.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f)) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.left_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.GrpObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.GrpObj.inv (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.GrpObj.right_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.GrpObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.GrpObj.inv) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.GrpObj.lift_comp_inv_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.GrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv) f) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.GrpObj.lift_comp_inv_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.GrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
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.tensorObj_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
CategoryTheory.GrpObj.lift_inv_comp_left_assoc 📋 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] {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f) f) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.GrpObj.lift_inv_comp_right_assoc 📋 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] {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.GrpObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} [toMonObj : CategoryTheory.MonObj X] (inv : X ⟶ X) (left_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X)) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one := by cat_disch) (right_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one := by cat_disch) : CategoryTheory.GrpObj X
CategoryTheory.Functor.FullyFaithful.grpObj_one 📋 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] (hF : F.FullyFaithful) (X : C) [CategoryTheory.GrpObj (F.obj X)] : CategoryTheory.MonObj.one = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one)
CategoryTheory.Functor.mapGrp_obj_grp_one 📋 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] (A : CategoryTheory.Grp C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
CategoryTheory.Functor.mapGrp_id_one 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.Grp C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
CategoryTheory.Grp.homMk'' 📋 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) : A ⟶ B
CategoryTheory.Grp.mkIso 📋 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) : G ≅ H
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.comp_mapGrp_one 📋 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] (A : CategoryTheory.Grp C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G)) ((F.comp G).map CategoryTheory.MonObj.one)
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.comp_mapGrp_one_assoc 📋 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] (A : CategoryTheory.Grp C) {Z : E} (h : ((F.comp G).mapGrp.obj A).X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G)) (G.map (F.map CategoryTheory.MonObj.one))) h
CategoryTheory.CommMon.trivial_mon_one 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
(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.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A) = CategoryTheory.MonObj.one
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.Functor.mapCommMon_id_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.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
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.mkIso 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.CommMon 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.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_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.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id A.X)
CategoryTheory.Functor.comp_mapCommMon_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] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxBraided] [G.LaxBraided] (A : CategoryTheory.CommMon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G)) ((F.comp G).map CategoryTheory.MonObj.one)
CategoryTheory.CommGrp.trivial_grp_one 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.CommGrp.forget₂Grp_obj_one 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
CategoryTheory.CommGrp.forget₂CommMon_obj_one 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
CategoryTheory.Functor.mapCommGrp_id_one 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
CategoryTheory.Functor.mapCommGrp_obj_grp_one 📋 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] (A : CategoryTheory.CommGrp C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
CategoryTheory.CommGrp.mkIso 📋 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) : G ≅ H
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.comp_mapCommGrp_one 📋 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] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] [CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} [F.Braided] {G : CategoryTheory.Functor D E} [G.Braided] (A : CategoryTheory.CommGrp C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G)) ((F.comp G).map CategoryTheory.MonObj.one)
CommGrpTypeEquivalenceCommGrp.inverse_obj_one 📋 Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
{A : CommGrpCat} {x : (fun X => X) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type u))} : (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.one) x = 1
CategoryTheory.Preadditive.one_def 📋 Mathlib.CategoryTheory.Preadditive.CommGrp_
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) : CategoryTheory.MonObj.one = 0
CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one 📋 Mathlib.CategoryTheory.Preadditive.CommGrp_
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.MonObj.one = 0
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.grpObjMkPullbackSnd_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.GrpObj (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)
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)
CategoryTheory.GrpObj.one_inv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.GrpObj.inv = CategoryTheory.MonObj.one
CategoryTheory.GrpObj.one_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] [CategoryTheory.BraidedCategory C] : CategoryTheory.IsCommMonObj G ↔ CategoryTheory.GrpObj.commutator G = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj G G)) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.whiskerLeft_η_commutator 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G CategoryTheory.MonObj.one) (CategoryTheory.GrpObj.commutator G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj G (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) CategoryTheory.MonObj.one
CategoryTheory.GrpObj.η_whiskerRight_commutator 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one G) (CategoryTheory.GrpObj.commutator G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) G)) CategoryTheory.MonObj.one
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.GrpObj.whiskerLeft_η_commutator_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.commutator G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj G (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one G) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.commutator G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) G)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
AlgebraicGeometry.instIsClosedImmersionLeftSchemeOneOverSpecOf 📋 Mathlib.AlgebraicGeometry.Group.Abelian
{K : Type u} [Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K))) [CategoryTheory.GrpObj G] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)
AlgebraicGeometry.one_spec_asOver_spec_left 📋 Mathlib.AlgebraicGeometry.Group.Affine
{R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))
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)
AlgebraicGeometry.one_spec_asOver_spec 📋 Mathlib.AlgebraicGeometry.Group.Affine
{R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.algSpec R)) (CategoryTheory.Over.homMk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))) ⋯)
CategoryTheory.Monad.one_def 📋 Mathlib.CategoryTheory.Monad.EquivMon
{C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : CategoryTheory.MonObj.one = M.η
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
Bimod.actRight_one 📋 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.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.one) self.actRight = (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom
Bimod.one_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.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one self.X) self.actLeft = (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom
Bimod.TensorBimod.actRight_one' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Bimod.TensorBimod.X P Q) CategoryTheory.MonObj.one) (Bimod.TensorBimod.actRight P Q) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Bimod.TensorBimod.X P Q)).hom
Bimod.TensorBimod.one_act_left' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (Bimod.TensorBimod.X P Q)) (Bimod.TensorBimod.actLeft P Q) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Bimod.TensorBimod.X P Q)).hom
Bimod.actRight_one_assoc 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp self.actRight h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom h
Bimod.one_actLeft_assoc 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one self.X) (CategoryTheory.CategoryStruct.comp self.actLeft h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom h
Bimod.mk 📋 Mathlib.CategoryTheory.Monoidal.Bimod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (X : C) (actLeft : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X X ⟶ X) (one_actLeft : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) actLeft = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom := by cat_disch) (left_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) actLeft = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actLeft) actLeft) := by cat_disch) (actRight : CategoryTheory.MonoidalCategoryStruct.tensorObj X B.X ⟶ X) (actRight_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) actRight = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom := by cat_disch) (right_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul) actRight = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X B.X B.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight B.X) actRight) := by cat_disch) (middle_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft B.X) actRight = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X X B.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actRight) actLeft) := by cat_disch) : Bimod A B
CategoryTheory.Bimon.trivial_X_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
(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.BimonObj.one_counit 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.BimonObj.one_counit_assoc 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) = h
CategoryTheory.BimonObj.one_comul 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.one
CategoryTheory.BimonObj.one_comul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
CategoryTheory.Bimon.toMonComonObj_mon_one_hom 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C) : CategoryTheory.MonObj.one.hom = CategoryTheory.MonObj.one
CategoryTheory.Bimon.ofMonComonObjX_one 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one.hom
CategoryTheory.Bimon.one_comul 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [CategoryTheory.BimonObj M] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
CategoryTheory.Bimon.one_comul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [CategoryTheory.BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one) h)
CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
CategoryTheory.BimonObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Bimon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : C} [toMonObj : CategoryTheory.MonObj M] [toComonObj : CategoryTheory.ComonObj M] (mul_comul : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)) := by cat_disch) (one_comul : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.one := by cat_disch) (mul_counit : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit := by cat_disch) (one_counit : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) := by cat_disch) : CategoryTheory.BimonObj M
CategoryTheory.Mon.limit_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Internal.Limits
{J : Type w} [CategoryTheory.Category.{v_1, w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.MonObj.one = hc.lift { pt := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, π := { app := fun X => CategoryTheory.MonObj.one, naturality := ⋯ } }
CategoryTheory.ModObj.one_smul_self 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.MonObj M] (X : C) [CategoryTheory.ModObj M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) CategoryTheory.ModObj.smul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
CategoryTheory.ModObj.one_smul_self_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.MonObj M] (X : C) [CategoryTheory.ModObj M X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
CategoryTheory.ModObj.one_smul 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : CategoryTheory.MonObj M} (X : D) [self : CategoryTheory.ModObj M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.one X) CategoryTheory.ModObj.smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
CategoryTheory.ModObj.one_smul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : CategoryTheory.MonObj M} (X : D) [self : CategoryTheory.ModObj M X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.one X) (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h
CategoryTheory.ModObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [CategoryTheory.MonObj M] {X : D} (smul : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X) (one_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.one X) smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom := by cat_disch) (mul_smul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.mul X) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul) := by cat_disch) : CategoryTheory.ModObj M X
CategoryTheory.IsMonHom.instNormalOne 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] : CategoryTheory.IsMonHom.Normal CategoryTheory.MonObj.one
CategoryTheory.IsMonHom.Normal.of_isPullback_η 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] {φ : H ⟶ G} [CategoryTheory.IsMonHom φ] {P : C} (p : G ⟶ P) [CategoryTheory.GrpObj P] [CategoryTheory.IsMonHom p] (h : CategoryTheory.IsPullback φ (CategoryTheory.SemiCartesianMonoidalCategory.toUnit H) p CategoryTheory.MonObj.one) : CategoryTheory.IsMonHom.Normal φ
CategoryTheory.Conv.one_eq 📋 Mathlib.CategoryTheory.Monoidal.Conv
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [CategoryTheory.ComonObj M] [CategoryTheory.MonObj N] : 1 = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one
CategoryTheory.HopfObj.one_antipode 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.HopfObj A] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.HopfObj.antipode = CategoryTheory.MonObj.one
CategoryTheory.HopfObj.one_antipode_assoc 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.HopfObj A] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode h) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
CategoryTheory.HopfObj.antipode_left 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X] : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode X) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one
CategoryTheory.HopfObj.antipode_right 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X] : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.HopfObj.antipode) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one
CategoryTheory.HopfObj.antipode_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode X) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.HopfObj.antipode_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.HopfObj.antipode) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
CategoryTheory.HopfObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : C} [toBimonObj : CategoryTheory.BimonObj X] (antipode : X ⟶ X) (antipode_left : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight antipode X) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one := by cat_disch) (antipode_right : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X antipode) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one := by cat_disch) : CategoryTheory.HopfObj X
CategoryTheory.HopfObj.antipode_comul₁ 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.HopfObj A] : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.ComonObj.comul)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul))))))))) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))
CategoryTheory.HopfObj.mul_antipode₁ 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.HopfObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode A) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.MonObj.mul) CategoryTheory.MonObj.mul))))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom CategoryTheory.MonObj.one)
CategoryTheory.HopfObj.mul_antipode₂ 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.HopfObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ A A).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HopfObj.antipode CategoryTheory.HopfObj.antipode)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.MonObj.mul) CategoryTheory.MonObj.mul)))))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom CategoryTheory.MonObj.one)
CategoryTheory.HopfObj.antipode_comul₂ 📋 Mathlib.CategoryTheory.Monoidal.Hopf_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.HopfObj A] : CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.ComonObj.comul)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ A A).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HopfObj.antipode CategoryTheory.HopfObj.antipode))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)))))))))) = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [CategoryTheory.MonObj A] (X : C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.app X
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app 📋 Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Mon D)) (X : C) : CategoryTheory.MonObj.one.app X = CategoryTheory.MonObj.one
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app 📋 Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C (CategoryTheory.CommMon D)) (X : C) : CategoryTheory.MonObj.one.app X = CategoryTheory.MonObj.one
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : CategoryTheory.CommMon (CategoryTheory.Functor C D)) (X : C) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.app X
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one 📋 Mathlib.CategoryTheory.Monoidal.Internal.Module
{R : Type u} [CommRing R] (A : AlgCat R) : CategoryTheory.MonObj.one = ModuleCat.ofHom (Algebra.linearMap R ↑A)
ModuleCat.MonModuleEquivalenceAlgebra.algebraMap 📋 Mathlib.CategoryTheory.Monoidal.Internal.Module
{R : Type u} [CommRing R] (A : ModuleCat R) [CategoryTheory.MonObj A] (r : R) : (algebraMap R ↑A) r = (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.one) r
MonObj.mopMonObj_one_unmop 📋 Mathlib.CategoryTheory.Monoidal.Opposite.Mon
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.MonObj M] : CategoryTheory.MonObj.one.unmop = CategoryTheory.MonObj.one
MonObj.unmopMonObj_one 📋 Mathlib.CategoryTheory.Monoidal.Opposite.Mon
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [CategoryTheory.MonObj M] : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.unmop
MonObj.mopEquiv_functor_obj_mon_one_unmop 📋 Mathlib.CategoryTheory.Monoidal.Opposite.Mon
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : CategoryTheory.MonObj.one.unmop = CategoryTheory.MonObj.one
MonObj.mopEquiv_inverse_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Opposite.Mon
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon Cᴹᵒᵖ) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.unmop

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 ce5dd8c