Loogle!
Result
Found 45 declarations mentioning CategoryTheory.Limits.coprod.map.
- CategoryTheory.Limits.coprod.map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨿ X ⟶ Y ⨿ Z - CategoryTheory.Limits.coprod.map_id_id 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X ⨿ Y) - CategoryTheory.Limits.isIso_coprod 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] : CategoryTheory.IsIso (CategoryTheory.Limits.coprod.map f g) - CategoryTheory.Limits.coprod.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Epi f] [CategoryTheory.Epi g] [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] : CategoryTheory.Epi (CategoryTheory.Limits.coprod.map f g) - CategoryTheory.Limits.coprod.map_codiag 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasBinaryCoproduct X X] [CategoryTheory.Limits.HasBinaryCoproduct Y Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f f) (CategoryTheory.Limits.codiag Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) f - CategoryTheory.Limits.coprod.mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.coprod.mapIso f g).hom = CategoryTheory.Limits.coprod.map f.hom g.hom - CategoryTheory.Limits.coprod.mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.coprod.mapIso f g).inv = CategoryTheory.Limits.coprod.map f.inv g.inv - CategoryTheory.Limits.coprod.inl_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.map f g) = CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl - CategoryTheory.Limits.coprod.inr_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.map f g) = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr - CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W Y] [CategoryTheory.Limits.HasBinaryCoproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) : CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr) = CategoryTheory.Limits.coprod.map g g' - CategoryTheory.Limits.coprod.map_codiag_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasBinaryCoproduct X X] [CategoryTheory.Limits.HasBinaryCoproduct Y Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) (CategoryTheory.CategoryStruct.comp f h) - CategoryTheory.Limits.coprod.map_inl_inr_codiag 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) (CategoryTheory.Limits.codiag (X ⨿ Y)) = CategoryTheory.CategoryStruct.id (X ⨿ Y) - CategoryTheory.Limits.coprod.map_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T U V W : C} [CategoryTheory.Limits.HasBinaryCoproduct U W] [CategoryTheory.Limits.HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) (CategoryTheory.Limits.coprod.desc f g) = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp k g) - CategoryTheory.Limits.coprod.inl_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⨿ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h) - CategoryTheory.Limits.coprod.inr_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⨿ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h) - CategoryTheory.Limits.coprod.map_comp_id 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct Z W] [CategoryTheory.Limits.HasBinaryCoproduct Y W] [CategoryTheory.Limits.HasBinaryCoproduct X W] : CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id W)) - CategoryTheory.Limits.coprod.map_id_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct W Y] [CategoryTheory.Limits.HasBinaryCoproduct W Z] : CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) f) (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) g) - CategoryTheory.Limits.coprod.functor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.Limits.coprod.functor.obj X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g - CategoryTheory.Limits.coprod.map_inl_inr_codiag_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag (X ⨿ Y)) h) = h - CategoryTheory.Limits.coprod.map_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂] [CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.Limits.coprod.map h k) = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k) - CategoryTheory.Limits.coprod.map_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {S T U V W : C} [CategoryTheory.Limits.HasBinaryCoproduct U W] [CategoryTheory.Limits.HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) {Z : C} (h✝ : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp k g)) h✝ - CategoryTheory.Limits.coprod.map_comp_id_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct Z W] [CategoryTheory.Limits.HasBinaryCoproduct Y W] [CategoryTheory.Limits.HasBinaryCoproduct X W] {Z✝ : C} (h : Z ⨿ W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id W)) h) - CategoryTheory.Limits.coprod.map_id_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryCoproduct W X] [CategoryTheory.Limits.HasBinaryCoproduct W Y] [CategoryTheory.Limits.HasBinaryCoproduct W Z] {Z✝ : C} (h : W ⨿ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) g) h) - CategoryTheory.Limits.coprod.map_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂] [CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {Z : C} (h✝ : A₃ ⨿ B₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)) h✝ - CategoryTheory.Limits.coprod.functor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (CategoryTheory.Limits.coprod.functor.map f).app T = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id T) - CategoryTheory.Limits.coprod.map_swap 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f) (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id A)) (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id Y) f) - CategoryTheory.Limits.coprod.map_swap_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] {Z : C} (h : Y ⨿ B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id B)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id Y) f) h) - CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr)) (CategoryTheory.Limits.codiag (Y ⨿ Y')) = CategoryTheory.Limits.coprod.map g g' - CategoryTheory.Limits.coprodComparison_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) (F.map (CategoryTheory.Limits.coprod.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) (CategoryTheory.Limits.coprodComparison F A' B') - CategoryTheory.Limits.coprod.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X (⊥_ C) Y).hom (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.coprod.leftUnitor Y).hom) = CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y) - CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨿ Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag (Y ⨿ Y')) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g g') h - CategoryTheory.Limits.coprodComparison_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj (A' ⨿ B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A' B') h) - CategoryTheory.Over.coprod_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) (g : CategoryTheory.Over A) : (CategoryTheory.Over.coprod.map k).app g = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map k.left (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj g.left))) ⋯ - CategoryTheory.Limits.coprodComparison_inv_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B')) - CategoryTheory.Limits.coprod.associator_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.map f₁ f₂) f₃) (CategoryTheory.Limits.coprod.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X₁ X₂ X₃).hom (CategoryTheory.Limits.coprod.map f₁ (CategoryTheory.Limits.coprod.map f₂ f₃)) - CategoryTheory.Limits.coprodComparison_inv_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] {Z : D} (h : F.obj A' ⨿ F.obj B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B')) h) - CategoryTheory.Over.coprodObj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (a✝ : CategoryTheory.Over A) {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) : a✝.coprodObj.map k = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj a✝.left)) k.left) ⋯ - CategoryTheory.Limits.coprod.pentagon 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator W (X ⨿ Y) Z).hom (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.coprod.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator (W ⨿ X) Y Z).hom (CategoryTheory.Limits.coprod.associator W X (Y ⨿ Z)).hom - CategoryTheory.Limits.coprod.map_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono f] [CategoryTheory.Mono g] [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] : CategoryTheory.Mono (CategoryTheory.Limits.coprod.map f g) - CategoryTheory.coprodMonad_map 📋 Mathlib.CategoryTheory.Monad.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.coprodMonad X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g - CategoryTheory.coprodComparison_tensorLeft_braiding_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.BraidedCategory C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z) (β_ X (Y ⨿ Z)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ X Y).hom (β_ X Z).hom) (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z) - CategoryTheory.coprodComparison_tensorRight_braiding_hom 📋 Mathlib.CategoryTheory.Distributive.Monoidal
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C] {X Y Z : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z) (β_ (Y ⨿ Z) X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ Y X).hom (β_ Z X).hom) (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z) - CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f - CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Z) - CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom 📋 Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.Limits.coprod.map f g
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. 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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
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.
This is Loogle revision 19971e9 serving mathlib revision 40fea08