Basic

📁 Source: Mathlib/Algebra/Homology/LeftResolution/Basic.lean

Statistics

Metric	Count
Definitions F, chainComplex, chainComplexFunctor, chainComplexMap, chainComplexXIso, chainComplexXOneIso, chainComplexXZeroIso, π	8
Theorems chainComplexMap_comp, chainComplexMap_comp_assoc, chainComplexMap_f_0, chainComplexMap_f_1, chainComplexMap_f_succ_succ, chainComplexMap_id, chainComplexMap_zero, epi_π_app, exactAt_map_chainComplex_succ, map_chainComplex_d, map_chainComplex_d_1_0, map_chainComplex_d_1_0_assoc, π_naturality, π_naturality_assoc	14
Total	22

CategoryTheory.Abelian.LeftResolution

Definitions

Name	Category	Theorems
F 📖	CompOp	19 math math: karoubi.F_obj_p, epi_π_app, karoubi.F'_map_f, map_chainComplex_d, π_naturality_assoc, karoubi.F_map_f, chainComplexMap_f_1, karoubi.F'_obj_p, chainComplexMap_f_0, karoubi_F, instPreservesZeroMorphismsFReduced, instPreservesZeroMorphismsKaroubiFKaroubi, map_chainComplex_d_1_0, karoubi.F'_obj_X, π_naturality, chainComplexMap_f_succ_succ, karoubi.π'_app_f, map_chainComplex_d_1_0_assoc, karoubi.F_obj_X
chainComplex 📖	CompOp	11 math math: chainComplexMap_zero, chainComplexMap_comp, chainComplexMap_id, exactAt_map_chainComplex_succ, map_chainComplex_d, chainComplexMap_f_1, chainComplexMap_comp_assoc, chainComplexMap_f_0, map_chainComplex_d_1_0, chainComplexMap_f_succ_succ, map_chainComplex_d_1_0_assoc
chainComplexFunctor 📖	CompOp	—
chainComplexMap 📖	CompOp	7 math math: chainComplexMap_zero, chainComplexMap_comp, chainComplexMap_id, chainComplexMap_f_1, chainComplexMap_comp_assoc, chainComplexMap_f_0, chainComplexMap_f_succ_succ
chainComplexXIso 📖	CompOp	2 math math: map_chainComplex_d, chainComplexMap_f_succ_succ
chainComplexXOneIso 📖	CompOp	3 math math: chainComplexMap_f_1, map_chainComplex_d_1_0, map_chainComplex_d_1_0_assoc
chainComplexXZeroIso 📖	CompOp	3 math math: chainComplexMap_f_0, map_chainComplex_d_1_0, map_chainComplex_d_1_0_assoc
π 📖	CompOp	9 math math: epi_π_app, map_chainComplex_d, π_naturality_assoc, karoubi_π, chainComplexMap_f_1, map_chainComplex_d_1_0, π_naturality, karoubi.π'_app_f, map_chainComplex_d_1_0_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chainComplexMap_comp 📖	mathematical	—	chainComplexMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainComplex	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.NatTrans.naturality CategoryTheory.Functor.map_comp_assoc CategoryTheory.Limits.kernel.map.congr_simp CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.kernel.lift_ι_assoc chainComplexMap_f_succ_succ
chainComplexMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainComplex chainComplexMap	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' chainComplexMap_comp
chainComplexMap_f_0 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne chainComplex chainComplexMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Functor.obj F CategoryTheory.Iso.hom chainComplexXZeroIso CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd
chainComplexMap_f_1 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne chainComplex chainComplexMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Functor.obj F CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app π CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom chainComplexXOneIso CategoryTheory.Functor.map CategoryTheory.Limits.kernel.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.naturality CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd
chainComplexMap_f_succ_succ 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne chainComplex chainComplexMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Functor.obj F CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.map HomologicalComplex.d CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom chainComplexXIso CategoryTheory.Limits.kernel.map CategoryTheory.Iso.inv	—	ChainComplex.mkHom_f_succ_succ
chainComplexMap_id 📖	mathematical	—	chainComplexMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainComplex	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.NatTrans.naturality CategoryTheory.Limits.kernel.map.congr_simp CategoryTheory.Limits.kernel.map_id chainComplexMap_f_succ_succ
chainComplexMap_zero 📖	mathematical	—	chainComplexMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainComplex HomologicalComplex.instZeroHom	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.NatTrans.naturality CategoryTheory.Functor.preservesZeroMorphisms_of_full CategoryTheory.Limits.kernel.map.congr_simp CategoryTheory.Limits.kernel.map_zero chainComplexMap_f_succ_succ
epi_π_app 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Functor.comp F CategoryTheory.Functor.id CategoryTheory.NatTrans.app π	—	—
exactAt_map_chainComplex_succ 📖	mathematical	—	HomologicalComplex.ExactAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_full chainComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_full HomologicalComplex.exactAt_iff' ComplexShape.prev_eq' ChainComplex.next_nat_succ CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Limits.kernel.lift_ι map_chainComplex_d CategoryTheory.Category.assoc CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_hom epi_π_app
map_chainComplex_d 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne chainComplex HomologicalComplex.d CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom chainComplexXIso CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp π CategoryTheory.Limits.kernel.ι	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Functor.map_preimage CategoryTheory.Functor.map_comp ChainComplex.mk'_d
map_chainComplex_d_1_0 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne chainComplex HomologicalComplex.d CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app π CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom chainComplexXOneIso CategoryTheory.Limits.kernel.ι CategoryTheory.Iso.inv chainComplexXZeroIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels ChainComplex.mk'_d_1_0 CategoryTheory.Functor.map_preimage CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_chainComplex_d_1_0_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne chainComplex CategoryTheory.Functor.map HomologicalComplex.d F CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id π CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom chainComplexXOneIso CategoryTheory.Limits.kernel.ι CategoryTheory.Iso.inv chainComplexXZeroIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_chainComplex_d_1_0
π_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp π	—	CategoryTheory.NatTrans.naturality
π_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_naturality

---

← Back to Index