Resolution

📁 Source: Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean

Statistics

Metric	Count
Definitions shortComplex, desc, descCompHomotopy, descFOne, descFSucc, descFZero, descHomotopy, descHomotopyZero, descHomotopyZeroOne, descHomotopyZeroSucc, descHomotopyZeroZero, descIdHomotopy, homotopyEquiv, iso, of, ofCocomplex, injectiveResolution, injectiveResolutions	18
Theorems shortExact_shortComplex, comp_descHomotopyZeroOne, comp_descHomotopyZeroOne_assoc, comp_descHomotopyZeroSucc, comp_descHomotopyZeroSucc_assoc, comp_descHomotopyZeroZero, comp_descHomotopyZeroZero_assoc, descFOne_zero_comm, desc_commutes, desc_commutes_assoc, desc_commutes_zero, desc_commutes_zero_assoc, exact₀, homotopyEquiv_hom_ι, homotopyEquiv_hom_ι_assoc, homotopyEquiv_inv_ι, homotopyEquiv_inv_ι_assoc, instHasInjectiveResolution, instHasInjectiveResolutions, instInjectiveXNatOfCocomplex, iso_hom_naturality, iso_hom_naturality_assoc, iso_inv_naturality, iso_inv_naturality_assoc, ofCocomplex_d_0_1, ofCocomplex_exactAt_succ, of_def, exact_f_d	28
Total	46

CategoryTheory

Definitions

Name	Category	Theorems
injectiveResolution 📖	CompOp	—
injectiveResolutions 📖	CompOp	4 math math: InjectiveResolution.iso_hom_naturality, InjectiveResolution.iso_hom_naturality_assoc, InjectiveResolution.iso_inv_naturality_assoc, InjectiveResolution.iso_inv_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_f_d 📖	mathematical	—	ShortComplex.Exact Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Injective.syzygies Limits.HasCokernels.has_colimit Abelian.has_cokernels Injective.d	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.cokernel.condition Limits.cokernel.condition_assoc Limits.zero_comp Category.id_comp Category.comp_id ShortComplex.exact_iff_of_epi_of_isIso_of_mono instEpiId IsIso.id Injective.ι_mono ShortComplex.exact_of_g_is_cokernel CategoryWithHomology.hasHomology categoryWithHomology_of_abelian

CategoryTheory.InjectivePresentation

Definitions

Name	Category	Theorems
shortComplex 📖	CompOp	1 math math: shortExact_shortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shortExact_shortComplex 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex	—	CategoryTheory.ShortComplex.exact_cokernel mono CategoryTheory.Limits.coequalizer.π_epi

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
desc 📖	CompOp	4 math math: desc_commutes_zero_assoc, desc_commutes, desc_commutes_assoc, desc_commutes_zero
descCompHomotopy 📖	CompOp	—
descFOne 📖	CompOp	1 math math: descFOne_zero_comm
descFSucc 📖	CompOp	—
descFZero 📖	CompOp	1 math math: descFOne_zero_comm
descHomotopy 📖	CompOp	—
descHomotopyZero 📖	CompOp	—
descHomotopyZeroOne 📖	CompOp	2 math math: comp_descHomotopyZeroOne_assoc, comp_descHomotopyZeroOne
descHomotopyZeroSucc 📖	CompOp	2 math math: comp_descHomotopyZeroSucc_assoc, comp_descHomotopyZeroSucc
descHomotopyZeroZero 📖	CompOp	4 math math: comp_descHomotopyZeroZero_assoc, comp_descHomotopyZeroOne_assoc, comp_descHomotopyZeroOne, comp_descHomotopyZeroZero
descIdHomotopy 📖	CompOp	—
homotopyEquiv 📖	CompOp	4 math math: homotopyEquiv_inv_ι, homotopyEquiv_hom_ι_assoc, homotopyEquiv_hom_ι, homotopyEquiv_inv_ι_assoc
iso 📖	CompOp	4 math math: iso_hom_naturality, iso_hom_naturality_assoc, iso_inv_naturality_assoc, iso_inv_naturality
of 📖	CompOp	1 math math: of_def
ofCocomplex 📖	CompOp	4 math math: of_def, ofCocomplex_d_0_1, ofCocomplex_exactAt_succ, instInjectiveXNatOfCocomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_descHomotopyZeroOne 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	HomologicalComplex.X HomologicalComplex.d descHomotopyZeroOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f descHomotopyZeroZero	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.Exact.comp_descToInjective HomologicalComplex.d_comp_d exact_succ
comp_descHomotopyZeroOne_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	HomologicalComplex.X HomologicalComplex.d descHomotopyZeroOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f descHomotopyZeroZero	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_descHomotopyZeroOne
comp_descHomotopyZeroSucc 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp HomologicalComplex.d	descHomotopyZeroSucc SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.Exact.comp_descToInjective HomologicalComplex.d_comp_d exact_succ
comp_descHomotopyZeroSucc_assoc 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp HomologicalComplex.d	descHomotopyZeroSucc SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_descHomotopyZeroSucc
comp_descHomotopyZeroZero 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	HomologicalComplex.X HomologicalComplex.d descHomotopyZeroZero HomologicalComplex.Hom.f	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.Exact.comp_descToInjective ι_f_zero_comp_complex_d exact₀
comp_descHomotopyZeroZero_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	HomologicalComplex.X HomologicalComplex.d descHomotopyZeroZero HomologicalComplex.Hom.f	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_descHomotopyZeroZero
descFOne_zero_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d descFOne descFZero	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.ShortComplex.Exact.comp_descToInjective AddRightCancelSemigroup.toIsRightCancelAdd ι_f_zero_comp_complex_d exact₀
desc_commutes 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι desc CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject HomologicalComplex.from_single_hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Injective.comp_factorThru CochainComplex.single₀_map_f_zero
desc_commutes_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι desc CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' desc_commutes
desc_commutes_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι desc	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.congr_hom desc_commutes CochainComplex.single₀_map_f_zero
desc_commutes_zero_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι desc	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' desc_commutes_zero
exact₀ 📖	mathematical	—	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι HomologicalComplex.d ι_f_zero_comp_complex_d	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.ShortComplex.exact_of_f_is_kernel AddRightCancelSemigroup.toIsRightCancelAdd ι_f_zero_comp_complex_d CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
homotopyEquiv_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι HomotopyEquiv.hom homotopyEquiv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd desc_commutes CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
homotopyEquiv_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι HomotopyEquiv.hom homotopyEquiv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homotopyEquiv_hom_ι
homotopyEquiv_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι HomotopyEquiv.inv homotopyEquiv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd desc_commutes CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
homotopyEquiv_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex ι HomotopyEquiv.inv homotopyEquiv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homotopyEquiv_inv_ι
instHasInjectiveResolution 📖	mathematical	—	CategoryTheory.HasInjectiveResolution CategoryTheory.Abelian.hasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Abelian.hasZeroObject
instHasInjectiveResolutions 📖	mathematical	—	CategoryTheory.HasInjectiveResolutions CategoryTheory.Abelian.hasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Abelian.hasZeroObject instHasInjectiveResolution
instInjectiveXNatOfCocomplex 📖	mathematical	—	CategoryTheory.Injective HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ofCocomplex	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Injective.injective_under
iso_hom_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory CategoryTheory.injectiveResolutions HomologicalComplex HomotopyCategory.quotient CategoryTheory.Functor.map CategoryTheory.Iso.hom iso	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.eq_of_homotopy desc_commutes_assoc homotopyEquiv_hom_ι homotopyEquiv_hom_ι_assoc HomologicalComplex.from_single_hom_ext CochainComplex.single₀_map_f_zero
iso_hom_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory CategoryTheory.injectiveResolutions CategoryTheory.Functor.map HomologicalComplex HomotopyCategory.quotient CategoryTheory.Iso.hom iso	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_hom_naturality
iso_inv_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory HomologicalComplex HomotopyCategory.quotient CategoryTheory.injectiveResolutions CategoryTheory.Iso.inv iso CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc iso_hom_naturality CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
iso_inv_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory HomologicalComplex HomotopyCategory.quotient CategoryTheory.injectiveResolutions CategoryTheory.Iso.inv iso CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_inv_naturality
ofCocomplex_d_0_1 📖	mathematical	—	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ofCocomplex CategoryTheory.Injective.d CategoryTheory.Injective.under CategoryTheory.Injective.ι CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CochainComplex.mk'_d_1_0
ofCocomplex_exactAt_succ 📖	mathematical	—	HomologicalComplex.ExactAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ofCocomplex	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.exactAt_iff' CochainComplex.prev_nat_succ CochainComplex.next HomologicalComplex.d_comp_d CochainComplex.of_d CategoryTheory.exact_f_d CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.hasCokernel_epi_comp CategoryTheory.Limits.coequalizer.π_epi
of_def 📖	mathematical	—	of CategoryTheory.Abelian.hasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofCocomplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.comp HomologicalComplex.d CategoryTheory.Limits.HasZeroMorphisms.zero CochainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CochainComplex.single₀ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CochainComplex.fromSingle₀Equiv CategoryTheory.Injective.ι	—	CategoryTheory.Abelian.hasZeroObject

---

← Back to Index