ConcreteCategory

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

Statistics

Metric	Count
Definitions cyclesMk	1
Theorems d_eq_zero_of_f_eq_d_apply, δ_apply, δ_apply', i_cyclesMk	4
Total	5

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_eq_zero_of_f_eq_d_apply 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms DFunLike.coe CategoryTheory.Functor.obj Ab AddCommGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier HomologicalComplex.X CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map HomologicalComplex.Hom.f CategoryTheory.ShortComplex.f HomologicalComplex.d	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive mono_f CategoryTheory.Preadditive.mono_iff_injective CategoryTheory.Abelian.hasZeroObject HomologicalComplex.instMonoFOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.ConcreteCategory.forget₂_comp_apply HomologicalComplex.Hom.comm HomologicalComplex.d_comp_d CategoryTheory.Functor.map_zero map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
δ_apply 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel DFunLike.coe CategoryTheory.Functor.obj Ab AddCommGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier HomologicalComplex.X CategoryTheory.ShortComplex.X₃ CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map HomologicalComplex.d NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.ShortComplex.X₂ HomologicalComplex.Hom.f CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f ComplexShape.next	HomologicalComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc δ HomologicalComplex.cycles HomologicalComplex.homologyπ HomologicalComplex.cyclesMk ComplexShape.next_eq' d_eq_zero_of_f_eq_d_apply	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive δ_apply' CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ComplexShape.next_eq' d_eq_zero_of_f_eq_d_apply CategoryTheory.ConcreteCategory.forget₂_comp_apply HomologicalComplex.p_opcyclesMap CategoryTheory.Functor.map_comp CategoryTheory.ConcreteCategory.comp_apply HomologicalComplex.homology_π_ι HomologicalComplex.i_cyclesMk CategoryTheory.Preadditive.mono_iff_injective CategoryTheory.Abelian.hasZeroObject HomologicalComplex.instMonoICycles HomologicalComplex.cyclesMap_i HomologicalComplex.pOpcycles_opcyclesToCycles_assoc HomologicalComplex.toCycles_i
δ_apply' 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel DFunLike.coe CategoryTheory.Functor.obj Ab AddCommGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier HomologicalComplex.opcycles CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₃ CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map HomologicalComplex.opcyclesMap CategoryTheory.ShortComplex.g HomologicalComplex.homology HomologicalComplex.homologyι HomologicalComplex.cycles CategoryTheory.ShortComplex.X₁ HomologicalComplex.cyclesMap CategoryTheory.ShortComplex.f HomologicalComplex.opcyclesToCycles	δ HomologicalComplex.homologyπ	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.SnakeInput.δ_apply'

HomologicalComplex

Definitions

Name	Category	Theorems
cyclesMk 📖	CompOp	2 math math: i_cyclesMk, CategoryTheory.ShortComplex.ShortExact.δ_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
i_cyclesMk 📖	mathematical	ComplexShape.next DFunLike.coe CategoryTheory.Functor.obj Ab AddCommGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map d NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	cycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian sc iCycles cyclesMk	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.i_cyclesMk

---

← Back to Index