Loogle!

Result

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

CategoryTheory.Mon 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max u₁ v₁)
CategoryTheory.Mon.trivial 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Mon C
CategoryTheory.Mon.X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : CategoryTheory.Mon C) : C
CategoryTheory.Mon.instCategory 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Mon C)
CategoryTheory.Mon.instInhabited 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Inhabited (CategoryTheory.Mon C)
CategoryTheory.Mon.Hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M N : CategoryTheory.Mon C) : Type v₁
CategoryTheory.Mon.instHasInitial 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.HasInitial (CategoryTheory.Mon C)
CategoryTheory.Mon.id 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : M.Hom M
CategoryTheory.Mon.mk 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [mon : CategoryTheory.MonObj X] : CategoryTheory.Mon C
CategoryTheory.Mon.forget 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.Mon C) C
CategoryTheory.Mon.homInhabited 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : Inhabited (M.Hom M)
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 (CategoryTheory.Discrete PUnit.{w + 1}) C
CategoryTheory.Mon.mon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : CategoryTheory.Mon C) : CategoryTheory.MonObj self.X
CategoryTheory.Mon.monMonoidal 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalCategory (CategoryTheory.Mon C)
CategoryTheory.Mon.monMonoidalStruct 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Mon C)
CategoryTheory.Mon.forget_faithful 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Mon.forget C).Faithful
CategoryTheory.Mon.instReflectsIsomorphismsForget 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Mon.forget C).ReflectsIsomorphisms
CategoryTheory.Mon.instSymmetricCategory 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory (CategoryTheory.Mon C)
CategoryTheory.Mon.instMonoidalForget 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.Mon.forget C).Monoidal
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).LaxMonoidal
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).obj x✝ = A.X
CategoryTheory.Mon.forget_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (CategoryTheory.Mon.forget C).obj A = A.X
CategoryTheory.Mon.uniqueHomFromTrivial 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : Unique (CategoryTheory.Mon.trivial C ⟶ A)
CategoryTheory.Mon.comp 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : CategoryTheory.Mon C} (f : M.Hom N) (g : N.Hom O) : M.Hom O
CategoryTheory.Mon.tensorUnit_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon C)).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
CategoryTheory.Mon.Hom.hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (self : M.Hom N) : M.X ⟶ N.X
CategoryTheory.Functor.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] : CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Mon D)
CategoryTheory.Mon.hom_injective 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} : Function.Injective CategoryTheory.Mon.Hom.hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C ≌ CategoryTheory.Mon C
CategoryTheory.Mon.id_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : M.id.hom = CategoryTheory.CategoryStruct.id M.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) (CategoryTheory.Mon C)
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
CategoryTheory.Mon.Hom.isMonHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (self : M.Hom N) : CategoryTheory.IsMonHom self.hom
CategoryTheory.Mon.monMonoidalStruct_tensorObj_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).X = CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X
CategoryTheory.Functor.Faithful.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.LaxMonoidal] [F.Faithful] : F.mapMon.Faithful
CategoryTheory.Mon.mkIso' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] : { X := M, mon := inst✝ } ≅ { X := N, mon := inst✝¹ }
CategoryTheory.Mon.id_hom' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
CategoryTheory.Functor.mapMonFunctor 📋 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] : CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor C D) (CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Mon D))
CategoryTheory.Mon.Hom.mk 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (hom : M.X ⟶ N.X) [isMonHom_hom : CategoryTheory.IsMonHom hom] : M.Hom N
CategoryTheory.Functor.mapMonIdIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Functor.id C).mapMon ≅ CategoryTheory.Functor.id (CategoryTheory.Mon C)
CategoryTheory.Functor.FullyFaithful.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapMon.FullyFaithful
CategoryTheory.Mon.instIsMonHomHom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (f : M ⟶ N) : CategoryTheory.IsMonHom f.hom
CategoryTheory.Mon.instIsIsoHom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} {f : M ⟶ N} [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom
CategoryTheory.Mon.ofHom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : C} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (f : A ⟶ B) [CategoryTheory.IsMonHom f] : { X := A, mon := inst✝ } ⟶ { X := B, mon := inst✝¹ }
CategoryTheory.Mon.Hom.ext 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : CategoryTheory.Mon C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y
CategoryTheory.Mon.Hom.ext_iff 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : CategoryTheory.Mon C} {x y : M.Hom N} : x = y ↔ x.hom = y.hom
CategoryTheory.Equivalence.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryTheory.Mon C ≌ CategoryTheory.Mon D
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).map x✝ = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.Functor.Full.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] : F.mapMon.Full
CategoryTheory.Functor.mapMon_obj_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.Mon C) : (F.mapMon.obj A).X = F.obj A.X
CategoryTheory.Mon.forget_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Mon.forget C).map f = f.hom
CategoryTheory.Functor.instLaxMonoidalMonMapMon 📋 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) [CategoryTheory.BraidedCategory C] [CategoryTheory.BraidedCategory D] [F.LaxBraided] : F.mapMon.LaxMonoidal
CategoryTheory.Functor.essImage_mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : CategoryTheory.Mon D} : F.mapMon.essImage M ↔ F.essImage M.X
CategoryTheory.Functor.instMonoidalMonMapMon 📋 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) [CategoryTheory.BraidedCategory C] [CategoryTheory.BraidedCategory D] [F.Braided] : F.mapMon.Monoidal
CategoryTheory.Mon.tensorUnit_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Mon.comp_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : CategoryTheory.Mon C} (f : M.Hom N) (g : N.Hom O) : (CategoryTheory.Mon.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) = CategoryTheory.MonObj.one
CategoryTheory.Mon.mkIso'_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] : (CategoryTheory.Mon.mkIso' e).hom.hom = e.hom
CategoryTheory.Mon.mkIso'_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] : (CategoryTheory.Mon.mkIso' e).inv.hom = e.inv
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A = CategoryTheory.LaxMonoidalFunctor.of (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A)
CategoryTheory.Adjunction.mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : F.mapMon ⊣ G.mapMon
CategoryTheory.Mon.instIsIsoHomOfMapForget 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((CategoryTheory.Mon.forget C).map f)] : CategoryTheory.IsIso f.hom
CategoryTheory.Mon.uniqueHomFromTrivial_default_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : default.hom = CategoryTheory.MonObj.one
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C) ≅ CategoryTheory.Functor.id (CategoryTheory.Mon C)
CategoryTheory.Mon.Hom.ext' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} {f g : M ⟶ N} (w : f.hom = g.hom) : f = g
CategoryTheory.Mon.Hom.ext'_iff 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom
CategoryTheory.Functor.mapMonFunctor_obj 📋 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.LaxMonoidalFunctor C D) : (CategoryTheory.Functor.mapMonFunctor C D).obj F = F.mapMon
CategoryTheory.Mon.forget_ε 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.forget C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Mon.forget_η 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Mon.forget C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : (((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C)).obj F).X ≅ ((CategoryTheory.Functor.id (CategoryTheory.Mon C)).obj F).X
CategoryTheory.Equivalence.mapMon_functor 📋 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 : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.functor = e.functor.mapMon
CategoryTheory.Equivalence.mapMon_inverse 📋 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 : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.inverse = e.inverse.mapMon
CategoryTheory.Functor.mapMonNatIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [CategoryTheory.NatTrans.IsMonoidal e.hom] : F.mapMon ≅ F'.mapMon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) X Y = CategoryTheory.MonObj.mul
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.obj A).obj x✝ = A.X
CategoryTheory.Mon.comp_hom' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N K : CategoryTheory.Mon C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
CategoryTheory.Functor.instLaxBraidedMonMapMon 📋 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} [CategoryTheory.SymmetricCategory C] [CategoryTheory.SymmetricCategory D] [F.LaxBraided] : F.mapMon.LaxBraided
CategoryTheory.Functor.mapMonCompIso 📋 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] : (F.comp G).mapMon ≅ F.mapMon.comp G.mapMon
CategoryTheory.Functor.mapMonNatTrans 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [CategoryTheory.NatTrans.IsMonoidal f] : F.mapMon ⟶ F'.mapMon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_X 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.functor.obj F).X = F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Mon.tensorUnit_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonObj.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
CategoryTheory.Functor.instBraidedMonMapMon 📋 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} [CategoryTheory.SymmetricCategory C] [CategoryTheory.SymmetricCategory D] [F.Braided] : F.mapMon.Braided
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.obj A).map x✝ = CategoryTheory.CategoryStruct.id A.X
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) = CategoryTheory.MonObj.one
CategoryTheory.Mon.whiskerLeft_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Mon C} (f : X ⟶ Y) (Z : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z.X
CategoryTheory.Mon.whiskerRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) {Y Z : CategoryTheory.Mon C} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
CategoryTheory.Mon.forget_δ 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Mon.forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
CategoryTheory.Mon.forget_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
CategoryTheory.Mon.comp_hom'_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N K : CategoryTheory.Mon C} (f : M ⟶ N) (g : N ⟶ K) {Z : C} (h : K.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
CategoryTheory.Functor.mapMon_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).obj F = F.mapMon.obj (CategoryTheory.Mon.trivial (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Functor.id_mapMon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
CategoryTheory.Mon.leftUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom
CategoryTheory.Mon.leftUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv
CategoryTheory.Mon.rightUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom
CategoryTheory.Mon.rightUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) (x✝ x✝¹ : CategoryTheory.Discrete PUnit.{w + 1}) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) x✝ x✝¹ = CategoryTheory.MonObj.mul
CategoryTheory.Functor.mapMon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) : (F.mapMon.map f).hom = F.map f.hom
CategoryTheory.Functor.mapMonNatTrans_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [CategoryTheory.NatTrans.IsMonoidal f] (X : CategoryTheory.Mon C) : ((CategoryTheory.Functor.mapMonNatTrans f).app X).hom = f.app X.X
CategoryTheory.Mon.tensorObj_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
CategoryTheory.Mon.tensor_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
CategoryTheory.Functor.mapMon_obj_mon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X) (F.map CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapMonIdIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonIdIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Functor.mapMonIdIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonIdIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor.id (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) ≅ (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).comp (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C)
CategoryTheory.Mon.monMonoidalStruct_tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.Mon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
CategoryTheory.Mon.Hom.mk' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (f : M.X ⟶ N.X) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul := by cat_disch) : M.Hom N
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).map f).hom.app x✝ = f.hom
CategoryTheory.Functor.id_mapMon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X X.X)) CategoryTheory.MonObj.mul
CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : CategoryTheory.Mon C} (f : F.mapMon.obj X ⟶ F.mapMon.obj Y) : (hF.mapMon.preimage f).hom = hF.preimage f.hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : CategoryTheory.MonObj.one = CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom = CategoryTheory.CategoryStruct.id F.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).inv = CategoryTheory.CategoryStruct.id F.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id F.X)
CategoryTheory.Mon.braiding_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.Mon C) : (β_ M N).hom.hom = (β_ M.X N.X).hom
CategoryTheory.Mon.braiding_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.Mon C) : (β_ M N).inv.hom = (β_ M.X N.X).inv
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.map f).hom.app x✝ = f.hom
CategoryTheory.Mon.mkIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.Mon C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.MonObj.mul := by cat_disch) : M ≅ N
CategoryTheory.Functor.mapMonNatIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.Mon C) : ((CategoryTheory.Functor.mapMonNatIso e).hom.app X).hom = e.hom.app X.X
CategoryTheory.Functor.mapMonNatIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F F' : CategoryTheory.Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.Mon C) : ((CategoryTheory.Functor.mapMonNatIso e).inv.app X).hom = e.inv.app X.X
CategoryTheory.Mon.associator_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom
CategoryTheory.Mon.associator_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Mon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv
CategoryTheory.Functor.comp_mapMon_one 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G)) ((F.comp G).map CategoryTheory.MonObj.one)
CategoryTheory.Mon.tensorObj_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
CategoryTheory.Mon.tensor_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapMonFunctor_map_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor C D} (α : X✝ ⟶ Y✝) (A : CategoryTheory.Mon C) : (((CategoryTheory.Functor.mapMonFunctor C D).map α).app A).hom = α.hom.app A.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : CategoryTheory.IsMonHom (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : CategoryTheory.MonObj.mul = CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Mon C) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.id F.X)
CategoryTheory.Functor.comp_mapMon_mul 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X.X X.X) ((F.comp G).map CategoryTheory.MonObj.mul)
CategoryTheory.Functor.mapMonCompIso_hom_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonCompIso.hom.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Functor.mapMonCompIso_inv_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.Mon C) : (CategoryTheory.Functor.mapMonCompIso.inv.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
CategoryTheory.Equivalence.mapMon_unitIso 📋 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 : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.unitIso = CategoryTheory.Functor.mapMonIdIso.symm ≪≫ CategoryTheory.Functor.mapMonNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapMonCompIso
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.functor.map α).hom = α.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Adjunction.mapMon_counit 📋 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} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : a.mapMon.counit = CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapMonCompIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapMonNatTrans a.counit) CategoryTheory.Functor.mapMonIdIso.hom)
CategoryTheory.Adjunction.mapMon_unit 📋 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} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : a.mapMon.unit = CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapMonIdIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapMonNatTrans a.unit) CategoryTheory.Functor.mapMonCompIso.hom)
CategoryTheory.Equivalence.mapMon_counitIso 📋 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 : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.counitIso = CategoryTheory.Functor.mapMonCompIso.symm ≪≫ CategoryTheory.Functor.mapMonNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapMonIdIso
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).map α = ((CategoryTheory.Functor.mapMonFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C).map α).app (CategoryTheory.Mon.trivial (CategoryTheory.Discrete PUnit.{w + 1}))
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{w + 1}) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso C).hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{w + 1}) : ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso C).inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})))
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.unitIso.hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.unitIso.inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})))
CategoryTheory.Comon.ComonToMonOpOpObj 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Comon C) : CategoryTheory.Mon Cᵒᵖ
CategoryTheory.Comon.MonOpOpToComonObj 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.Comon C
CategoryTheory.Comon.MonOpOpToComonObjComon 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.ComonObj (Opposite.unop A.X)
CategoryTheory.Comon.MonOpOpToComonObj_X 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : (CategoryTheory.Comon.MonOpOpToComonObj A).X = Opposite.unop A.X
CategoryTheory.Comon.ComonToMonOpOp 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.Comon C) (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ
CategoryTheory.Comon.Comon_EquivMon_OpOp 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Comon C ≌ (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ
CategoryTheory.Comon.MonOpOpToComon 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ (CategoryTheory.Comon C)
CategoryTheory.Comon.ComonToMonOpOp_obj 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Comon C) : (CategoryTheory.Comon.ComonToMonOpOp C).obj A = Opposite.op A.ComonToMonOpOpObj
CategoryTheory.Comon.MonOpOpToComon_obj 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ) : (CategoryTheory.Comon.MonOpOpToComon C).obj A = CategoryTheory.Comon.MonOpOpToComonObj (Opposite.unop A)
CategoryTheory.Comon.Comon_EquivMon_OpOp_functor 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Comon.Comon_EquivMon_OpOp C).functor = CategoryTheory.Comon.ComonToMonOpOp C
CategoryTheory.Comon.Comon_EquivMon_OpOp_inverse 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Comon.Comon_EquivMon_OpOp C).inverse = CategoryTheory.Comon.MonOpOpToComon C
CategoryTheory.Comon.MonOpOpToComonObj_comon_counit 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.ComonObj.counit = CategoryTheory.MonObj.one.unop
CategoryTheory.Comon.MonOpOpToComonObj_comon_comul 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon Cᵒᵖ) : CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.mul.unop
CategoryTheory.Comon.Comon_EquivMon_OpOp_unitIso 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Comon.Comon_EquivMon_OpOp C).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comon C)).obj x)) ⋯
CategoryTheory.Comon.monoidal_tensorUnit_comon_counit 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.Comon.MonOpOpToComon_map_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comon.MonOpOpToComon C).map f).hom = f.unop.hom.unop
CategoryTheory.Comon.ComonToMonOpOp_map 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Comon C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comon.ComonToMonOpOp C).map f = Opposite.op { hom := f.hom.op, isMonHom_hom := ⋯ }
CategoryTheory.Comon.monoidal_tensorUnit_comon_comul 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.ComonObj.comul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
CategoryTheory.Comon.Comon_EquivMon_OpOp_counitIso 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Comon.Comon_EquivMon_OpOp C).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.Comon.MonOpOpToComon C).comp (CategoryTheory.Comon.ComonToMonOpOp C)).obj x)) ⋯
CategoryTheory.Comon.monoidal_whiskerLeft_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X x✝ x✝¹ : CategoryTheory.Comon C) (f : x✝ ⟶ x✝¹) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
CategoryTheory.Comon.monoidal_whiskerRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ X₂✝ : CategoryTheory.Comon C} (f : X₁✝ ⟶ X₂✝) (X : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.X
CategoryTheory.Comon.monoidal_tensorHom_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.Comon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
CategoryTheory.Comon.monoidal_tensorObj_comon_comul 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Comon C) : CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.mul.unop
CategoryTheory.Comon.monoidal_leftUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop X.X) (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom
CategoryTheory.Comon.monoidal_leftUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop X.X)
CategoryTheory.Comon.monoidal_rightUnitor_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom
CategoryTheory.Comon.monoidal_rightUnitor_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop)
CategoryTheory.Comon.monoidal_associator_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop))
CategoryTheory.Comon.monoidal_associator_inv_hom 📋 Mathlib.CategoryTheory.Monoidal.Comon_
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Comon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Comon.MonOpOpToComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop Z.X))
commBialgCatEquivComonCommAlgCat 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] : CommBialgCat R ≌ (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ
commBialgCatEquivComonCommAlgCat_functor_obj_unop_X 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (A : CommBialgCat R) : (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X = Opposite.op (CommAlgCat.of R ↑A)
commBialgCatEquivComonCommAlgCat_inverse_obj 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (A : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).inverse.obj A = CommBialgCat.of R ↑(Opposite.unop (Opposite.unop A).X)
instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A : CommBialgCat R} [Coalgebra.IsCocomm R ↑A] : CategoryTheory.IsCommMonObj (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X
commBialgCatEquivComonCommAlgCat_functor_map_unop_hom 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A ⟶ B) : ((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom = (CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)).op
commBialgCatEquivComonCommAlgCat_unitIso_hom_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : CommBialgCat R) : (commBialgCatEquivComonCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
commBialgCatEquivComonCommAlgCat_counitIso_inv_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom 📋 Mathlib.Algebra.Category.CommBialgCat
{R : Type u} [CommRing R] {A B : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B) : ↑(CommBialgCat.Hom.hom ((commBialgCatEquivComonCommAlgCat R).inverse.map f)) = CommAlgCat.Hom.hom f.unop.hom.unop
commBialgCatEquivComonCommAlgCat_unitIso_inv_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : CommBialgCat R) : (commBialgCatEquivComonCommAlgCat R).unitIso.inv.app X = CategoryTheory.CategoryStruct.id (CommBialgCat.of R ↑X)
commBialgCatEquivComonCommAlgCat_counitIso_hom_app 📋 Mathlib.Algebra.Category.CommBialgCat
(R : Type u) [CommRing R] (X : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), mon := CommAlgCat.monObjOpOf })
CategoryTheory.Mon.instHasZeroMorphisms 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.Mon D)
CategoryTheory.Mon.instHasZeroObject 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Mon D)
CategoryTheory.Mon.isZero_trivial 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
(D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.IsZero (CategoryTheory.Mon.trivial D)
CategoryTheory.Mon.instCartesianMonoidalCategory 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Mon C)
CategoryTheory.yonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Functor Cᵒᵖ MonCat)
CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaMon.Faithful
CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaMon.Full
CategoryTheory.yonedaMonFullyFaithful 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaMon.FullyFaithful
CategoryTheory.uniqueHomToTrivial 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (A : CategoryTheory.Mon D) : Unique (A ⟶ CategoryTheory.Mon.trivial D)
CategoryTheory.Mon.uniqueHomToTrivial 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (A : CategoryTheory.Mon D) : Unique (A ⟶ CategoryTheory.Mon.trivial D)
CategoryTheory.Mon.instZeroHom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] (M N : CategoryTheory.Mon D) : Zero (M ⟶ N)
CategoryTheory.Mon.instMonObjOfIsCommMonObjX 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj M.X] : CategoryTheory.MonObj M
CategoryTheory.yonedaMon_obj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : CategoryTheory.Mon C) : CategoryTheory.yonedaMon.obj M = CategoryTheory.yonedaMonObj M.X
CategoryTheory.Mon.instIsCommMonObj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj M.X] : CategoryTheory.IsCommMonObj M
CategoryTheory.essImage_yonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaMon.essImage = fun F => (F.comp (CategoryTheory.forget MonCat)).IsRepresentable

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision 69fae59