HomologicalComplexBiprod

📁 Source: Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean

Statistics

Metric	Count
Definitions biprodXIso	1
Theorems biprodXIso_hom_fst, biprodXIso_hom_fst_assoc, biprodXIso_hom_snd, biprodXIso_hom_snd_assoc, biprod_inl_desc_f, biprod_inl_desc_f_assoc, biprod_inl_fst_f, biprod_inl_fst_f_assoc, biprod_inl_snd_f, biprod_inl_snd_f_assoc, biprod_inr_desc_f, biprod_inr_desc_f_assoc, biprod_inr_fst_f, biprod_inr_fst_f_assoc, biprod_inr_snd_f, biprod_inr_snd_f_assoc, biprod_lift_fst_f, biprod_lift_fst_f_assoc, biprod_lift_snd_f, biprod_lift_snd_f_assoc, inl_biprodXIso_inv, inl_biprodXIso_inv_assoc, inr_biprodXIso_inv, inr_biprodXIso_inv_assoc, instHasBinaryBiproduct, instHasBinaryBiproductObjEval, instHasColimitDiscreteWalkingPairCompPairEval, instHasLimitDiscreteWalkingPairCompPairEval, instPreservesBinaryBiproductEval	29
Total	30

HomologicalComplex

Definitions

Name	Category	Theorems
biprodXIso 📖	CompOp	8 math math: inl_biprodXIso_inv_assoc, biprodXIso_hom_fst, inr_biprodXIso_inv, inl_biprodXIso_inv, biprodXIso_hom_fst_assoc, biprodXIso_hom_snd, biprodXIso_hom_snd_assoc, inr_biprodXIso_inv_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biprodXIso_hom_fst 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Iso.hom biprodXIso CategoryTheory.Limits.biprod.fst Hom.f	—	instHasBinaryBiproduct CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Functor.hasBinaryBiproduct_of_preserves instPreservesBinaryBiproductEval
biprodXIso_hom_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Iso.hom biprodXIso CategoryTheory.Limits.biprod.fst Hom.f	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprodXIso_hom_fst
biprodXIso_hom_snd 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Iso.hom biprodXIso CategoryTheory.Limits.biprod.snd Hom.f	—	instHasBinaryBiproduct CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Functor.hasBinaryBiproduct_of_preserves instPreservesBinaryBiproductEval
biprodXIso_hom_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Iso.hom biprodXIso CategoryTheory.Limits.biprod.snd Hom.f	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprodXIso_hom_snd
biprod_inl_desc_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.desc	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.inl_desc
biprod_inl_desc_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.desc	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprod_inl_desc_f
biprod_inl_fst_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.fst CategoryTheory.CategoryStruct.id	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.inl_fst id_f
biprod_inl_fst_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.fst	—	instHasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' biprod_inl_fst_f
biprod_inl_snd_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.inl_snd zero_f
biprod_inl_snd_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprod_inl_snd_f
biprod_inr_desc_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.desc	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.inr_desc
biprod_inr_desc_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.desc	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprod_inr_desc_f
biprod_inr_fst_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.inr_fst zero_f
biprod_inr_fst_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprod_inr_fst_f
biprod_inr_snd_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.snd CategoryTheory.CategoryStruct.id	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.inr_snd id_f
biprod_inr_snd_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.snd	—	instHasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' biprod_inr_snd_f
biprod_lift_fst_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.fst	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.lift_fst
biprod_lift_fst_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.fst	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprod_lift_fst_f
biprod_lift_snd_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd	—	instHasBinaryBiproduct comp_f CategoryTheory.Limits.biprod.lift_snd
biprod_lift_snd_f_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct Hom.f CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biprod_lift_snd_f
inl_biprodXIso_inv 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Limits.biprod.inl CategoryTheory.Iso.inv biprodXIso Hom.f	—	instHasBinaryBiproduct CategoryTheory.Limits.biprod.inl_desc
inl_biprodXIso_inv_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inl HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Iso.inv biprodXIso Hom.f	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_biprodXIso_inv
inr_biprodXIso_inv 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Limits.biprod.inr CategoryTheory.Iso.inv biprodXIso Hom.f	—	instHasBinaryBiproduct CategoryTheory.Limits.biprod.inr_desc
inr_biprodXIso_inv_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod CategoryTheory.Limits.biprod.inr HomologicalComplex instCategory instHasZeroMorphisms instHasBinaryBiproduct CategoryTheory.Iso.inv biprodXIso Hom.f	—	instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_biprodXIso_inv
instHasBinaryBiproduct 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	HomologicalComplex instCategory instHasZeroMorphisms	—	CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct instHasLimit instHasLimitDiscreteWalkingPairCompPairEval
instHasBinaryBiproductObjEval 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.Functor.obj HomologicalComplex instCategory eval	—	—
instHasColimitDiscreteWalkingPairCompPairEval 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.Limits.HasColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Functor.comp HomologicalComplex instCategory CategoryTheory.Limits.pair eval	—	CategoryTheory.Limits.hasColimit_of_iso CategoryTheory.Limits.HasBinaryBiproduct.hasColimit_pair
instHasLimitDiscreteWalkingPairCompPairEval 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.Limits.HasLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Functor.comp HomologicalComplex instCategory CategoryTheory.Limits.pair eval	—	CategoryTheory.Limits.hasLimit_of_iso CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair
instPreservesBinaryBiproductEval 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	CategoryTheory.Limits.PreservesBinaryBiproduct HomologicalComplex instCategory instHasZeroMorphisms eval instPreservesZeroMorphismsEval	—	CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct instPreservesZeroMorphismsEval instPreservesLimitEval instHasLimitDiscreteWalkingPairCompPairEval

---

← Back to Index