Loogle!

Result

Found 27 declarations mentioning CategoryTheory.Limits.biprod.map.

• CategoryTheory.Limits.biprod.map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⊞ X ⟶ Y ⊞ Z
• CategoryTheory.Limits.biprod.map_epi 📋 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.Epi f] [CategoryTheory.Epi g] [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] : CategoryTheory.Epi (CategoryTheory.Limits.biprod.map f g)
• CategoryTheory.Limits.biprod.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.biprod.map f g)
• CategoryTheory.Limits.biprod.map_eq_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.Limits.biprod.map f g = CategoryTheory.Limits.biprod.map' f g
• CategoryTheory.isIso_left_of_isIso_biprod_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)] : CategoryTheory.IsIso f
• CategoryTheory.isIso_right_of_isIso_biprod_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)] : CategoryTheory.IsIso g
• CategoryTheory.Limits.biprod.mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.biprod.mapIso f g).hom = CategoryTheory.Limits.biprod.map f.hom g.hom
• CategoryTheory.Limits.biprod.mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (CategoryTheory.Limits.biprod.mapIso f g).inv = CategoryTheory.Limits.biprod.map f.inv g.inv
• CategoryTheory.Limits.biprod.inl_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.map f g) = CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl
• CategoryTheory.Limits.biprod.inr_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.map f g) = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr
• CategoryTheory.Limits.biprod.map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f
• CategoryTheory.Limits.biprod.map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
• CategoryTheory.Limits.biprod.inl_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⊞ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)
• CategoryTheory.Limits.biprod.inr_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⊞ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)
• CategoryTheory.Limits.biprod.map_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.biprod.map_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.biprod.braid_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.Limits.biprod.braiding Y W).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom (CategoryTheory.Limits.biprod.map g f)
• CategoryTheory.Limits.biprod.braiding_map_braiding 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X W).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.Limits.biprod.braiding Y Z).hom) = CategoryTheory.Limits.biprod.map g f
• CategoryTheory.Limits.biprod.braid_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⊞ Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding Y W).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map g f) h)
• CategoryTheory.Limits.biprod.braiding_map_braiding_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Z ⊞ Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X W).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding Y Z).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map g f) h
• CategoryTheory.Limits.biprod.associator_inv_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)) (CategoryTheory.Limits.biprod.associator X Y Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
• CategoryTheory.Limits.biprod.associator_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h) (CategoryTheory.Limits.biprod.associator X Y Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
• CategoryTheory.Limits.biprod.associator_inv_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) {Z✝ : C} (h✝ : (X ⊞ Y) ⊞ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator X Y Z).inv h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h) h✝)
• CategoryTheory.Limits.biprod.associator_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) {Z✝ : C} (h✝ : X ⊞ Y ⊞ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator X Y Z).hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)) h✝)
• CategoryTheory.Biprod.gaussian' 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) [CategoryTheory.IsIso f₁₁] : (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×' (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) R.hom) = CategoryTheory.Limits.biprod.map f₁₁ g₂₂
• CategoryTheory.Limits.biprod.map_eq 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.biprod.map f g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl) + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr)
• CategoryTheory.Biprod.gaussian 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))] : (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×' (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp f R.hom) = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) 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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

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