Refinements

📁 Source: Mathlib/CategoryTheory/Abelian/Refinements.lean

Statistics

Metric	Count
Definitions	0
Theorems comp_π_eq_zero_iff_up_to_refinements, exact_up_to_refinements, comp_homologyπ_eq_iff_up_to_refinements, comp_homologyπ_eq_zero_iff_up_to_refinements, comp_pOpcycles_eq_zero_iff_up_to_refinements, epi_homologyMap_iff_up_to_refinements, eq_liftCycles_homologyπ_up_to_refinements, exact_iff_exact_up_to_refinements, liftCycles_comp_homologyπ_eq_iff_up_to_refinements, liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, mono_homologyMap_iff_up_to_refinements, epi_iff_surjective_up_to_refinements, surjective_up_to_refinements_of_epi	13
Total	13

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_surjective_up_to_refinements 📖	mathematical	—	Epi Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp	—	Limits.hasLimitOfHasLimitsOfShape Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype Limits.hasFiniteWidePullbacks_of_hasFiniteLimits Abelian.hasFiniteLimits Abelian.epi_pullback_of_epi_g Limits.pullback.condition epi_of_epi_fac Category.comp_id
surjective_up_to_refinements_of_epi 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Epi CategoryStruct.comp	—	epi_iff_surjective_up_to_refinements

CategoryTheory.Limits.CokernelCofork.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_π_eq_zero_iff_up_to_refinements 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.Cofork.π CategoryTheory.Epi	—	CategoryTheory.Limits.CokernelCofork.condition CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.ShortComplex.zero CategoryTheory.Category.comp_id CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.cancel_epi CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.comp_zero

CategoryTheory.ShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_homologyπ_eq_iff_up_to_refinements 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian homology homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup toCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc iCycles_g CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono instMonoICycles liftCycles_i CategoryTheory.Preadditive.add_comp toCycles_i
comp_homologyπ_eq_zero_iff_up_to_refinements 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian homology homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Epi X₁ toCycles	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc iCycles_g CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono instMonoICycles liftCycles_i toCycles_i
comp_pOpcycles_eq_zero_iff_up_to_refinements 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive opcycles hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian pOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Epi X₁ f	—	CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian f_pOpcycles
epi_homologyMap_iff_up_to_refinements 📖	mathematical	—	CategoryTheory.Epi homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian homologyMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.HasZeroMorphisms.zero X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Hom.τ₂ f	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.epi_iff_surjective_up_to_refinements hasLeftHomology_of_hasHomology eq_liftCycles_homologyπ_up_to_refinements CategoryTheory.whisker_eq comp_liftCycles_assoc CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_naturality liftCycles_comp_cyclesMap_assoc CategoryTheory.epi_comp CategoryTheory.Limits.comp_zero CategoryTheory.instEpiId CategoryTheory.Category.id_comp
eq_liftCycles_homologyπ_up_to_refinements 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₃ CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.HasZeroMorphisms.zero homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian cycles hasLeftHomology_of_hasHomology liftCycles homologyπ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.surjective_up_to_refinements_of_epi instEpiHomologyπ CategoryTheory.Category.assoc iCycles_g CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono instMonoICycles liftCycles_i
exact_iff_exact_up_to_refinements 📖	mathematical	—	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi X₁ CategoryTheory.CategoryStruct.comp X₂ f	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian exact_iff_epi_toCycles CategoryTheory.epi_iff_surjective_up_to_refinements CategoryTheory.Category.assoc liftCycles_i toCycles_i CategoryTheory.eq_whisker iCycles_g CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono instMonoICycles
liftCycles_comp_homologyπ_eq_iff_up_to_refinements 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian homology liftCycles homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi X₁ X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup f	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.Preadditive.sub_comp sub_self sub_eq_zero sub_liftCycles liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements CategoryTheory.Preadditive.comp_sub
liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian homology liftCycles homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Epi X₁ X₂ f	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian toCycles_comp_homologyπ CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc liftCycles_i toCycles_i
mono_homologyMap_iff_up_to_refinements 📖	mathematical	—	CategoryTheory.Mono homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian homologyMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi X₁ CategoryTheory.CategoryStruct.comp X₂ f	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.cancel_mono CategoryTheory.Category.assoc homologyπ_naturality liftCycles_comp_cyclesMap_assoc CategoryTheory.Limits.zero_comp liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements CategoryTheory.instEpiId CategoryTheory.Category.id_comp CategoryTheory.Preadditive.mono_iff_cancel_zero eq_liftCycles_homologyπ_up_to_refinements CategoryTheory.cancel_epi CategoryTheory.Limits.comp_zero CategoryTheory.whisker_eq Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.eq_whisker liftCycles_i toCycles_i CategoryTheory.epi_comp

CategoryTheory.ShortComplex.Exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_up_to_refinements 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements

---

← Back to Index