BifunctorHomotopy

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

Statistics

Metric	Count
Definitions hom₁, hom₂, mapBifunctorMapHomotopy₁, mapBifunctorMapHomotopy₂	4
Theorems comm₁, comm₁_aux, zero₁, ιMapBifunctor_hom₁, ιMapBifunctor_hom₁_assoc, ιMapBifunctor_hom₂, ιMapBifunctor_hom₂_assoc	7
Total	11

HomologicalComplex

Definitions

Name	Category	Theorems
mapBifunctorMapHomotopy₁ 📖	CompOp	—
mapBifunctorMapHomotopy₂ 📖	CompOp	—

HomologicalComplex.mapBifunctorMapHomotopy

Definitions

Name	Category	Theorems
hom₁ 📖	CompOp	5 math math: comm₁, zero₁, comm₁_aux, ιMapBifunctor_hom₁_assoc, ιMapBifunctor_hom₁
hom₂ 📖	CompOp	2 math math: ιMapBifunctor_hom₂, ιMapBifunctor_hom₂_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive	HomologicalComplex.Hom.f HomologicalComplex.mapBifunctor HomologicalComplex.mapBifunctorMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp ComplexShape.next HomologicalComplex.d hom₁ ComplexShape.prev	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.mapBifunctor.hom_ext HomologicalComplex.ι_mapBifunctorMap Homotopy.comm CategoryTheory.Functor.map_add CategoryTheory.Functor.map_comp CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc CategoryTheory.Preadditive.comp_add HomologicalComplex₂.ι_D₁_assoc HomologicalComplex₂.ι_D₂_assoc AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg ComplexShape.next_π₁ HomologicalComplex₂.d₁_eq CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f CategoryTheory.Linear.units_smul_comp ιMapBifunctor_hom₁ ComplexShape.prev_eq' CategoryTheory.Linear.comp_units_smul smul_smul Int.units_mul_self one_smul HomologicalComplex.ιMapBifunctorOrZero_eq HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp HomologicalComplex₂.d₁_eq_zero ιMapBifunctor_hom₁_assoc ComplexShape.prev_π₁ HomologicalComplex₂.ι_D₁ CategoryTheory.NatTrans.naturality_assoc Homotopy.zero smul_zero HomologicalComplex₂.ι_D₂ comm₁_aux HomologicalComplex₂.d₂_eq_zero CategoryTheory.Limits.comp_zero zero_eq_neg ComplexShape.next_π₂ HomologicalComplex₂.d₂_eq CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d zero₁
comm₁_aux 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel ComplexShape.π	Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject HomologicalComplex HomologicalComplex.instCategory HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.mapBifunctorHomologicalComplex Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map Homotopy.hom HomologicalComplex.Hom.f HomologicalComplex₂.d₂ HomologicalComplex.mapBifunctor NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ComplexShape.next hom₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_π₂ ComplexShape.next_π₁ HomologicalComplex₂.d₂_eq ComplexShape.next_eq' ComplexShape.rel_π₂ CategoryTheory.Linear.comp_units_smul CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc ιMapBifunctor_hom₁ ComplexShape.prev_eq' HomologicalComplex.ιMapBifunctorOrZero_eq smul_smul CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d CategoryTheory.NatTrans.naturality_assoc ComplexShape.ε₁_ε₂ neg_mul Units.neg_smul smul_left_cancel_iff CategoryTheory.Functor.map_comp_assoc HomologicalComplex.Hom.comm
zero₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel	hom₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.mapBifunctor CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.mapBifunctor.hom_ext CategoryTheory.Limits.comp_zero HomologicalComplex₂.ι_totalDesc HomologicalComplex.ιMapBifunctorOrZero_eq_zero ComplexShape.rel_π₁ smul_zero Homotopy.zero CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp
ιMapBifunctor_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.π ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor hom₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.NatTrans.app CategoryTheory.Functor.map Homotopy.hom HomologicalComplex.Hom.f HomologicalComplex.ιMapBifunctorOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex₂.ι_totalDesc
ιMapBifunctor_hom₁_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.π ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor hom₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.NatTrans.app CategoryTheory.Functor.map Homotopy.hom HomologicalComplex.Hom.f HomologicalComplex.ιMapBifunctorOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapBifunctor_hom₁
ιMapBifunctor_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.π ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor hom₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.Hom.f Homotopy.hom HomologicalComplex.ιMapBifunctorOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex₂.ι_totalDesc
ιMapBifunctor_hom₂_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.π ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor hom₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.Hom.f Homotopy.hom HomologicalComplex.ιMapBifunctorOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapBifunctor_hom₂

---

← Back to Index