Loogle!

Result

Found 146 declarations mentioning CategoryTheory.Limits.HasFiniteBiproducts.

CategoryTheory.Limits.HasFiniteBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
(C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop
CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
(C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasFiniteCoproducts C
CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
(C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasFiniteProducts C
CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasZeroObject C
CategoryTheory.Limits.HasFiniteBiproducts.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (out : ∀ (n : ℕ), CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C) : CategoryTheory.Limits.HasFiniteBiproducts C
CategoryTheory.Limits.HasFiniteBiproducts.out 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type uC} {inst✝ : CategoryTheory.Category.{uC', uC} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.Limits.HasFiniteBiproducts C] (n : ℕ) : CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C
CategoryTheory.Limits.hasBiproductsOfShape_finite 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type w} (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite J] : CategoryTheory.Limits.HasBiproductsOfShape J C
CategoryTheory.Limits.biproduct.matrix_components 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J) (k : K) : CategoryTheory.Limits.biproduct.components (CategoryTheory.Limits.biproduct.matrix m) j k = m j k
CategoryTheory.Limits.biproduct.components 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : ⨁ f ⟶ ⨁ g) (j : J) (k : K) : f j ⟶ g k
CategoryTheory.Limits.biproduct.matrix 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) : ⨁ f ⟶ ⨁ g
CategoryTheory.Limits.biproduct.matrixEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} : (⨁ f ⟶ ⨁ g) ≃ ((j : J) → (k : K) → f j ⟶ g k)
CategoryTheory.Limits.instHasCokernelFromSubtype 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.biproduct.fromSubtype f p)
CategoryTheory.Limits.instHasKernelToSubtype 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.biproduct.toSubtype f p)
CategoryTheory.Limits.biproduct.components_matrix 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : ⨁ f ⟶ ⨁ g) : (CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.Limits.biproduct.components m j k) = m
CategoryTheory.Limits.biproduct.matrix_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.Limits.biproduct.π g k) = CategoryTheory.Limits.biproduct.desc fun j => m j k
CategoryTheory.Limits.biproduct.ι_matrix 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.matrix m) = CategoryTheory.Limits.biproduct.lift fun k => m j k
CategoryTheory.Limits.cokernelBiproductFromSubtypeIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : CategoryTheory.Limits.cokernel (CategoryTheory.Limits.biproduct.fromSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f
CategoryTheory.Limits.kernelBiproductToSubtypeIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : CategoryTheory.Limits.kernel (CategoryTheory.Limits.biproduct.toSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f
CategoryTheory.Limits.biproduct.matrix_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (k : K) {Z : C} (h : g k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc fun j => m j k) h
CategoryTheory.Limits.biproduct.ι_matrix_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J) {Z : C} (h : ⨁ g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift fun k => m j k) h
CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0)
CategoryTheory.Limits.kernelForkBiproductToSubtype 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0)
CategoryTheory.Limits.biproduct.matrixEquiv_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : ⨁ f ⟶ ⨁ g) (j : J) (k : K) : CategoryTheory.Limits.biproduct.matrixEquiv m j k = CategoryTheory.Limits.biproduct.components m j k
CategoryTheory.Limits.biproduct.matrixEquiv_symm_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) : CategoryTheory.Limits.biproduct.matrixEquiv.symm m = CategoryTheory.Limits.biproduct.matrix m
CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).cocone = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯
CategoryTheory.Limits.kernelForkBiproductToSubtype_cone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.kernelForkBiproductToSubtype f p).cone = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯
CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).isColimit = CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯ ⋯
CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.kernelForkBiproductToSubtype f p).isLimit = CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯
CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯)
CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯)
CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).inv = (CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯ ⋯).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0))
CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).hom = (CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0))
CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
(C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasBinaryBiproducts C
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Limits.HasFiniteBiproducts C
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.Limits.HasFiniteBiproducts C
CategoryTheory.Limits.biproduct.lift_matrix 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type} [Fintype J] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} {P : C} (x : (j : J) → P ⟶ f j) (m : (j : J) → (k : K) → f j ⟶ g k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift x) (CategoryTheory.Limits.biproduct.matrix m) = CategoryTheory.Limits.biproduct.lift fun k => ∑ j, CategoryTheory.CategoryStruct.comp (x j) (m j k)
CategoryTheory.Limits.biproduct.matrix_desc 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J K : Type} [Finite J] [CategoryTheory.Limits.HasFiniteBiproducts C] [Fintype K] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) {P : C} (x : (k : K) → g k ⟶ P) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.Limits.biproduct.desc x) = CategoryTheory.Limits.biproduct.desc fun j => ∑ k, CategoryTheory.CategoryStruct.comp (m j k) (x k)
CategoryTheory.Limits.biproduct.map_matrix 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J K : Type} [Finite J] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite K] {f g : J → C} {h : K → C} (m : (k : J) → f k ⟶ g k) (n : (j : J) → (k : K) → g j ⟶ h k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map m) (CategoryTheory.Limits.biproduct.matrix n) = CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j) (n j k)
CategoryTheory.Limits.biproduct.matrix_map 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J K : Type} [Finite J] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite K] {f : J → C} {g h : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (n : (k : K) → g k ⟶ h k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.Limits.biproduct.map n) = CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j k) (n k)
CategoryTheory.Limits.biproduct.lift_matrix_assoc 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type} [Fintype J] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} {P : C} (x : (j : J) → P ⟶ f j) (m : (j : J) → (k : K) → f j ⟶ g k) {Z : C} (h : ⨁ g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift x) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift fun k => ∑ j, CategoryTheory.CategoryStruct.comp (x j) (m j k)) h
CategoryTheory.Limits.biproduct.matrix_desc_assoc 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J K : Type} [Finite J] [CategoryTheory.Limits.HasFiniteBiproducts C] [Fintype K] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) {P : C} (x : (k : K) → g k ⟶ P) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc x) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc fun j => ∑ k, CategoryTheory.CategoryStruct.comp (m j k) (x k)) h
CategoryTheory.Limits.biproduct.map_matrix_assoc 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J K : Type} [Finite J] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite K] {f g : J → C} {h : K → C} (m : (k : J) → f k ⟶ g k) (n : (j : J) → (k : K) → g j ⟶ h k) {Z : C} (h✝ : ⨁ h ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j) (n j k)) h✝
CategoryTheory.Limits.biproduct.matrix_map_assoc 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J K : Type} [Finite J] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite K] {f : J → C} {g h : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (n : (k : K) → g k ⟶ h k) {Z : C} (h✝ : ⨁ h ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j k) (n k)) h✝
CategoryTheory.Limits.biproduct.map_eq 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type} [Fintype J] [CategoryTheory.Limits.HasFiniteBiproducts C] {f g : J → C} {h : (j : J) → f j ⟶ g j} : CategoryTheory.Limits.biproduct.map h = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.CategoryStruct.comp (h j) (CategoryTheory.Limits.biproduct.ι g j))
CategoryTheory.leftDistributor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ≅ ⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)
CategoryTheory.rightDistributor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ≅ ⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X
CategoryTheory.biproduct_ι_comp_leftDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryTheory.leftDistributor X f).inv = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)
CategoryTheory.biproduct_ι_comp_rightDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryTheory.rightDistributor f X).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X
CategoryTheory.leftDistributor_hom_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)
CategoryTheory.rightDistributor_hom_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X
CategoryTheory.biproduct_ι_comp_leftDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) (CategoryTheory.leftDistributor X f).hom = CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j
CategoryTheory.biproduct_ι_comp_rightDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) (CategoryTheory.rightDistributor f X).hom = CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j
CategoryTheory.leftDistributor_inv_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j
CategoryTheory.rightDistributor_inv_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) = CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j
CategoryTheory.leftDistributor_ext_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h) : g = h
CategoryTheory.leftDistributor_ext_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))) : g = h
CategoryTheory.rightDistributor_ext_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h) : g = h
CategoryTheory.rightDistributor_ext_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)) : g = h
CategoryTheory.leftDistributor_ext_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h
CategoryTheory.leftDistributor_ext_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))
CategoryTheory.rightDistributor_ext_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h
CategoryTheory.rightDistributor_ext_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)
CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h
CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h
CategoryTheory.leftDistributor_hom_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) h
CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) h
CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : (⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h
CategoryTheory.biproduct_ι_comp_rightDistributor_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : (⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h
CategoryTheory.leftDistributor_inv_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h
CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h
CategoryTheory.leftDistributor_ext₂_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) h) : g = h
CategoryTheory.leftDistributor_ext₂_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z (⨁ f))} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))) : g = h
CategoryTheory.rightDistributor_ext₂_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) h) : g = h
CategoryTheory.rightDistributor_ext₂_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)) : g = h
CategoryTheory.leftDistributor_ext₂_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) h
CategoryTheory.leftDistributor_ext₂_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z (⨁ f))} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))
CategoryTheory.rightDistributor_ext₂_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) h
CategoryTheory.rightDistributor_ext₂_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)
CategoryTheory.leftDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (CategoryTheory.leftDistributor X f).hom = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j)
CategoryTheory.leftDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (CategoryTheory.leftDistributor X f).inv = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j))
CategoryTheory.rightDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (CategoryTheory.rightDistributor f X).hom = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j)
CategoryTheory.rightDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (CategoryTheory.rightDistributor f X).inv = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X)
CategoryTheory.rightDistributor_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X Y : C) : CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.rightDistributor f X) (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫ CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) Y = CategoryTheory.MonoidalCategoryStruct.associator (⨁ f) X Y ≪≫ CategoryTheory.rightDistributor f (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≪≫ CategoryTheory.Limits.biproduct.mapIso fun x => (CategoryTheory.MonoidalCategoryStruct.associator (f x) X Y).symm
CategoryTheory.leftDistributor_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X Y : C) (f : J → C) : (CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.leftDistributor Y f) ≪≫ CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj Y (f j)) = (CategoryTheory.MonoidalCategoryStruct.associator X Y (⨁ f)).symm ≪≫ CategoryTheory.leftDistributor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f ≪≫ CategoryTheory.Limits.biproduct.mapIso fun x => CategoryTheory.MonoidalCategoryStruct.associator X Y (f x)
CategoryTheory.leftDistributor_rightDistributor_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (Y : C) : CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.leftDistributor X f) (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫ CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) Y = CategoryTheory.MonoidalCategoryStruct.associator X (⨁ f) Y ≪≫ CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.rightDistributor f Y) ≪≫ (CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) Y) ≪≫ CategoryTheory.Limits.biproduct.mapIso fun x => (CategoryTheory.MonoidalCategoryStruct.associator X (f x) Y).symm
CategoryTheory.Abelian.hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Abelian.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteBiproducts C
AddCommGrpCat.instHasFiniteBiproducts 📋 Mathlib.Algebra.Category.Grp.Biproducts
: CategoryTheory.Limits.HasFiniteBiproducts AddCommGrpCat
CategoryTheory.hasExactColimitsOfShape_discrete_finite 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (J : Type u_1) [Finite J] : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C
CategoryTheory.hasExactLimitsOfShape_discrete_finite 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type u_1} [Finite J] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C
CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasCountableCoproducts C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4 C
CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasCountableProducts C] [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4Star C
CategoryTheory.AB4.of_AB5 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5OfSize.{w, w, v, u} C] : CategoryTheory.AB4OfSize.{w, v, u} C
CategoryTheory.AB4Star.of_AB5Star 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5StarOfSize.{w, w, v, u} C] : CategoryTheory.AB4StarOfSize.{w, v, u} C
CategoryTheory.CountableAB4.of_countableAB5 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape ℕ C] [CategoryTheory.HasExactColimitsOfShape ℕ C] [CategoryTheory.Limits.HasCountableCoproducts C] : CategoryTheory.CountableAB4 C
CategoryTheory.CountableAB4Star.of_countableAB5Star 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape ℕᵒᵖ C] [CategoryTheory.Limits.HasCountableProducts C] : CategoryTheory.CountableAB4Star C
CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] (J : Type u_1) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete J)) C] [CategoryTheory.HasExactColimitsOfShape (Finset (CategoryTheory.Discrete J)) C] : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C
CategoryTheory.preservesFiniteLimits_liftToFinset 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α)
CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] (J : Type u_1) [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C
CategoryTheory.preservesFiniteColimits_liftToFinset 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α)
AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux 📋 Mathlib.Algebra.Category.Grp.LeftExactFunctor
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor (C ⥤ₗ Type v) (CategoryTheory.Functor C AddCommGrpCat)
AddCommGrpCat.leftExactFunctorForgetEquivalence 📋 Mathlib.Algebra.Category.Grp.LeftExactFunctor
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : C ⥤ₗ AddCommGrpCat ≌ C ⥤ₗ Type v
AddCommGrpCat.leftExactFunctorForgetEquivalence.inverse 📋 Mathlib.Algebra.Category.Grp.LeftExactFunctor
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor (C ⥤ₗ Type v) (C ⥤ₗ AddCommGrpCat)
AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux 📋 Mathlib.Algebra.Category.Grp.LeftExactFunctor
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (F : C ⥤ₗ Type v) : CategoryTheory.Limits.PreservesFiniteLimits (AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux.obj F)
AddCommGrpCat.leftExactFunctorForgetEquivalence.unitIso 📋 Mathlib.Algebra.Category.Grp.LeftExactFunctor
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor.id (C ⥤ₗ AddCommGrpCat) ≅ ((CategoryTheory.LeftExactFunctor.whiskeringRight C AddCommGrpCat (Type v)).obj (CategoryTheory.LeftExactFunctor.of (CategoryTheory.forget AddCommGrpCat))).comp AddCommGrpCat.leftExactFunctorForgetEquivalence.inverse
AddCommGrpCat.leftExactFunctorForgetEquivalence.unitIsoAux 📋 Mathlib.Algebra.Category.Grp.LeftExactFunctor
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (F : CategoryTheory.Functor C AddCommGrpCat) [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrpCat.toCommGrp.obj (F.obj X)) ≅ (F.comp (CategoryTheory.forget AddCommGrpCat)).mapCommGrp.obj (CategoryTheory.Preadditive.commGrpEquivalence.functor.obj X)
ModuleCat.instHasFiniteBiproducts 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
{R : Type u} [Ring R] : CategoryTheory.Limits.HasFiniteBiproducts (ModuleCat R)
CategoryTheory.Pretriangulated.instHasFiniteBiproducts 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] : CategoryTheory.Limits.HasFiniteBiproducts C
CategoryTheory.InjectiveObject.instHasFiniteBiproductsOfHasFiniteProducts 📋 Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.InjectiveObject C)
CategoryTheory.instHasFiniteBiproductsInd 📋 Mathlib.CategoryTheory.Preadditive.Indization
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)
CategoryTheory.Idempotents.Karoubi.karoubi_hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Idempotents.Karoubi C)
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.Limits.Bicone F
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_X 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) : (CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).pt.X = ⨁ fun j => (F j).X
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_p 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) : (CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).pt.p = CategoryTheory.Limits.biproduct.map fun j => (F j).p
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_ι_f 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) (j : J) : ((CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).ι j).f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => (F j).X) j) (CategoryTheory.Limits.biproduct.map fun j => (F j).p)
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_π_f 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) (j : J) : ((CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).π j).f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map fun j => (F j).p) ((CategoryTheory.Limits.biproduct.bicone fun j => (F j).X).π j)
CategoryTheory.Limits.SequentialProduct.functorMap_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
{C : Type u_1} {M N : ℕ → C} [CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [CategoryTheory.Limits.HasCountableProducts C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (n : ℕ), CategoryTheory.Epi (f n)] (n : ℕ) : CategoryTheory.Epi (CategoryTheory.Limits.SequentialProduct.functorMap f n)
CategoryTheory.HomOrthogonal.matrixDecomposition 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃ ((i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
CategoryTheory.HomOrthogonal.equiv_of_iso 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (i : ι), InvariantBasisNumber (CategoryTheory.End (s i))] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) : ∃ e, ∀ (a : α), g (e a) = f a
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+ ((i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {R : Type u_2} [Semiring R] [CategoryTheory.Linear R C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃ₗ[R] (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))
CategoryTheory.HomOrthogonal.matrixDecomposition_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι) (j : ↑(g ⁻¹' {i})) (k : ↑(f ⁻¹' {i})) : o.matrixDecomposition z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j) (CategoryTheory.eqToHom ⋯))
CategoryTheory.HomOrthogonal.matrixDecomposition_id 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α : Type} [Finite α] {f : α → ι} (i : ι) : o.matrixDecomposition (CategoryTheory.CategoryStruct.id (⨁ fun a => s (f a))) i = 1
CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))) : o.matrixDecomposition.symm z = CategoryTheory.Limits.biproduct.matrix fun j k => if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι) (j : ↑(g ⁻¹' {i})) (k : ↑(f ⁻¹' {i})) : o.matrixDecompositionAddEquiv z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j) (CategoryTheory.eqToHom ⋯))
CategoryTheory.HomOrthogonal.matrixDecomposition_comp 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β γ : Type} [Finite α] [Fintype β] [Finite γ] {f : α → ι} {g : β → ι} {h : γ → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)) (i : ι) : o.matrixDecomposition (CategoryTheory.CategoryStruct.comp z w) i = o.matrixDecomposition w i * o.matrixDecomposition z i
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {R : Type u_2} [Semiring R] [CategoryTheory.Linear R C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (a✝ : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι) : o.matrixDecompositionLinearEquiv a✝ i = o.matrixDecompositionAddEquiv.toFun a✝ i
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))) : o.matrixDecompositionAddEquiv.symm z = CategoryTheory.Limits.biproduct.matrix fun j k => if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply 📋 Mathlib.CategoryTheory.Preadditive.HomOrthogonal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C} [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {R : Type u_2} [Semiring R] [CategoryTheory.Linear R C] (o : CategoryTheory.HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι} (a✝ : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))) : o.matrixDecompositionLinearEquiv.symm a✝ = o.matrixDecompositionAddEquiv.invFun a✝
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts 📋 Mathlib.CategoryTheory.Preadditive.Mat
(C : Type (u₁ + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Mat_ C ≌ C
CategoryTheory.Mat_.hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Mat_ C)
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_inverse 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type (u₁ + 1)} [CategoryTheory.LargeCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : (CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).inverse = CategoryTheory.Mat_.embedding C
CategoryTheory.Mat_.lift 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (CategoryTheory.Mat_ C) D
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_functor 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type (u₁ + 1)} [CategoryTheory.LargeCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : (CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).functor = CategoryTheory.Mat_.lift (CategoryTheory.Functor.id C)
CategoryTheory.Mat_.lift_additive 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] : (CategoryTheory.Mat_.lift F).Additive
CategoryTheory.Mat_.embeddingLiftIso 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] : (CategoryTheory.Mat_.embedding C).comp (CategoryTheory.Mat_.lift F) ≅ F
CategoryTheory.Mat_.lift_obj 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] (X : CategoryTheory.Mat_ C) : (CategoryTheory.Mat_.lift F).obj X = ⨁ fun i => F.obj (X.X i)
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproductsAux 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : (CategoryTheory.Mat_.embedding C).comp (CategoryTheory.Functor.id (CategoryTheory.Mat_ C)) ≅ (CategoryTheory.Mat_.embedding C).comp ((CategoryTheory.Mat_.lift (CategoryTheory.Functor.id C)).comp (CategoryTheory.Mat_.embedding C))
CategoryTheory.Mat_.liftUnique 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] (L : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [L.Additive] (α : (CategoryTheory.Mat_.embedding C).comp L ≅ F) : L ≅ CategoryTheory.Mat_.lift F
CategoryTheory.Mat_.ext 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {F G : CategoryTheory.Functor (CategoryTheory.Mat_ C) D} [F.Additive] [G.Additive] (α : (CategoryTheory.Mat_.embedding C).comp F ≅ (CategoryTheory.Mat_.embedding C).comp G) : F ≅ G
CategoryTheory.Mat_.embeddingLiftIso_hom_app 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) : (CategoryTheory.Mat_.embeddingLiftIso F).hom.app X = CategoryTheory.Limits.biproduct.desc fun x => CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Mat_.embeddingLiftIso_inv_app 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) : (CategoryTheory.Mat_.embeddingLiftIso F).inv.app X = CategoryTheory.Limits.biproduct.lift fun x => CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Mat_.lift_map 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] {X✝ Y✝ : CategoryTheory.Mat_ C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Mat_.lift F).map f = CategoryTheory.Limits.biproduct.matrix fun i j => F.map (f i j)
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j)))
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality_assoc 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D} (h : (⨁ fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (N.X i))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) h)
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality' 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv (F.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'_assoc 📋 Mathlib.CategoryTheory.Preadditive.Mat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D} (h : F.obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv h)

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 ce5dd8c