Loogle!

Result

Found 91 declarations mentioning CategoryTheory.Prod.mkHom.

CategoryTheory.Prod.mkHom 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] {X₁ X₂ : C} {Y₁ Y₂ : D} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (X₁, Y₁) ⟶ (X₂, Y₂)
CategoryTheory.prod_id 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C) (Y : D) : CategoryTheory.CategoryStruct.id (X, Y) = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)
CategoryTheory.Prod.sectL_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (Z : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.sectL C Z).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Z)
CategoryTheory.Prod.sectR_map 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.sectR Z D).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id Z) f
CategoryTheory.Iso.prod_hom 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (f.prod g).hom = CategoryTheory.Prod.mkHom f.hom g.hom
CategoryTheory.Iso.prod_inv 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (f.prod g).inv = CategoryTheory.Prod.mkHom f.inv g.inv
CategoryTheory.Functor.diag_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Functor.diag C).map f = CategoryTheory.Prod.mkHom f f
CategoryTheory.Prod.mkHom_eq 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] {X₁ X₂ : C} {Y₁ Y₂ : D} (f f' : X₁ ⟶ X₂) (g g' : Y₁ ⟶ Y₂) : CategoryTheory.Prod.mkHom f g = CategoryTheory.Prod.mkHom f' g' ↔ f = f' ∧ g = g'
CategoryTheory.prod.etaIso_hom 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.prod.etaIso X).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.prod.etaIso_inv 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.prod.etaIso X).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.Functor.prod'_map 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) : (F.prod' G).map f = CategoryTheory.Prod.mkHom (F.map f) (G.map f)
CategoryTheory.Prod.swap_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.swap C D).map f = CategoryTheory.Prod.mkHom f.2 f.1
CategoryTheory.Prod.fac 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id x.1) f.2) (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id y.2))
CategoryTheory.Prod.fac' 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id x.2)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id y.1) f.2)
CategoryTheory.Prod.fac'_assoc 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id x.2)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id y.1) f.2) h)
CategoryTheory.Prod.fac_assoc 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id x.1) f.2) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id y.2)) h)
CategoryTheory.Functor.prod_map 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D) {X✝ Y✝ : A × C} (f : X✝ ⟶ Y✝) : (F.prod G).map f = CategoryTheory.Prod.mkHom (F.map f.1) (G.map f.2)
CategoryTheory.prod_comp 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.comp f.1 g.1) (CategoryTheory.CategoryStruct.comp f.2 g.2)
CategoryTheory.prodOpEquiv_functor_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {X✝ Y✝ : (C × D)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.prodOpEquiv C).functor.map f = CategoryTheory.Prod.mkHom f.unop.1.op f.unop.2.op
CategoryTheory.functorProdToProdFunctor_map 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X✝ Y✝ : CategoryTheory.Functor A (B × C)} (α : X✝ ⟶ Y✝) : (CategoryTheory.functorProdToProdFunctor A B C).map α = CategoryTheory.Prod.mkHom (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Prod.fst B C)) (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Prod.snd B C))
CategoryTheory.prodOpEquiv_inverse_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {X✝ Y✝ : Cᵒᵖ × Dᵒᵖ} (x✝ : X✝ ⟶ Y✝) : (CategoryTheory.prodOpEquiv C).inverse.map x✝ = match x✝ with | (f, g) => Opposite.op (CategoryTheory.Prod.mkHom f.unop g.unop)
CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).hom.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X✝).1) (CategoryTheory.CategoryStruct.id (X.obj X✝).2)
CategoryTheory.functorProdFunctorEquivCounitIso_inv_app_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).inv.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X✝).1) (CategoryTheory.CategoryStruct.id (X.obj X✝).2)
CategoryTheory.functorProdFunctorEquivUnitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A B × CategoryTheory.Functor A C) : (CategoryTheory.functorProdFunctorEquivUnitIso A B C).hom.app X = CategoryTheory.Prod.mkHom (X.1.prod'CompFst X.2).inv (X.1.prod'CompSnd X.2).inv
CategoryTheory.functorProdFunctorEquivUnitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A B × CategoryTheory.Functor A C) : (CategoryTheory.functorProdFunctorEquivUnitIso A B C).inv.app X = CategoryTheory.Prod.mkHom (X.1.prod'CompFst X.2).hom (X.1.prod'CompSnd X.2).hom
CategoryTheory.prodOpEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : Cᵒᵖ × Dᵒᵖ) : (CategoryTheory.prodOpEquiv C).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.prodOpEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : Cᵒᵖ × Dᵒᵖ) : (CategoryTheory.prodOpEquiv C).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.prod.leftInverseUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.leftInverseUnitor C).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id { as := PUnit.unit }) f
CategoryTheory.prod.rightInverseUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.rightInverseUnitor C).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id { as := PUnit.unit })
CategoryTheory.Comma.equivProd_functor_map 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.equivProd L R).functor.map f = CategoryTheory.Prod.mkHom f.left f.right
CategoryTheory.Comma.equivProd_counitIso_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.Comma.equivProd_counitIso_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.Functor.curry_obj_obj_map 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.curry.obj F).obj X).map g = F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
CategoryTheory.Functor.currying_inverse_obj_obj_map 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.currying.inverse.obj F).obj X).map g = F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
CategoryTheory.Functor.curryingEquiv_symm_apply_obj_map 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (G : CategoryTheory.Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.curryingEquiv.symm G).obj X).map g = G.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
CategoryTheory.Functor.curry_obj_map_app 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((CategoryTheory.Functor.curry.obj F).map f).app Y = F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y))
CategoryTheory.Functor.currying_inverse_obj_map_app 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((CategoryTheory.Functor.currying.inverse.obj F).map f).app Y = F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y))
CategoryTheory.Functor.curryingEquiv_symm_apply_map_app 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (G : CategoryTheory.Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((CategoryTheory.Functor.curryingEquiv.symm G).map f).app Y = G.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y))
CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_map 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (a✝ : CategoryTheory.Functor (C × D) E) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.curryingFlipEquiv.symm a✝).obj k).map f = a✝.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id k))
CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app 📋 Mathlib.CategoryTheory.Functor.Currying
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (a✝ : CategoryTheory.Functor (C × D) E) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : ((CategoryTheory.Functor.curryingFlipEquiv.symm a✝).map f).app j = a✝.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id j) f)
CategoryTheory.Functor.whiskeringRight₂_obj_map_app_app 📋 Mathlib.CategoryTheory.Functor.Currying
(B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X✝ Y✝ : CategoryTheory.Functor B C} (f : X✝ ⟶ Y✝) (Y : CategoryTheory.Functor B D) (X✝¹ : B) : ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).map f).app Y).app X✝¹ = (X.map (f.app X✝¹)).app (Y.obj X✝¹)
CategoryTheory.MonoidalCategory.prodMonoidal_whiskerLeft 📋 Mathlib.CategoryTheory.Monoidal.Category
(C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X x✝ x✝¹ : C₁ × C₂) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.1 f.1) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.2 f.2)
CategoryTheory.MonoidalCategory.prodMonoidal_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Category
(C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] {X₁✝ X₂✝ : C₁ × C₂} (f : X₁✝ ⟶ X₂✝) (X : C₁ × C₂) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.1 X.1) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.2 X.2)
CategoryTheory.MonoidalCategory.prodMonoidal_tensorHom 📋 Mathlib.CategoryTheory.Monoidal.Category
(C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] {X₁✝ Y₁✝ X₂✝ Y₂✝ : C₁ × C₂} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f.1 g.1) (CategoryTheory.MonoidalCategoryStruct.tensorHom f.2 g.2)
CategoryTheory.Bifunctor.map_id 📋 Mathlib.CategoryTheory.Products.Bifunctor
{C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) : F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)) = CategoryTheory.CategoryStruct.id (F.obj (X, Y))
CategoryTheory.Bifunctor.diagonal 📋 Mathlib.CategoryTheory.Products.Bifunctor
{C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor (C × D) E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)) (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y'))) = F.map (CategoryTheory.Prod.mkHom f g)
CategoryTheory.Bifunctor.diagonal' 📋 Mathlib.CategoryTheory.Products.Bifunctor
{C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor (C × D) E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y))) (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X') g)) = F.map (CategoryTheory.Prod.mkHom f g)
CategoryTheory.Bifunctor.map_comp_id 📋 Mathlib.CategoryTheory.Products.Bifunctor
{C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor (C × D) E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z) : F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id W))) (F.map (CategoryTheory.Prod.mkHom g (CategoryTheory.CategoryStruct.id W)))
CategoryTheory.Bifunctor.map_id_comp 📋 Mathlib.CategoryTheory.Products.Bifunctor
{C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor (C × D) E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) : F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id W) f)) (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id W) g))
CategoryTheory.prod.associator_map 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (x✝ x✝¹ : (C × D) × E) (f : x✝ ⟶ x✝¹) : (CategoryTheory.prod.associator C D E).map f = CategoryTheory.Prod.mkHom f.1.1 (CategoryTheory.Prod.mkHom f.1.2 f.2)
CategoryTheory.prod.inverseAssociator_map 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (x✝ x✝¹ : C × D × E) (f : x✝ ⟶ x✝¹) : (CategoryTheory.prod.inverseAssociator C D E).map f = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1 f.2.1) f.2.2
CategoryTheory.prod.prodμ_functor_map 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] {X✝ Y✝ : (A × C) × D × E} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.prodμ C D E A).functor.map f = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1.1 f.2.1) (CategoryTheory.Prod.mkHom f.1.2 f.2.2)
CategoryTheory.prod.prodμ_inverse_map 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] {X✝ Y✝ : (A × D) × C × E} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.prodμ C D E A).inverse.map f = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1.1 f.2.1) (CategoryTheory.Prod.mkHom f.1.2 f.2.2)
CategoryTheory.prod.prodμ_counitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : (A × D) × C × E) : (CategoryTheory.prod.prodμ C D E A).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
CategoryTheory.prod.prodμ_counitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : (A × D) × C × E) : (CategoryTheory.prod.prodμ C D E A).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
CategoryTheory.prod.prodμ_unitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : (A × C) × D × E) : (CategoryTheory.prod.prodμ C D E A).unitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
CategoryTheory.prod.prodμ_unitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : (A × C) × D × E) : (CategoryTheory.prod.prodμ C D E A).unitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
CategoryTheory.prod.functorProdToProdFunctorAssociator_hom_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : CategoryTheory.Functor A ((C × D) × E)) : (CategoryTheory.prod.functorProdToProdFunctorAssociator C D E A).hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id ((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.fst C (D × E)))) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp (CategoryTheory.Prod.fst D E))) (CategoryTheory.CategoryStruct.id (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp (CategoryTheory.Prod.snd D E))))
CategoryTheory.prod.functorProdToProdFunctorAssociator_inv_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : CategoryTheory.Functor A ((C × D) × E)) : (CategoryTheory.prod.functorProdToProdFunctorAssociator C D E A).inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id ((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.fst C (D × E)))) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp (CategoryTheory.Prod.fst D E))) (CategoryTheory.CategoryStruct.id (((X.comp (CategoryTheory.prod.associator C D E)).comp (CategoryTheory.Prod.snd C (D × E))).comp (CategoryTheory.Prod.snd D E))))
CategoryTheory.prod.prodFunctorToFunctorProdAssociator_hom_app_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : (CategoryTheory.Functor A C × CategoryTheory.Functor A D) × CategoryTheory.Functor A E) (X✝ : A) : ((CategoryTheory.prod.prodFunctorToFunctorProdAssociator C D E A).hom.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.1.obj X✝)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.2.obj X✝)) (CategoryTheory.CategoryStruct.id (X.2.obj X✝)))
CategoryTheory.prod.prodFunctorToFunctorProdAssociator_inv_app_app 📋 Mathlib.CategoryTheory.Products.Associator
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄) [CategoryTheory.Category.{v₄, u₄} A] (X : (CategoryTheory.Functor A C × CategoryTheory.Functor A D) × CategoryTheory.Functor A E) (X✝ : A) : ((CategoryTheory.prod.prodFunctorToFunctorProdAssociator C D E A).inv.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.1.obj X✝)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.2.obj X✝)) (CategoryTheory.CategoryStruct.id (X.2.obj X✝)))
CategoryTheory.Limits.map_id_left_eq_curry_map 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
{J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) {j : J} {k k' : K} {f : k ⟶ k'} : F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id j) f) = ((CategoryTheory.Functor.curry.obj F).obj j).map f
CategoryTheory.Limits.map_id_right_eq_curry_swap_map 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
{J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) {j j' : J} {f : j ⟶ j'} {k : K} : F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id k)) = ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k).map f
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
{X Y : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} (e : SSet.Truncated.Edge x₀ x₁) (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })) : (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map (CategoryTheory.Prod.mkHom (SSet.Truncated.HomotopyCategory.homMk e) (CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk y))) = SSet.Truncated.HomotopyCategory.homMk (e.tensor (SSet.Truncated.Edge.id y))
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
{X Y : SSet.Truncated 2} (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })) {y₀ y₁ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} (e : SSet.Truncated.Edge y₀ y₁) : (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk x)) (SSet.Truncated.HomotopyCategory.homMk e)) = SSet.Truncated.HomotopyCategory.homMk ((SSet.Truncated.Edge.id x).tensor e)
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
{X Y : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} (e : SSet.Truncated.Edge x₀ x₁) {y₀ y₁ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} (e' : SSet.Truncated.Edge y₀ y₁) : (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map (CategoryTheory.Prod.mkHom (SSet.Truncated.HomotopyCategory.homMk e) (SSet.Truncated.HomotopyCategory.homMk e')) = SSet.Truncated.HomotopyCategory.homMk (e.tensor e')
CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((CategoryTheory.curryingIso.inv.toFunctor.obj F).obj X).map g = F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
CategoryTheory.curryingIso_inv_toFunctor_obj_map_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((CategoryTheory.curryingIso.inv.toFunctor.obj F).map f).app Y = F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y))
CategoryTheory.Bicategory.Prod.sectR_map 📋 Mathlib.CategoryTheory.Bicategory.Product
{B : Type u₁} [CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [CategoryTheory.Bicategory C] {X✝ Y✝ : C} (a✝ : X✝ ⟶ Y✝) : (CategoryTheory.Bicategory.Prod.sectR b C).map a✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id b) a✝
CategoryTheory.Bicategory.Prod.sectL_map 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (c : C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : (CategoryTheory.Bicategory.Prod.sectL B c).map a✝ = CategoryTheory.Prod.mkHom a✝ (CategoryTheory.CategoryStruct.id c)
CategoryTheory.Bicategory.Prod.swap_map 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {X✝ Y✝ : B × C} (a✝ : X✝ ⟶ Y✝) : (CategoryTheory.Bicategory.Prod.swap B C).map a✝ = CategoryTheory.Prod.mkHom a✝.2 a✝.1
CategoryTheory.Bicategory.Prod.sectR_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Product
{B : Type u₁} [CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ : C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (CategoryTheory.Bicategory.Prod.sectR b C).map₂ a✝¹ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) a✝¹
CategoryTheory.Bicategory.Prod.sectR_mapComp_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
{B : Type u₁} [CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ c✝ : C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.sectR b C).mapComp f g).hom = CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id b)).inv (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
CategoryTheory.Bicategory.Prod.sectR_mapComp_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
{B : Type u₁} [CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ c✝ : C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.sectR b C).mapComp f g).inv = CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
CategoryTheory.Bicategory.Prod.sectL_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (c : C) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (CategoryTheory.Bicategory.Prod.sectL B c).map₂ a✝¹ = CategoryTheory.Prod.mkHom a✝¹ (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c))
CategoryTheory.Bicategory.Prod.sectL_mapComp_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (c : C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.sectL B c).mapComp f g).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id c)).inv
CategoryTheory.Bicategory.Prod.sectL_mapComp_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (c : C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.sectL B c).mapComp f g).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id c)).hom
CategoryTheory.Bicategory.Prod.swap_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (CategoryTheory.Bicategory.Prod.swap B C).map₂ a✝¹ = CategoryTheory.Prod.mkHom a✝¹.2 a✝¹.1
CategoryTheory.Bicategory.Prod.sectR_mapId_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
{B : Type u₁} [CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [CategoryTheory.Bicategory C] (x : C) : ((CategoryTheory.Bicategory.Prod.sectR b C).mapId x).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x))
CategoryTheory.Bicategory.Prod.sectR_mapId_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
{B : Type u₁} [CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [CategoryTheory.Bicategory C] (x : C) : ((CategoryTheory.Bicategory.Prod.sectR b C).mapId x).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x))
CategoryTheory.Bicategory.Prod.sectL_mapId_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (c : C) (x : B) : ((CategoryTheory.Bicategory.Prod.sectL B c).mapId x).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c))
CategoryTheory.Bicategory.Prod.sectL_mapId_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (c : C) (x : B) : ((CategoryTheory.Bicategory.Prod.sectL B c).mapId x).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c))
CategoryTheory.Bicategory.Prod.swap_mapId_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (x : B × C) : ((CategoryTheory.Bicategory.Prod.swap B C).mapId x).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1))
CategoryTheory.Bicategory.Prod.swap_mapId_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (x : B × C) : ((CategoryTheory.Bicategory.Prod.swap B C).mapId x).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1))
CategoryTheory.Bicategory.Prod.swap_mapComp_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.swap B C).mapComp f g).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.2 g.2)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1))
CategoryTheory.Bicategory.Prod.swap_mapComp_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
(B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.swap B C).mapComp f g).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.2 g.2)) (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1))
CategoryTheory.Discrete.productEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
{J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K) : CategoryTheory.Discrete.productEquiv.counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.Discrete.productEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
{J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K) : CategoryTheory.Discrete.productEquiv.counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
CategoryTheory.Sum.functorEquiv_functor_map 📋 Mathlib.CategoryTheory.Sums.Products
(A : Type u_1) [CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2) [CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [CategoryTheory.Category.{v, u} B] {X✝ Y✝ : CategoryTheory.Functor (A ⊕ A') B} (η : X✝ ⟶ Y✝) : (CategoryTheory.Sum.functorEquiv A A' B).functor.map η = CategoryTheory.Prod.mkHom ((CategoryTheory.Sum.inl_ A A').whiskerLeft η) ((CategoryTheory.Sum.inr_ A A').whiskerLeft η)
CategoryTheory.Sum.functorEquiv_unitIso 📋 Mathlib.CategoryTheory.Sums.Products
(A : Type u_1) [CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2) [CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [CategoryTheory.Category.{v, u} B] : (CategoryTheory.Sum.functorEquiv A A' B).unitIso = CategoryTheory.NatIso.ofComponents (fun F => F.isoSum) ⋯
CategoryTheory.Sum.functorEquiv_counitIso 📋 Mathlib.CategoryTheory.Sums.Products
(A : Type u_1) [CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2) [CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [CategoryTheory.Category.{v, u} B] : (CategoryTheory.Sum.functorEquiv A A' B).counitIso = CategoryTheory.NatIso.ofComponents (fun F => (F.1.inlCompSum' F.2).prod (F.1.inrCompSum' F.2) ≪≫ CategoryTheory.prod.etaIso F) ⋯

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