Refinements

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

Statistics

Metric	Count
Definitions	0
Theorems exact_up_to_refinements, eq_liftCycles_homologyπ_up_to_refinements, exact_iff_exact_up_to_refinements, epi_iff_surjective_up_to_refinements, surjective_up_to_refinements_of_epi	5
Total	5

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_surjective_up_to_refinements 📖	mathematical	—	Epi CategoryStruct.comp Category.toCategoryStruct	—	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	—	CategoryStruct.comp Category.toCategoryStruct	—	epi_iff_surjective_up_to_refinements

CategoryTheory.ShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_liftCycles_homologyπ_up_to_refinements 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ 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

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	CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements

---

← Back to Index