Resolution

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

Statistics

Metric	Count
Definitions HasInjectiveResolution, HasInjectiveResolutions, InjectiveResolution, hom, cocomplex, isLimitKernelFork, kernelFork, self, ι	9
Theorems out, out, ι_comp_hom, ι_comp_hom_assoc, ι_f_zero_comp_hom_f_zero, ι_f_zero_comp_hom_f_zero_assoc, cocomplex_exactAt_succ, complex_d_comp, exact_succ, hasHomology, injective, instMonoFNatι, quasiIso, self_cocomplex, self_ι, ι_f_succ, ι_f_zero_comp_complex_d, ι_f_zero_comp_complex_d_assoc	18
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
HasInjectiveResolution 📖	CompData	2 math math: InjectiveResolution.instHasInjectiveResolution, HasInjectiveResolutions.out
HasInjectiveResolutions 📖	CompData	1 math math: InjectiveResolution.instHasInjectiveResolutions
InjectiveResolution 📖	CompData	1 math math: HasInjectiveResolution.out

CategoryTheory.HasInjectiveResolution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.InjectiveResolution	—	—

CategoryTheory.HasInjectiveResolutions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.HasInjectiveResolution	—	—

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
cocomplex 📖	CompOp	39 math math: injective, Hom.hom'_f, homotopyEquiv_inv_ι, ι'_f_zero, toRightDerivedZero'_comp_iCycles, complex_d_comp, desc_commutes_zero_assoc, CategoryTheory.instIsIsoToRightDerivedZero', toRightDerivedZero_eq, Hom.ι_comp_hom_assoc, ι_f_succ, ι_f_zero_comp_complex_d_assoc, instIsIsoToRightDerivedZero'Self, extMk_zero, ι_f_zero_comp_complex_d, self_cocomplex, desc_commutes, desc_commutes_assoc, Hom.ι_f_zero_comp_hom_f_zero, ι'_f_zero_assoc, cocomplex_exactAt_succ, Hom.hom'_f_assoc, cochainComplex_d_assoc, desc_commutes_zero, hasHomology, Hom.ι_f_zero_comp_hom_f_zero_assoc, exact_succ, instMonoFNatι, toRightDerivedZero'_comp_iCycles_assoc, homotopyEquiv_hom_ι_assoc, homotopyEquiv_hom_ι, exact₀, homotopyEquiv_inv_ι_assoc, rightDerivedToHomotopyCategory_app_eq, quasiIso, Hom.ι_comp_hom, descFOne_zero_comm, rightDerived_app_eq, cochainComplex_d
isLimitKernelFork 📖	CompOp	—
kernelFork 📖	CompOp	—
self 📖	CompOp	3 math math: self_ι, instIsIsoToRightDerivedZero'Self, self_cocomplex
ι 📖	CompOp	23 math math: homotopyEquiv_inv_ι, ι'_f_zero, self_ι, toRightDerivedZero'_comp_iCycles, desc_commutes_zero_assoc, Hom.ι_comp_hom_assoc, ι_f_succ, ι_f_zero_comp_complex_d_assoc, ι_f_zero_comp_complex_d, desc_commutes, desc_commutes_assoc, Hom.ι_f_zero_comp_hom_f_zero, ι'_f_zero_assoc, desc_commutes_zero, Hom.ι_f_zero_comp_hom_f_zero_assoc, instMonoFNatι, toRightDerivedZero'_comp_iCycles_assoc, homotopyEquiv_hom_ι_assoc, homotopyEquiv_hom_ι, exact₀, homotopyEquiv_inv_ι_assoc, quasiIso, Hom.ι_comp_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocomplex_exactAt_succ 📖	mathematical	—	HomologicalComplex.ExactAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasHomologyObjSingle hasHomology quasiIsoAt_iff_exactAt CochainComplex.exactAt_succ_single_obj QuasiIso.quasiIsoAt quasiIso
complex_d_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.d_comp_d
exact_succ 📖	mathematical	—	CategoryTheory.ShortComplex.Exact HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex HomologicalComplex.d HomologicalComplex.d_comp_d	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.exactAt_iff' CochainComplex.prev_nat_succ CochainComplex.next cocomplex_exactAt_succ
hasHomology 📖	mathematical	—	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex	—	—
injective 📖	mathematical	—	CategoryTheory.Injective HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex	—	—
instMonoFNatι 📖	mathematical	—	CategoryTheory.Mono 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₀ cocomplex HomologicalComplex.Hom.f ι	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.mono_of_isLimit_fork ι_f_succ CategoryTheory.Limits.HasZeroObject.instMono
quasiIso 📖	mathematical	—	QuasiIso 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₀ cocomplex ι HomologicalComplex.instHasHomologyObjSingle hasHomology	—	—
self_cocomplex 📖	mathematical	—	cocomplex self CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex.single₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
self_ι 📖	mathematical	—	ι self CategoryTheory.CategoryStruct.id CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CochainComplex.single₀	—	—
ι_f_succ 📖	mathematical	—	HomologicalComplex.Hom.f 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₀ cocomplex ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.IsZero.eq_of_src AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isZero_single_obj_X
ι_f_zero_comp_complex_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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₀ cocomplex HomologicalComplex.Hom.f ι HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.Hom.comm ι_f_succ CategoryTheory.Limits.comp_zero
ι_f_zero_comp_complex_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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₀ cocomplex HomologicalComplex.Hom.f ι HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_f_zero_comp_complex_d

CategoryTheory.InjectiveResolution.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: hom'_f, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, ι_comp_hom_assoc, ι_f_zero_comp_hom_f_zero, hom'_f_assoc, ι_f_zero_comp_hom_f_zero_assoc, ι_comp_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_comp_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex 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.InjectiveResolution.cocomplex CategoryTheory.InjectiveResolution.ι hom CategoryTheory.Functor.map	—	HomologicalComplex.from_single_hom_ext AddRightCancelSemigroup.toIsRightCancelAdd ι_f_zero_comp_hom_f_zero CochainComplex.single₀_map_f_zero
ι_comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex 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.InjectiveResolution.cocomplex CategoryTheory.InjectiveResolution.ι hom CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_hom
ι_f_zero_comp_hom_f_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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.InjectiveResolution.cocomplex HomologicalComplex.Hom.f CategoryTheory.InjectiveResolution.ι hom CategoryTheory.Functor.map	—	—
ι_f_zero_comp_hom_f_zero_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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.InjectiveResolution.cocomplex HomologicalComplex.Hom.f CategoryTheory.InjectiveResolution.ι hom CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_f_zero_comp_hom_f_zero

---

← Back to Index