ExactSequenceFour

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

Statistics

Metric	Count
Definitions cokerIsoKer, cokerIsoKer', cokerToKer', opcyclesIsoCycles, cokerToKer, cokerToKer', opcyclesToCycles	7
Theorems cokerIsoKer'_hom, cokerIsoKer'_hom_inv_id, cokerIsoKer'_hom_inv_id_assoc, cokerIsoKer'_inv_hom_id, cokerIsoKer'_inv_hom_id_assoc, cokerIsoKer_hom_fac, cokerIsoKer_hom_fac_assoc, isIso_cokerToKer', opcyclesIsoCycles_hom_fac, opcyclesIsoCycles_hom_fac_assoc, cokerToKer'_fac, cokerToKer'_fac_assoc, cokerToKer_fac, cokerToKer_fac_assoc, epi_cokerToKer', mono_cokerToKer', opcyclesToCycles_fac, opcyclesToCycles_fac_assoc	18
Total	25

CategoryTheory.ComposableArrows.Exact

Definitions

Name	Category	Theorems
cokerIsoKer 📖	CompOp	2 math math: cokerIsoKer_hom_fac_assoc, cokerIsoKer_hom_fac
cokerIsoKer' 📖	CompOp	5 math math: cokerIsoKer'_hom_inv_id_assoc, cokerIsoKer'_hom, cokerIsoKer'_inv_hom_id, cokerIsoKer'_hom_inv_id, cokerIsoKer'_inv_hom_id_assoc
cokerToKer' 📖	CompOp	6 math math: cokerIsoKer'_hom_inv_id_assoc, cokerIsoKer'_hom, cokerIsoKer'_inv_hom_id, cokerIsoKer'_hom_inv_id, cokerIsoKer'_inv_hom_id_assoc, isIso_cokerToKer'
opcyclesIsoCycles 📖	CompOp	2 math math: opcyclesIsoCycles_hom_fac_assoc, opcyclesIsoCycles_hom_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokerIsoKer'_hom 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair 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.Limits.Cone.pt cokerIsoKer' cokerToKer'	—	—
cokerIsoKer'_hom_inv_id 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.Cone.pt cokerToKer' CategoryTheory.Iso.inv cokerIsoKer' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
cokerIsoKer'_hom_inv_id_assoc 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.Cone.pt cokerToKer' CategoryTheory.Iso.inv cokerIsoKer'	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cokerIsoKer'_hom_inv_id
cokerIsoKer'_inv_hom_id 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv cokerIsoKer' cokerToKer' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
cokerIsoKer'_inv_hom_id_assoc 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv cokerIsoKer' cokerToKer'	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cokerIsoKer'_inv_hom_id
cokerIsoKer_hom_fac 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.cokernel CategoryTheory.ComposableArrows.map' CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel CategoryTheory.Iso.hom cokerIsoKer CategoryTheory.Limits.kernel.ι	—	CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac toIsComplex
cokerIsoKer_hom_fac_assoc 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.cokernel CategoryTheory.ComposableArrows.map' CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel CategoryTheory.Iso.hom cokerIsoKer CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokerIsoKer_hom_fac
isIso_cokerToKer' 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.IsIso CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair 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.Limits.Cone.pt cokerToKer'	—	CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer' toIsComplex exact CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer' CategoryTheory.isIso_of_mono_of_epi
opcyclesIsoCycles_hom_fac 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ sc CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.pOpcycles CategoryTheory.ShortComplex.cycles CategoryTheory.Iso.hom opcyclesIsoCycles CategoryTheory.ShortComplex.iCycles CategoryTheory.ComposableArrows.map'	—	CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac toIsComplex
opcyclesIsoCycles_hom_fac_assoc 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ShortComplex.opcycles sc CategoryTheory.ShortComplex.pOpcycles CategoryTheory.ShortComplex.cycles CategoryTheory.Iso.hom opcyclesIsoCycles CategoryTheory.ShortComplex.iCycles CategoryTheory.ComposableArrows.map'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoCycles_hom_fac

CategoryTheory.ComposableArrows.IsComplex

Definitions

Name	Category	Theorems
cokerToKer 📖	CompOp	2 math math: cokerToKer_fac, cokerToKer_fac_assoc
cokerToKer' 📖	CompOp	4 math math: mono_cokerToKer', epi_cokerToKer', cokerToKer'_fac_assoc, cokerToKer'_fac
opcyclesToCycles 📖	CompOp	2 math math: opcyclesToCycles_fac_assoc, opcyclesToCycles_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokerToKer'_fac 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cofork.π CategoryTheory.Limits.Cone.pt cokerToKer' CategoryTheory.Limits.Fork.ι	—	CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc CategoryTheory.Limits.Fork.IsLimit.lift_ι
cokerToKer'_fac_assoc 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cofork.π CategoryTheory.Limits.Cone.pt cokerToKer' CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokerToKer'_fac
cokerToKer_fac 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.cokernel CategoryTheory.ComposableArrows.map' CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel cokerToKer CategoryTheory.Limits.kernel.ι	—	cokerToKer'_fac CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero
cokerToKer_fac_assoc 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Limits.cokernel CategoryTheory.ComposableArrows.map' CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel cokerToKer CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokerToKer_fac
epi_cokerToKer' 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.Exact CategoryTheory.ComposableArrows.sc	CategoryTheory.Epi CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair 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.Limits.Cone.pt cokerToKer'	—	CategoryTheory.ShortComplex.Exact.hasZeroObject CategoryTheory.ShortComplex.Exact.hasHomology CategoryTheory.Limits.Cofork.IsColimit.hom_ext CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f' CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.ShortComplex.LeftHomologyData.f'_i CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i CategoryTheory.Category.assoc cokerToKer'_fac CategoryTheory.epi_of_epi_fac
mono_cokerToKer' 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.Exact CategoryTheory.ComposableArrows.sc	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair 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.Limits.Cone.pt cokerToKer'	—	CategoryTheory.ShortComplex.Exact.hasZeroObject CategoryTheory.ShortComplex.Exact.hasHomology CategoryTheory.Limits.Fork.IsLimit.hom_ext CategoryTheory.ShortComplex.RightHomologyData.exact_iff_mono_g' CategoryTheory.cancel_epi CategoryTheory.ShortComplex.RightHomologyData.instEpiP CategoryTheory.ShortComplex.RightHomologyData.p_g' CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p cokerToKer'_fac CategoryTheory.mono_of_mono_fac
opcyclesToCycles_fac 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ComposableArrows.sc CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.pOpcycles CategoryTheory.ShortComplex.cycles opcyclesToCycles CategoryTheory.ShortComplex.iCycles CategoryTheory.ComposableArrows.map'	—	cokerToKer'_fac CategoryTheory.ShortComplex.f_pOpcycles CategoryTheory.ShortComplex.iCycles_g
opcyclesToCycles_fac_assoc 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ShortComplex.opcycles CategoryTheory.ComposableArrows.sc CategoryTheory.ShortComplex.pOpcycles CategoryTheory.ShortComplex.cycles opcyclesToCycles CategoryTheory.ShortComplex.iCycles CategoryTheory.ComposableArrows.map'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesToCycles_fac

---

← Back to Index