Loogle!

Result

Found 61 declarations mentioning CategoryTheory.Hom.monoid.

CategoryTheory.Hom.monoid 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [CategoryTheory.MonObj M] : Monoid (X ⟶ M)
CategoryTheory.isCommMonObj_iff_isMulCommutative 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [CategoryTheory.MonObj M] [CategoryTheory.BraidedCategory C] : CategoryTheory.IsCommMonObj M ↔ ∀ (X : C), IsMulCommutative (X ⟶ M)
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.IsMonHom.monoidHom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f : M ⟶ N) [CategoryTheory.IsMonHom f] (X : C) : (X ⟶ M) →* (X ⟶ N)
CategoryTheory.Hom.mulEquivCongrRight 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] (X : C) : (X ⟶ M) ≃* (X ⟶ N)
CategoryTheory.IsMonHom.monoidHom_id 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [CategoryTheory.MonObj M] : CategoryTheory.IsMonHom.monoidHom (CategoryTheory.CategoryStruct.id M) X = MonoidHom.id (X ⟶ M)
CategoryTheory.MonObj.comp_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [CategoryTheory.MonObj M] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f 1 = 1
CategoryTheory.Hom.mul_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] (f₁ f₂ : X ⟶ M) : f₁ * f₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) CategoryTheory.MonObj.mul
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.MonObj.comp_pow 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [CategoryTheory.MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) : CategoryTheory.CategoryStruct.comp h (f ^ n) = CategoryTheory.CategoryStruct.comp h f ^ n
CategoryTheory.MonObj.one_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f : M ⟶ N) [CategoryTheory.IsMonHom f] : CategoryTheory.CategoryStruct.comp 1 f = 1
CategoryTheory.MonObj.comp_one_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [CategoryTheory.MonObj M] (f : X ⟶ Y) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp 1 h) = CategoryTheory.CategoryStruct.comp 1 h
CategoryTheory.Functor.homMonoidHom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] : (X ⟶ M) →* (F.obj X ⟶ F.obj M)
CategoryTheory.MonObj.pow_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [CategoryTheory.IsMonHom g] : CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n
CategoryTheory.MonObj.comp_pow_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [CategoryTheory.MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) {Z : C} (h✝ : M ⟶ Z) : CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp (f ^ n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f ^ n) h✝
CategoryTheory.MonObj.one_comp_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f : M ⟶ N) [CategoryTheory.IsMonHom f] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp 1 (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 1 h
CategoryTheory.MonObj.comp_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [CategoryTheory.MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) : CategoryTheory.CategoryStruct.comp f (g₁ * g₂) = CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂
CategoryTheory.MonObj.pow_comp_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [CategoryTheory.IsMonHom g] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (f ^ n) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h
CategoryTheory.Functor.FullyFaithful.homMulEquiv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) : (X ⟶ M) ≃* (F.obj X ⟶ F.obj M)
CategoryTheory.MonObj.mul_eq_mul 📋 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.mul = CategoryTheory.SemiCartesianMonoidalCategory.fst M M * CategoryTheory.SemiCartesianMonoidalCategory.snd M M
CategoryTheory.MonObj.mul_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [CategoryTheory.IsMonHom g] : CategoryTheory.CategoryStruct.comp (f₁ * f₂) g = CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g
CategoryTheory.MonObj.comp_mul_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [CategoryTheory.MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g₁ * g₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂) h
CategoryTheory.IsMonHom.monoidHom_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f : M ⟶ N) [CategoryTheory.IsMonHom f] (X : C) (x✝ : X ⟶ M) : (CategoryTheory.IsMonHom.monoidHom f X) x✝ = CategoryTheory.CategoryStruct.comp x✝ f
CategoryTheory.MonObj.mul_comp_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [CategoryTheory.IsMonHom g] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (f₁ * f₂) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g) h
CategoryTheory.Functor.map_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] : F.map 1 = 1
CategoryTheory.IsMonHom.monoidHom_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N O X : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] [CategoryTheory.MonObj O] (f : M ⟶ N) (g : N ⟶ O) [CategoryTheory.IsMonHom f] [CategoryTheory.IsMonHom g] : CategoryTheory.IsMonHom.monoidHom (CategoryTheory.CategoryStruct.comp f g) X = (CategoryTheory.IsMonHom.monoidHom g X).comp (CategoryTheory.IsMonHom.monoidHom f X)
CategoryTheory.Functor.map_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (f g : X ⟶ M) : F.map (f * g) = F.map f * F.map g
CategoryTheory.yonedaMonObj_map 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [CategoryTheory.MonObj M] {X Y₂ : Cᵒᵖ} (φ : X ⟶ Y₂) : (CategoryTheory.yonedaMonObj M).map φ = MonCat.ofHom { toFun := fun x => CategoryTheory.CategoryStruct.comp φ.unop x, map_one' := ⋯, map_mul' := ⋯ }
CategoryTheory.yonedaMon_map_app 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {X✝ Y✝ : CategoryTheory.Mon C} (ψ : X✝ ⟶ Y✝) (x✝ : Cᵒᵖ) : (CategoryTheory.yonedaMon.map ψ).app x✝ = MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom ψ.hom (Opposite.unop x✝))
CategoryTheory.Functor.homMonoidHom_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (a✝ : X ⟶ M) : F.homMonoidHom a✝ = F.map a✝
CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply 📋 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) (X✝ : Cᵒᵖ) (a✝ : Opposite.unop X✝ ⟶ X) : (MonCat.Hom.hom ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X F α).hom.app X✝)) a✝ = α.homEquiv' a✝
CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply 📋 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) (X✝ : Cᵒᵖ) (a✝ : ↑(F.1 X✝)) : (MonCat.Hom.hom ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X F α).inv.app X✝)) a✝ = α.homEquiv'.symm a✝
CategoryTheory.Mon.Hom.hom_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj N.X] : CategoryTheory.Mon.Hom.hom 1 = 1
CategoryTheory.Mon.Hom.hom_pow 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj N.X] (f : M ⟶ N) (n : ℕ) : (f ^ n).hom = f.hom ^ n
CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (a✝ : X ⟶ M) : (CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF) a✝ = F.map a✝
CategoryTheory.Mon.Hom.hom_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [CategoryTheory.IsCommMonObj N.X] (f g : M ⟶ N) : (f * g).hom = f.hom * g.hom
CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Category.{w, u_2} D] [CategoryTheory.CartesianMonoidalCategory D] {M X : C} [CategoryTheory.MonObj M] (F : CategoryTheory.Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M) : (CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF).symm f = hF.preimage f
CategoryTheory.Hom.mulEquivCongrRight_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] (X : C) (a : ↑((CategoryTheory.yonedaMon.obj { X := M, mon := inst✝ }).obj (Opposite.op X))) : (CategoryTheory.Hom.mulEquivCongrRight e X) a = (MonCat.Hom.hom (MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom e.hom X))) a
CategoryTheory.Hom.mulEquivCongrRight_symm_apply 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj N] (e : M ≅ N) [CategoryTheory.IsMonHom e.hom] (X : C) (a : ↑((CategoryTheory.yonedaMon.obj { X := N, mon := inst✝ }).obj (Opposite.op X))) : (CategoryTheory.Hom.mulEquivCongrRight e X).symm a = (MonCat.Hom.hom (MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom e.inv X))) a
CategoryTheory.GrpObj.ofInvertible 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] (h : (X : C) → (f : X ⟶ G) → Invertible f) : CategoryTheory.GrpObj G
CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {X G : C} [CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) (CategoryTheory.GrpObj.conj G) = f₁ * f₂ * f₁⁻¹
CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {X G : C} [CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.conj G) h) = CategoryTheory.CategoryStruct.comp (f₁ * f₂ * f₁⁻¹) h
CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {X G : C} [CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) (CategoryTheory.GrpObj.commutator G) = f₁ * f₂ * f₁⁻¹ * f₂⁻¹
CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {X G : C} [CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.commutator G) h) = CategoryTheory.CategoryStruct.comp (f₁ * f₂ * f₁⁻¹ * f₂⁻¹) h
CategoryTheory.Grp.Hom.hom_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [CategoryTheory.IsCommMonObj H.X] : CategoryTheory.InducedCategory.Hom.hom 1 = 1
CategoryTheory.Grp.Hom.hom_pow 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [CategoryTheory.IsCommMonObj H.X] (f : G ⟶ H) (n : ℕ) : (f ^ n).hom = f.hom ^ n
CategoryTheory.Grp.Hom.hom_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [CategoryTheory.IsCommMonObj H.X] (f g : G ⟶ H) : (f * g).hom = f.hom * g.hom
AlgebraicGeometry.Spec.mapMulEquiv 📋 Mathlib.AlgebraicGeometry.Group.Affine
{R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Bialgebra R S] [Algebra R T] : WithConv (S →ₐ[R] T) ≃* ((AlgebraicGeometry.Spec (CommRingCat.of T)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (AlgebraicGeometry.Spec (CommRingCat.of S)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)))
CategoryTheory.shrinkYonedaGrpObjObjEquiv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Grp C} {Y : Cᵒᵖ} : ↑((CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj M).obj Y) ≃* (Opposite.unop Y ⟶ M.X)
CategoryTheory.shrinkYonedaMonObjObjEquiv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Mon C} {Y : Cᵒᵖ} : ↑((CategoryTheory.shrinkYonedaMon.{w, v, u}.obj M).obj Y) ≃* (Opposite.unop Y ⟶ M.X)
CategoryTheory.shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Grp C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Opposite.unop Y ⟶ M.X) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj M).map g)) (CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm f) = CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
CategoryTheory.shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M M' : CategoryTheory.Grp C} {Y : Cᵒᵖ} (f : Opposite.unop Y ⟶ M.X) (g : M ⟶ M') : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaGrp.{w, v, u}.map g).app Y)) (CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm f) = CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g.hom.hom)
CategoryTheory.shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Mon C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Opposite.unop Y ⟶ M.X) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaMon.{w, v, u}.obj M).map g)) (CategoryTheory.shrinkYonedaMonObjObjEquiv.symm f) = CategoryTheory.shrinkYonedaMonObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
CategoryTheory.shrinkYonedaGrpObjObjEquiv_symm_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Grp C} {Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ M.X) : CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj M).map g.op)) (CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm f)
CategoryTheory.shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M M' : CategoryTheory.Mon C} {Y : Cᵒᵖ} (f : Opposite.unop Y ⟶ M.X) (g : M ⟶ M') : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaMon.{w, v, u}.map g).app Y)) (CategoryTheory.shrinkYonedaMonObjObjEquiv.symm f) = CategoryTheory.shrinkYonedaMonObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g.hom)
CategoryTheory.shrinkYonedaMonObjObjEquiv_symm_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Mon C} {Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ M.X) : CategoryTheory.shrinkYonedaMonObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaMon.{w, v, u}.obj M).map g.op)) (CategoryTheory.shrinkYonedaMonObjObjEquiv.symm f)
CategoryTheory.Hom.mulAction 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {X : C} [CategoryTheory.ModObj M X] (Z : C) : MulAction (Z ⟶ M) (Z ⟶ X)
CategoryTheory.Hom.add_mul 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {R : C} [CategoryTheory.RingObj R] {X : C} (a b c : X ⟶ R) : (a + b) * c = a * c + b * c
CategoryTheory.Hom.mul_add 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {R : C} [CategoryTheory.RingObj R] {X : C} (a b c : X ⟶ R) : a * (b + c) = a * b + a * c
CategoryTheory.add_mul_iff 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (R : C) [CategoryTheory.MonObj R] [CategoryTheory.AddMonObj R] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R) CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R) CategoryTheory.MonObj.mul)) CategoryTheory.AddMonObj.add ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
CategoryTheory.mul_add_iff 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (R : C) [CategoryTheory.MonObj R] [CategoryTheory.AddMonObj R] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.AddMonObj.add) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.fst R R)) CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.snd R R)) CategoryTheory.MonObj.mul)) CategoryTheory.AddMonObj.add ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c

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