Four

📁 Source: Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_of_epi_of_epi_of_epi, epi_of_epi_of_epi_of_mono, epi_of_epi_of_epi_of_mono', epi_of_mono_of_epi_of_mono, epi_of_mono_of_epi_of_mono', isIso_of_epi_of_isIso_of_isIso_of_mono, mono_of_epi_of_epi_mono', mono_of_epi_of_epi_of_mono, mono_of_epi_of_mono_of_mono, mono_of_epi_of_mono_of_mono', mono_of_mono_of_mono_of_mono, epi_of_epi_of_epi_of_epi, epi_of_mono_of_epi_of_mono, mono_of_epi_of_epi_of_mono, mono_of_mono_of_mono_of_mono	15
Total	15

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_of_epi_of_epi_of_epi 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.Epi CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	le_rfl CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero epi_of_epi_of_epi_of_mono' CategoryTheory.ShortComplex.exact_iff_epi hasZeroObject CategoryTheory.ShortComplex.Exact.exact_toComposableArrows CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.instMonoId
epi_of_epi_of_epi_of_mono 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.Epi CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	epi_of_epi_of_epi_of_mono' CategoryTheory.ShortComplex.Exact.exact_toComposableArrows CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ComposableArrows.Exact.exact le_rfl CategoryTheory.ComposableArrows.map'_comp CategoryTheory.ComposableArrows.IsComplex.zero
epi_of_epi_of_epi_of_mono' 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.ComposableArrows.mk₂ CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Epi CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	CategoryTheory.epi_iff_surjective_up_to_refinements CategoryTheory.surjective_up_to_refinements_of_epi le_rfl CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp CategoryTheory.NatTrans.naturality Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.ComposableArrows.map'_comp CategoryTheory.Limits.comp_zero CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ShortComplex.Exact.exact_up_to_refinements CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.Preadditive.sub_comp sub_self CategoryTheory.epi_comp CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_sub add_sub_cancel
epi_of_mono_of_epi_of_mono 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.Epi CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	epi_of_mono_of_epi_of_mono' le_rfl CategoryTheory.ComposableArrows.map'_comp CategoryTheory.ComposableArrows.IsComplex.zero CategoryTheory.ComposableArrows.Exact.toIsComplex
epi_of_mono_of_epi_of_mono' 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Epi CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	le_rfl CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.ComposableArrows.naturality' epi_of_epi_of_epi_of_mono' CategoryTheory.ShortComplex.Exact.exact_toComposableArrows CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.ShortComplex.exact_iff_mono hasZeroObject CategoryTheory.Functor.map_comp CategoryTheory.instEpiId
isIso_of_epi_of_isIso_of_isIso_of_mono 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.IsIso CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	mono_of_epi_of_mono_of_mono CategoryTheory.ComposableArrows.exact_iff_δlast CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso epi_of_epi_of_epi_of_mono CategoryTheory.ComposableArrows.exact_iff_δ₀ CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory
mono_of_epi_of_epi_mono' 📖	mathematical	CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.ComposableArrows.Exact	CategoryTheory.Mono CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	le_rfl CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero mono_of_epi_of_mono_of_mono' CategoryTheory.Functor.map_comp CategoryTheory.ShortComplex.exact_iff_epi hasZeroObject CategoryTheory.ShortComplex.Exact.exact_toComposableArrows CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.instMonoId
mono_of_epi_of_epi_of_mono 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.Mono CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	mono_of_epi_of_epi_mono' le_rfl CategoryTheory.ComposableArrows.map'_comp CategoryTheory.ComposableArrows.IsComplex.zero CategoryTheory.ComposableArrows.Exact.toIsComplex
mono_of_epi_of_mono_of_mono 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.Mono CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	mono_of_epi_of_mono_of_mono' CategoryTheory.ComposableArrows.map'_comp CategoryTheory.ComposableArrows.IsComplex.zero CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ShortComplex.Exact.exact_toComposableArrows CategoryTheory.ComposableArrows.Exact.exact
mono_of_epi_of_mono_of_mono' 📖	mathematical	CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.ComposableArrows.Exact CategoryTheory.ComposableArrows.mk₂	CategoryTheory.Mono CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	CategoryTheory.Preadditive.mono_of_cancel_zero le_rfl CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ShortComplex.Exact.exact_up_to_refinements CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.Limits.comp_zero CategoryTheory.surjective_up_to_refinements_of_epi CategoryTheory.cancel_epi CategoryTheory.ComposableArrows.map'_comp
mono_of_mono_of_mono_of_mono 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	CategoryTheory.Mono CategoryTheory.ComposableArrows.obj' CategoryTheory.ComposableArrows.app'	—	le_rfl CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.ComposableArrows.naturality' mono_of_epi_of_mono_of_mono' CategoryTheory.ShortComplex.Exact.exact_toComposableArrows CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.ShortComplex.exact_iff_mono hasZeroObject CategoryTheory.instEpiId

CategoryTheory.ShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_of_epi_of_epi_of_epi 📖	mathematical	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Epi X₂ Hom.τ₂	—	CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi Exact.exact_toComposableArrows
epi_of_mono_of_epi_of_mono 📖	mathematical	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Epi X₁ Hom.τ₁	—	CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono' Exact.exact_toComposableArrows zero
mono_of_epi_of_epi_of_mono 📖	mathematical	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Mono X₃ Hom.τ₃	—	CategoryTheory.Abelian.mono_of_epi_of_epi_mono' zero Exact.exact_toComposableArrows
mono_of_mono_of_mono_of_mono 📖	mathematical	Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Mono X₂ Hom.τ₂	—	CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono Exact.exact_toComposableArrows

---

← Back to Index