ExactSequence

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

Statistics

Metric	Count
Definitions sc, sc', IsComplex, sc, sc', sc'Map, sc'MapIso, scMap, scMapIso, mapToComposableArrows, toComposableArrows	11
Theorems exact, exact', isIso_map', toIsComplex, δlast, δ₀, zero, zero', zero'_assoc, zero_assoc, exact_iff_of_iso, exact_iff_δlast, exact_iff_δ₀, exact_of_iso, exact_of_δlast, exact_of_δ₀, exact₀, exact₁, exact₂_iff, exact₂_mk, isComplex_iff_of_iso, isComplex_of_iso, isComplex₀, isComplex₁, isComplex₂_iff, isComplex₂_mk, sc'MapIso_hom, sc'MapIso_inv, sc'Map_τ₁, sc'Map_τ₂, sc'Map_τ₃, scMapIso_hom, scMapIso_inv, scMap_τ₁, scMap_τ₂, scMap_τ₃, exact_toComposableArrows, exact_iff_exact_toComposableArrows, isComplex_toComposableArrows, mapToComposableArrows_app_0, mapToComposableArrows_app_1, mapToComposableArrows_app_2, mapToComposableArrows_comp, mapToComposableArrows_id, toComposableArrows_map, toComposableArrows_obj	46
Total	57

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
IsComplex 📖	CompData	7 math math: CategoryTheory.ShortComplex.isComplex_toComposableArrows, Exact.toIsComplex, isComplex₁, isComplex₂_mk, isComplex₂_iff, isComplex₀, isComplex_iff_of_iso
sc 📖	CompOp	8 math math: scMap_τ₁, IsComplex.opcyclesToCycles_fac_assoc, IsComplex.opcyclesToCycles_fac, scMapIso_inv, scMapIso_hom, scMap_τ₃, scMap_τ₂, Exact.exact
sc' 📖	CompOp	7 math math: sc'MapIso_inv, sc'MapIso_hom, sc'Map_τ₁, sc'Map_τ₃, exact₂_iff, Exact.exact', sc'Map_τ₂
sc'Map 📖	CompOp	5 math math: sc'MapIso_inv, sc'MapIso_hom, sc'Map_τ₁, sc'Map_τ₃, sc'Map_τ₂
sc'MapIso 📖	CompOp	2 math math: sc'MapIso_inv, sc'MapIso_hom
scMap 📖	CompOp	5 math math: scMap_τ₁, scMapIso_inv, scMapIso_hom, scMap_τ₃, scMap_τ₂
scMapIso 📖	CompOp	2 math math: scMapIso_inv, scMapIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_iff_of_iso 📖	mathematical	—	Exact	—	exact_of_iso
exact_iff_δlast 📖	mathematical	—	Exact δlast mk₂ CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map'	—	IsComplex.zero Exact.toIsComplex Exact.exact isComplex₂_iff exact₂_iff LE.le.lt_or_eq
exact_iff_δ₀ 📖	mathematical	—	Exact mk₂ CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' δ₀	—	isComplex₂_iff IsComplex.zero Exact.toIsComplex exact₂_iff Exact.exact
exact_of_iso 📖	—	Exact	—	—	isComplex_of_iso Exact.toIsComplex CategoryTheory.ShortComplex.exact_of_iso Exact.exact
exact_of_δlast 📖	—	Exact δlast mk₂ CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map'	—	—	exact_iff_δlast
exact_of_δ₀ 📖	—	Exact mk₂ CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' δ₀	—	—	exact_iff_δ₀
exact₀ 📖	mathematical	—	Exact	—	isComplex₀ Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
exact₁ 📖	mathematical	—	Exact	—	isComplex₁
exact₂_iff 📖	mathematical	IsComplex	Exact CategoryTheory.ShortComplex.Exact sc'	—	Exact.exact
exact₂_mk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.Exact	Exact	—	exact₂_iff
isComplex_iff_of_iso 📖	mathematical	—	IsComplex	—	isComplex_of_iso
isComplex_of_iso 📖	—	IsComplex	—	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Limits.comp_zero CategoryTheory.NatTrans.naturality_assoc CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' IsComplex.zero CategoryTheory.Limits.zero_comp
isComplex₀ 📖	mathematical	—	IsComplex	—	Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
isComplex₁ 📖	mathematical	—	IsComplex	—	—
isComplex₂_iff 📖	mathematical	—	IsComplex CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	IsComplex.zero
isComplex₂_mk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	IsComplex	—	isComplex₂_iff
sc'MapIso_hom 📖	mathematical	IsComplex	CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory sc' sc'MapIso sc'Map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
sc'MapIso_inv 📖	mathematical	IsComplex	CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory sc' sc'MapIso sc'Map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
sc'Map_τ₁ 📖	mathematical	IsComplex	CategoryTheory.ShortComplex.Hom.τ₁ sc' sc'Map CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
sc'Map_τ₂ 📖	mathematical	IsComplex	CategoryTheory.ShortComplex.Hom.τ₂ sc' sc'Map CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
sc'Map_τ₃ 📖	mathematical	IsComplex	CategoryTheory.ShortComplex.Hom.τ₃ sc' sc'Map CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
scMapIso_hom 📖	mathematical	IsComplex	CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory sc scMapIso scMap CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
scMapIso_inv 📖	mathematical	IsComplex	CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory sc scMapIso scMap CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
scMap_τ₁ 📖	mathematical	IsComplex	CategoryTheory.ShortComplex.Hom.τ₁ sc scMap CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
scMap_τ₂ 📖	mathematical	IsComplex	CategoryTheory.ShortComplex.Hom.τ₂ sc scMap CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
scMap_τ₃ 📖	mathematical	IsComplex	CategoryTheory.ShortComplex.Hom.τ₃ sc scMap CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—

CategoryTheory.ComposableArrows.Exact

Definitions

Name	Category	Theorems
sc 📖	CompOp	2 math math: opcyclesIsoCycles_hom_fac_assoc, opcyclesIsoCycles_hom_fac
sc' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact 📖	mathematical	CategoryTheory.ComposableArrows.Exact	CategoryTheory.ShortComplex.Exact CategoryTheory.ComposableArrows.sc toIsComplex	—	—
exact' 📖	mathematical	CategoryTheory.ComposableArrows.Exact	CategoryTheory.ShortComplex.Exact CategoryTheory.ComposableArrows.sc' toIsComplex	—	toIsComplex exact
isIso_map' 📖	mathematical	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.IsIso	—	toIsComplex CategoryTheory.ShortComplex.Exact.mono_g exact CategoryTheory.ShortComplex.Exact.epi_f CategoryTheory.isIso_of_mono_of_epi
toIsComplex 📖	mathematical	CategoryTheory.ComposableArrows.Exact	CategoryTheory.ComposableArrows.IsComplex	—	—
δlast 📖	mathematical	CategoryTheory.ComposableArrows.Exact	CategoryTheory.ComposableArrows.δlast	—	CategoryTheory.ComposableArrows.exact_iff_δlast
δ₀ 📖	mathematical	CategoryTheory.ComposableArrows.Exact	CategoryTheory.ComposableArrows.δ₀	—	CategoryTheory.ComposableArrows.exact_iff_δ₀

CategoryTheory.ComposableArrows.IsComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zero 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
zero' 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	zero
zero'_assoc 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' zero'
zero_assoc 📖	mathematical	CategoryTheory.ComposableArrows.IsComplex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' zero

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
mapToComposableArrows 📖	CompOp	5 math math: mapToComposableArrows_app_0, mapToComposableArrows_app_1, mapToComposableArrows_comp, mapToComposableArrows_app_2, mapToComposableArrows_id
toComposableArrows 📖	CompOp	10 math math: mapToComposableArrows_app_0, isComplex_toComposableArrows, mapToComposableArrows_app_1, exact_iff_exact_toComposableArrows, mapToComposableArrows_comp, mapToComposableArrows_app_2, toComposableArrows_map, Exact.exact_toComposableArrows, toComposableArrows_obj, mapToComposableArrows_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_iff_exact_toComposableArrows 📖	mathematical	—	Exact CategoryTheory.ComposableArrows.Exact toComposableArrows	—	isComplex_toComposableArrows CategoryTheory.ComposableArrows.exact₂_iff
isComplex_toComposableArrows 📖	mathematical	—	CategoryTheory.ComposableArrows.IsComplex toComposableArrows	—	zero
mapToComposableArrows_app_0 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows mapToComposableArrows Hom.τ₁	—	—
mapToComposableArrows_app_1 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows mapToComposableArrows Hom.τ₂	—	—
mapToComposableArrows_app_2 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows mapToComposableArrows Hom.τ₃	—	—
mapToComposableArrows_comp 📖	mathematical	—	mapToComposableArrows CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows	—	CategoryTheory.ComposableArrows.hom_ext₂
mapToComposableArrows_id 📖	mathematical	—	mapToComposableArrows CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows	—	CategoryTheory.ComposableArrows.hom_ext₂
toComposableArrows_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows CategoryTheory.ComposableArrows.Precomp.map CategoryTheory.ComposableArrows.mk₁ X₂ X₃ g X₁ f	—	—
toComposableArrows_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder toComposableArrows CategoryTheory.ComposableArrows.Precomp.obj CategoryTheory.ComposableArrows.mk₁ X₂ X₃ g X₁	—	—

CategoryTheory.ShortComplex.Exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_toComposableArrows 📖	mathematical	CategoryTheory.ShortComplex.Exact	CategoryTheory.ComposableArrows.Exact CategoryTheory.ShortComplex.toComposableArrows	—	CategoryTheory.ShortComplex.zero

---

← Back to Index