Loogle!

Result

Found 93 declarations mentioning CategoryTheory.Limits.biprod.snd.

CategoryTheory.Limits.biprod.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : X ⊞ Y ⟶ Y
CategoryTheory.Limits.biprod.snd_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsSplitEpi CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.instHasKernelSnd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.HasKernel CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.sndKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.KernelFork CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.kernelBiprodSndIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.kernel CategoryTheory.Limits.biprod.snd ≅ X
CategoryTheory.Limits.BinaryBiproduct.bicone_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).snd = CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.inr_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.id Y
CategoryTheory.Limits.isoZeroBiprod_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero X) : (CategoryTheory.Limits.isoZeroBiprod hY).inv = CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.lift_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) CategoryTheory.Limits.biprod.snd = g
CategoryTheory.Limits.biprod.inr_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = h
CategoryTheory.Limits.biprod.inl_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd = 0
CategoryTheory.Limits.biprod.isKernelSndKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.biprod.sndKernelFork X Y)
CategoryTheory.Limits.biprod.isoProd_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.biprod.isoProd X Y).hom = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.lift_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp g h
CategoryTheory.Limits.biprod.inl_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp 0 h
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.braiding_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C) : (CategoryTheory.Limits.biprod.braiding P Q).hom = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst
CategoryTheory.Limits.biprod.braiding_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C) : (CategoryTheory.Limits.biprod.braiding P Q).inv = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst
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.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f g : Z ⟶ X ⊞ Y) (h₀ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst) (h₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd) : f = g
CategoryTheory.Limits.biprod.opIso_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.inr.op
CategoryTheory.Limits.biprod.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] {f g : Z ⟶ X ⊞ Y} : f = g ↔ CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst ∧ CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.inr_opIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.opIso P Q).inv = CategoryTheory.Limits.biprod.snd.op
CategoryTheory.Limits.biprod.inlCokernelCofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.biprod.inlCokernelCofork X Y) = CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.sndKernelFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.biprod.sndKernelFork X Y) = CategoryTheory.Limits.biprod.inl
CategoryTheory.Limits.biprod.opIso_inv_inr_op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv CategoryTheory.Limits.biprod.inr.op = CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.snd_op_opIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op (CategoryTheory.Limits.biprod.opIso P Q).hom = CategoryTheory.Limits.biprod.inr
CategoryTheory.Limits.biprod.symmetry' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) = CategoryTheory.CategoryStruct.id (P ⊞ Q)
CategoryTheory.Limits.biprod.symmetry'_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C) {Z : C} (h : P ⊞ Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) h) = h
CategoryTheory.Limits.biprod.inr_opIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op (P ⊞ Q) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op h
CategoryTheory.Limits.biprod.opIso_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr.op h
CategoryTheory.Limits.biprod.opIso_inv_inr_op_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr.op h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h
CategoryTheory.Limits.biprod.snd_op_opIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P Q : C) [CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⊞ Opposite.op Q ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
CategoryTheory.Limits.biprod.associator_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P Q R : C) : (CategoryTheory.Limits.biprod.associator P Q R).hom = CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd) CategoryTheory.Limits.biprod.snd)
CategoryTheory.Limits.biprod.associator_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P Q R : C) : (CategoryTheory.Limits.biprod.associator P Q R).inv = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.snd)
CategoryTheory.Limits.kernelBiprodSndIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.kernelBiprodSndIso.inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0) (CategoryTheory.Limits.biprod.sndKernelFork X Y)
CategoryTheory.Limits.kernelBiprodSndIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
{C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.kernelBiprodSndIso.hom = (CategoryTheory.Limits.biprod.isKernelSndKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0))
CategoryTheory.Functor.biprodComparison_snd 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] : CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y) CategoryTheory.Limits.biprod.snd = F.map CategoryTheory.Limits.biprod.snd
CategoryTheory.Functor.biprodComparison_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.biprod.snd) h
CategoryTheory.Functor.mapBiprod_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] : (F.mapBiprod X Y).hom = CategoryTheory.Limits.biprod.lift (F.map CategoryTheory.Limits.biprod.fst) (F.map CategoryTheory.Limits.biprod.snd)
CategoryTheory.Limits.biprod.ext_to_iff 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} {f g : Z ⟶ X ⊞ Y} : f = g ↔ CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst ∧ CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd
CategoryTheory.Limits.biprod.desc_eq 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] {T : C} {f : X ⟶ T} {g : Y ⟶ T} : CategoryTheory.Limits.biprod.desc f g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
CategoryTheory.Limits.biprod.decomp_hom_from 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (f : X ⊞ Y ⟶ Z) : ∃ f₁ f₂, f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂
CategoryTheory.Limits.biprod.total 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inr = CategoryTheory.CategoryStruct.id (X ⊞ Y)
CategoryTheory.Biprod.column_nonzero_of_iso 📋 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 ⊞ X ⟶ Y ⊞ Z) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.id W = 0 ∨ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst) ≠ 0 ∨ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd) ≠ 0
CategoryTheory.Biprod.ofComponents_fst 📋 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.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₁ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₁
CategoryTheory.Biprod.ofComponents_snd 📋 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.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₂ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₂
CategoryTheory.Biprod.ofComponents_eq 📋 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.Biprod.ofComponents (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) = f
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)
AddCommGrpCat.biprodIsoProd_inv_comp_snd 📋 Mathlib.Algebra.Category.Grp.Biproducts
(G H : AddCommGrpCat) : CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.snd = AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H)
AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply 📋 Mathlib.Algebra.Category.Grp.Biproducts
(G H : AddCommGrpCat) (x : ↑G × ↑H) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd) ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) = x.2
CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X₁ X₂ : C) [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := CategoryTheory.Limits.biprod.inl, g := CategoryTheory.Limits.biprod.snd, zero := ⋯ }.Splitting
ModuleCat.biprodIsoProd_inv_comp_snd 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
{R : Type u} [Ring R] (M N : ModuleCat R) : CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.snd = ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)
ModuleCat.biprodIsoProd_inv_comp_snd_apply 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
{R : Type u} [Ring R] (M N : ModuleCat R) (x : ↑M × ↑N) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd) ((CategoryTheory.ConcreteCategory.hom (M.biprodIsoProd N).inv) x) = x.2
HomologicalComplex.biprod_inr_snd_f 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.Limits.biprod.snd.f i) = CategoryTheory.CategoryStruct.id (L.X i)
HomologicalComplex.biprod_inr_snd_f_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : L.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) = h
HomologicalComplex.biprod_inl_snd_f 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.Limits.biprod.snd.f i) = 0
HomologicalComplex.biprodXIso_hom_snd 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) : CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.snd.f i
HomologicalComplex.biprod_lift_snd_f 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K L : HomologicalComplex C c} [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c} (α : M ⟶ K) (β : M ⟶ L) (i : ι) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i) (CategoryTheory.Limits.biprod.snd.f i) = β.f i
HomologicalComplex.biprod_inl_snd_f_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : L.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) = CategoryTheory.CategoryStruct.comp 0 h
HomologicalComplex.biprod_lift_snd_f_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K L : HomologicalComplex C c} [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c} (α : M ⟶ K) (β : M ⟶ L) (i : ι) {Z : C} (h : L.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) = CategoryTheory.CategoryStruct.comp (β.f i) h
HomologicalComplex.biprodXIso_hom_snd_assoc 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : L.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h
HomologicalComplex.biprodX_ext_to 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K L : HomologicalComplex C c} [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι} {f g : A ⟶ (K ⊞ L).X i} (h₁ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.fst.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.fst.f i)) (h₂ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.snd.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.snd.f i)) : f = g
HomologicalComplex.biprodX_ext_to_iff 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K L : HomologicalComplex C c} [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι} {f g : A ⟶ (K ⊞ L).X i} : f = g ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.fst.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.fst.f i) ∧ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.snd.f i) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.snd.f i)
HomologicalComplex.biprod_total_f 📋 Mathlib.Algebra.Homology.HomologicalComplexBiprod
{C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K L : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) (CategoryTheory.Limits.biprod.inl.f i) + CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) (CategoryTheory.Limits.biprod.inr.f i) = CategoryTheory.CategoryStruct.id ((K ⊞ L).X i)
CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₂ = CategoryTheory.Limits.biprod.snd
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₂ = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang 📋 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] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (zero : T.mor₃ = 0) : ∃ e, CategoryTheory.CategoryStruct.comp T.mor₁ e.hom = CategoryTheory.Limits.biprod.inl ∧ T.mor₂ = CategoryTheory.CategoryStruct.comp e.hom CategoryTheory.Limits.biprod.snd
CategoryTheory.Abelian.Ext.addEquivBiprod_apply_snd 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X Y₁ Y₂ : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext X (Y₁ ⊞ Y₂) n) : (CategoryTheory.Abelian.Ext.addEquivBiprod e).2 = e.comp (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.snd) ⋯
CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X₁ X₂ Y : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext X₁ Y n × CategoryTheory.Abelian.Ext X₂ Y n) : CategoryTheory.Abelian.Ext.biprodAddEquiv.symm e = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.fst).comp e.1 ⋯ + (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.snd).comp e.2 ⋯
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₁.g = CategoryTheory.Limits.biprod.snd
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_g 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₂.g = CategoryTheory.Limits.biprod.snd
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₁ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₁₂.τ₁ = f
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₁₂.τ₃ = g
CategoryTheory.kernelCokernelCompSequence.φ_snd 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₁₂.τ₂ = CategoryTheory.kernelCokernelCompSequence.φ f g
CategoryTheory.kernelCokernelCompSequence.φ_snd_assoc 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g h)
CategoryTheory.kernelCokernelCompSequence.ι_snd 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) f
CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₀₁.τ₁ = CategoryTheory.Limits.kernel.ι f
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₀₁.τ₃ = CategoryTheory.Limits.kernel.ι g
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₁ = CategoryTheory.Limits.cokernel.π f
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₃ = CategoryTheory.Limits.cokernel.π g
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₀₁.τ₂ = CategoryTheory.kernelCokernelCompSequence.ι f g
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₂ = CategoryTheory.kernelCokernelCompSequence.π f g
CategoryTheory.Limits.pointwiseBinaryBicone_snd_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (F G : CategoryTheory.Functor D C) (X : D) : (CategoryTheory.Limits.pointwiseBinaryBicone F G).snd.app X = CategoryTheory.Limits.biprod.snd
CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.HasPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.pushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd ≅ 0
CategoryTheory.BicartesianSq.of_has_biproduct₁ 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.BicartesianSq CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
CategoryTheory.IsPullback.inl_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
CategoryTheory.IsPullback.of_has_biproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPullback CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
CategoryTheory.IsPushout.inl_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
CategoryTheory.IsPushout.of_hasBinaryBiproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0

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