Single

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

Statistics

Metric	Count
Definitions fromSingle₀Equiv, single₀, toSingle₀Equiv, fromSingle₀Equiv, single₀, toSingle₀Equiv, mkHomFromSingle, mkHomToSingle, single, singleCompEvalIsoSelf, singleObjXIsoOfEq, singleObjXSelf	12
Theorems fromSingle₀Equiv_apply, fromSingle₀Equiv_symm_apply_f_succ, fromSingle₀Equiv_symm_apply_f_zero, single₀ObjXSelf, single₀_map_f_zero, single₀_obj_zero, toSingle₀Equiv_apply_coe, toSingle₀Equiv_symm_apply_f_zero, fromSingle₀Equiv_apply_coe, fromSingle₀Equiv_symm_apply_f_zero, single₀ObjXSelf, single₀_map_f_zero, single₀_obj_zero, toSingle₀Equiv_apply, toSingle₀Equiv_symm_apply_f_succ, toSingle₀Equiv_symm_apply_f_zero, from_single_hom_ext, from_single_hom_ext_iff, instFaithfulSingle, instFullSingle, instPreservesZeroMorphismsSingle, isZero_single_comp_eval, isZero_single_obj_X, mkHomFromSingle_f, mkHomToSingle_f, singleCompEvalIsoSelf_hom_app, singleCompEvalIsoSelf_inv_app, single_map_f_self, single_map_f_self_assoc, single_obj_X_self, single_obj_d, to_single_hom_ext, to_single_hom_ext_iff	33
Total	45

ChainComplex

Definitions

Name	Category	Theorems
fromSingle₀Equiv 📖	CompOp	3 math math: fromSingle₀Equiv_symm_apply_f_zero, fromSingle₀Equiv_apply, fromSingle₀Equiv_symm_apply_f_succ
single₀ 📖	CompOp	42 math math: CategoryTheory.ProjectiveResolution.quasiIso, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, CategoryTheory.ProjectiveResolution.self_π, CategoryTheory.Functor.mapProjectiveResolution_π, toSingle₀Equiv_apply_coe, Rep.standardComplex.εToSingle₀_comp_eq, exactAt_succ_single_obj, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.ProjectiveResolution.of_def, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.ProjectiveResolution.π_f_succ, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, CategoryTheory.ProjectiveResolution.lift_commutes_zero, CategoryTheory.ProjectiveResolution.lift_commutes, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π, CategoryTheory.ProjectiveResolution.π'_f_zero, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, CategoryTheory.ProjectiveResolution.self_complex, fromSingle₀Equiv_symm_apply_f_zero, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, toSingle₀Equiv_symm_apply_f_zero, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, Rep.standardComplex.instQuasiIsoNatεToSingle₀, fromSingle₀Equiv_apply, Rep.FiniteCyclicGroup.resolution_quasiIso, CategoryTheory.ProjectiveResolution.exact₀, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, single₀_obj_zero, fromSingle₀Equiv_symm_apply_f_succ, single₀_map_f_zero, Rep.FiniteCyclicGroup.resolution.π_f
toSingle₀Equiv 📖	CompOp	3 math math: toSingle₀Equiv_apply_coe, CategoryTheory.ProjectiveResolution.of_def, toSingle₀Equiv_symm_apply_f_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSingle₀Equiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj single₀ HomologicalComplex.X EquivLike.toFunLike Equiv.instEquivLike fromSingle₀Equiv HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
fromSingle₀Equiv_symm_apply_f_succ 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory single₀ DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fromSingle₀Equiv CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
fromSingle₀Equiv_symm_apply_f_zero 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory single₀ DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fromSingle₀Equiv	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.mkHomFromSingle_f CategoryTheory.Category.id_comp
single₀ObjXSelf 📖	mathematical	—	HomologicalComplex.singleObjXSelf ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Iso.refl HomologicalComplex.X CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.single	—	AddRightCancelSemigroup.toIsRightCancelAdd
single₀_map_f_zero 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory single₀ CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.single_map_f_self CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
single₀_obj_zero 📖	mathematical	—	HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory single₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
toSingle₀Equiv_apply_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.comp HomologicalComplex.d CategoryTheory.Limits.HasZeroMorphisms.zero DFunLike.coe Equiv ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj single₀ EquivLike.toFunLike Equiv.instEquivLike toSingle₀Equiv HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
toSingle₀Equiv_symm_apply_f_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.Hom.f CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory single₀ DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSingle₀Equiv	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.mkHomToSingle_f CategoryTheory.Category.comp_id

CochainComplex

Definitions

Name	Category	Theorems
fromSingle₀Equiv 📖	CompOp	3 math math: CategoryTheory.InjectiveResolution.of_def, fromSingle₀Equiv_apply_coe, fromSingle₀Equiv_symm_apply_f_zero
single₀ 📖	CompOp	33 math math: CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.InjectiveResolution.self_ι, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, CategoryTheory.InjectiveResolution.of_def, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, fromSingle₀Equiv_apply_coe, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CategoryTheory.InjectiveResolution.ι_f_succ, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, exactAt_succ_single_obj, single₀_map_f_zero, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, CategoryTheory.InjectiveResolution.self_cocomplex, CategoryTheory.InjectiveResolution.desc_commutes, CategoryTheory.InjectiveResolution.desc_commutes_assoc, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, toSingle₀Equiv_symm_apply_f_succ, CategoryTheory.InjectiveResolution.desc_commutes_zero, fromSingle₀Equiv_symm_apply_f_zero, toSingle₀Equiv_apply, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, CategoryTheory.InjectiveResolution.instMonoFNatι, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, single₀_obj_zero, toSingle₀Equiv_symm_apply_f_zero, CategoryTheory.InjectiveResolution.quasiIso, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom
toSingle₀Equiv 📖	CompOp	3 math math: toSingle₀Equiv_symm_apply_f_succ, toSingle₀Equiv_apply, toSingle₀Equiv_symm_apply_f_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSingle₀Equiv_apply_coe 📖	mathematical	—	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 DFunLike.coe Equiv CochainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj single₀ EquivLike.toFunLike Equiv.instEquivLike fromSingle₀Equiv HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
fromSingle₀Equiv_symm_apply_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 HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.Hom.f CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory single₀ DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm fromSingle₀Equiv	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.mkHomFromSingle_f CategoryTheory.Category.id_comp
single₀ObjXSelf 📖	mathematical	—	HomologicalComplex.singleObjXSelf ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Iso.refl HomologicalComplex.X CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.single	—	AddRightCancelSemigroup.toIsRightCancelAdd
single₀_map_f_zero 📖	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 single₀ CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.single_map_f_self CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
single₀_obj_zero 📖	mathematical	—	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 single₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
toSingle₀Equiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj single₀ HomologicalComplex.X EquivLike.toFunLike Equiv.instEquivLike toSingle₀Equiv HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
toSingle₀Equiv_symm_apply_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 single₀ DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSingle₀Equiv CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
toSingle₀Equiv_symm_apply_f_zero 📖	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 single₀ DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSingle₀Equiv	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.mkHomToSingle_f CategoryTheory.Category.comp_id

HomologicalComplex

Definitions

Name	Category	Theorems
mkHomFromSingle 📖	CompOp	2 math math: evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, mkHomFromSingle_f
mkHomToSingle 📖	CompOp	1 math math: mkHomToSingle_f
single 📖	CompOp	92 math math: extendSingleIso_inv_f, singleMapHomologicalComplex_hom_app_ne, instPreservesLimitsOfShapeSingle, rightUnitor'_inv, isZero_single_obj_X, singleMapHomologicalComplex_hom_app_self, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, instPreservesColimitsOfShapeSingle, pOpcycles_singleObjOpcyclesSelfIso_inv, isZero_single_obj_homology, singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_inv_iCycles, CategoryTheory.InjectiveResolution.ι'_f_zero, homologyι_singleObjOpcyclesSelfIso_inv_assoc, CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle, to_single_hom_ext_iff, singleObjCyclesSelfIso_inv_homologyπ, CochainComplex.HomComplex.Cochain.toSingleMk_v, single_obj_d, CategoryTheory.Functor.mapProjectiveResolution_π, CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle, homologyι_singleObjOpcyclesSelfIso_inv, extendSingleIso_inv_f_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, ChainComplex.single₀ObjXSelf, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_hom_naturality, singleObjCyclesSelfIso_inv_naturality_assoc, Rep.standardComplex.εToSingle₀_comp_eq, from_single_hom_ext_iff, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homologyπ_singleObjHomologySelfIso_hom_assoc, single_obj_X_self, singleMapHomologicalComplex_inv_app_self, extendSingleIso_hom_f_assoc, instHasHomologyObjSingle, CochainComplex.HomComplex.Cochain.fromSingleMk_v, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, extend_single_d, singleObjHomologySelfIso_inv_homologyι_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, singleObjCyclesSelfIso_inv_homologyπ_assoc, singleObjOpcyclesSelfIso_inv_naturality, mkHomToSingle_f, CategoryTheory.ProjectiveResolution.π'_f_zero, leftUnitor'_inv, single_map_f_self_assoc, CochainComplex.exists_iso_single, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, homologyπ_singleObjHomologySelfIso_hom, singleObjCyclesSelfIso_inv_iCycles_assoc, singleObjOpcyclesSelfIso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, singleMapHomologicalComplex_inv_app_ne, single_map_f_self, singleCompEvalIsoSelf_inv_app, homologyFunctorSingleIso_inv_app, singleObjHomologySelfIso_hom_naturality, singleObjHomologySelfIso_hom_naturality_assoc, singleObjHomologySelfIso_inv_naturality_assoc, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, singleObjCyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_inv_naturality, singleCompEvalIsoSelf_hom_app, singleObjOpcyclesSelfIso_inv_naturality_assoc, instPreservesFiniteColimitsSingle, singleObjHomologySelfIso_inv_naturality, evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, singleObjCyclesSelfIso_hom_naturality_assoc, mkHomFromSingle_f, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, exactAt_single_obj, instPreservesFiniteLimitsSingle, instAdditiveSingle, instPreservesZeroMorphismsSingle, singleObjCyclesSelfIso_hom, extendSingleIso_hom_f, instFullSingle, instFaithfulSingle, singleObjHomologySelfIso_inv_homologyι, homologyFunctorSingleIso_hom_app, singleObjOpcyclesSelfIso_hom_assoc, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv, isZero_single_comp_eval, singleObjOpcyclesSelfIso_hom_naturality, Rep.FiniteCyclicGroup.resolution.π_f, CochainComplex.single₀ObjXSelf
singleCompEvalIsoSelf 📖	CompOp	2 math math: singleCompEvalIsoSelf_inv_app, singleCompEvalIsoSelf_hom_app
singleObjXIsoOfEq 📖	CompOp	1 math math: Rep.FiniteCyclicGroup.resolution.π_f
singleObjXSelf 📖	CompOp	31 math math: extendSingleIso_inv_f, rightUnitor'_inv, singleMapHomologicalComplex_hom_app_self, pOpcycles_singleObjOpcyclesSelfIso_inv, singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_inv_iCycles, CategoryTheory.InjectiveResolution.ι'_f_zero, CochainComplex.HomComplex.Cochain.toSingleMk_v, extendSingleIso_inv_f_assoc, ChainComplex.single₀ObjXSelf, singleMapHomologicalComplex_inv_app_self, extendSingleIso_hom_f_assoc, CochainComplex.HomComplex.Cochain.fromSingleMk_v, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, mkHomToSingle_f, CategoryTheory.ProjectiveResolution.π'_f_zero, leftUnitor'_inv, single_map_f_self_assoc, singleObjCyclesSelfIso_inv_iCycles_assoc, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, single_map_f_self, singleCompEvalIsoSelf_inv_app, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, singleObjCyclesSelfIso_hom_assoc, singleCompEvalIsoSelf_hom_app, evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, mkHomFromSingle_f, singleObjCyclesSelfIso_hom, extendSingleIso_hom_f, singleObjOpcyclesSelfIso_hom_assoc, CochainComplex.single₀ObjXSelf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
from_single_hom_ext 📖	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	—	hom_ext CategoryTheory.Limits.IsZero.eq_of_src isZero_single_obj_X
from_single_hom_ext_iff 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	from_single_hom_ext
instFaithfulSingle 📖	mathematical	—	CategoryTheory.Functor.Faithful HomologicalComplex instCategory single	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom single_map_f_self
instFullSingle 📖	mathematical	—	CategoryTheory.Functor.Full HomologicalComplex instCategory single	—	from_single_hom_ext CategoryTheory.Functor.map_comp single_map_f_self CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Iso.inv_hom_id_assoc
instPreservesZeroMorphismsSingle 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms HomologicalComplex instCategory instHasZeroMorphisms single	—	CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full instFullSingle
isZero_single_comp_eval 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp HomologicalComplex instCategory single eval	—	CategoryTheory.Functor.isZero isZero_single_obj_X
isZero_single_obj_X 📖	mathematical	—	CategoryTheory.Limits.IsZero X CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	CategoryTheory.Limits.isZero_zero
mkHomFromSingle_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single mkHomFromSingle CategoryTheory.Iso.hom singleObjXSelf	—	CategoryTheory.Category.comp_id
mkHomToSingle_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single mkHomToSingle CategoryTheory.Iso.inv singleObjXSelf	—	CategoryTheory.Category.id_comp
singleCompEvalIsoSelf_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp HomologicalComplex instCategory single eval CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category singleCompEvalIsoSelf X CategoryTheory.Functor.obj singleObjXSelf	—	—
singleCompEvalIsoSelf_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp HomologicalComplex instCategory single eval CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category singleCompEvalIsoSelf X CategoryTheory.Functor.obj singleObjXSelf	—	—
single_map_f_self 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom singleObjXSelf CategoryTheory.Iso.inv	—	—
single_map_f_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Functor.obj HomologicalComplex instCategory single Hom.f CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjXSelf CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' single_map_f_self
single_obj_X_self 📖	mathematical	—	X CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	—
single_obj_d 📖	mathematical	—	d CategoryTheory.Functor.obj HomologicalComplex instCategory single Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
to_single_hom_ext 📖	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	—	hom_ext CategoryTheory.Limits.IsZero.eq_of_tgt isZero_single_obj_X
to_single_hom_ext_iff 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	to_single_hom_ext

---

← Back to Index