Exact

📁 Source: Mathlib/CategoryTheory/Functor/ReflectsIso/Exact.lean

Statistics

Metric	Count
Definitions Exact	1
Theorems exactAt_iff, exact_iff, isZero_iff, quasiIsoAt_iff, quasiIso_iff, shortComplexQuasiIso_iff, shortExact_iff	7
Total	8

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
Exact 📖	CompData	28 math math: CategoryTheory.Abelian.SpectralObject.exact₁', exact_iff_δlast, CategoryTheory.Abelian.SpectralObject.sequenceΨ_exact, exact₀, exact_iff_δ₀, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, CategoryTheory.Abelian.SpectralObject.exact₂', CategoryTheory.ShortComplex.exact_iff_exact_toComposableArrows, CategoryTheory.Functor.homologySequenceComposableArrows₅_exact, exact₂_mk, CategoryTheory.kernelCokernelCompSequence_exact, CategoryTheory.Abelian.SpectralObject.exact₃', CategoryTheory.Abelian.Ext.covariantSequence_exact, exact_iff_of_iso, CategoryTheory.Abelian.SpectralObject.composableArrows₅_exact, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, exact_of_iso, exact₂_iff, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, exact_of_δlast, HomologicalComplex.HomologySequence.composableArrows₂_exact, HomologicalComplex.HomologySequence.composableArrows₃_exact, Exact.δlast, exact_of_δ₀, CategoryTheory.Abelian.Ext.contravariantSequence_exact, exact₁, Exact.δ₀

CategoryTheory.JointlyReflectIsomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exactAt_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Functor.PreservesHomology	HomologicalComplex.ExactAt CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex	—	exact_iff
exact_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Functor.PreservesHomology	CategoryTheory.ShortComplex.Exact CategoryTheory.ShortComplex.map	—	CategoryTheory.ShortComplex.Exact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.CategoryWithHomology.hasHomology isZero_iff CategoryTheory.Limits.IsZero.of_iso CategoryTheory.ShortComplex.hasHomology_of_preserves
isZero_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Functor.PreservesZeroMorphisms	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_isZero isIso_iff CategoryTheory.Limits.IsZero.isIso CategoryTheory.Limits.isZero_zero CategoryTheory.Limits.IsZero.of_iso
quasiIsoAt_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.PreservesFiniteColimits	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.finCategoryDiscreteOfFintype Fintype.instPEmpty CategoryTheory.Functor.empty CategoryTheory.Functor.map CategoryTheory.categoryWithHomology_of_abelian	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.categoryWithHomology_of_abelian quasiIsoAt_iff' shortComplexQuasiIso_iff
quasiIso_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.PreservesFiniteColimits	QuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.finCategoryDiscreteOfFintype Fintype.instPEmpty CategoryTheory.Functor.empty CategoryTheory.Functor.map CategoryTheory.categoryWithHomology_of_abelian	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.categoryWithHomology_of_abelian quasiIsoAt_iff
shortComplexQuasiIso_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.PreservesFiniteColimits	CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.finCategoryDiscreteOfFintype Fintype.instPEmpty CategoryTheory.Functor.empty CategoryTheory.ShortComplex.hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Functor.map	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.ShortComplex.hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.ShortComplex.quasiIso_map_of_preservesRightHomology isIso_iff CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms
shortExact_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.PreservesFiniteColimits	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.finCategoryDiscreteOfFintype Fintype.instPEmpty CategoryTheory.Functor.empty	—	CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.ShortComplex.ShortExact.mono_f CategoryTheory.ShortComplex.ShortExact.epi_g CategoryTheory.ShortComplex.ShortExact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Functor.map_mono CategoryTheory.Functor.instPreservesMonomorphisms CategoryTheory.Functor.map_epi CategoryTheory.Functor.instPreservesEpimorphisms CategoryTheory.JointlyReflectMonomorphisms.mono_iff jointlyReflectMonomorphisms CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.JointlyReflectEpimorphisms.epi_iff jointlyReflectEpimorphisms CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Abelian.hasFiniteColimits exact_iff CategoryTheory.ShortComplex.ShortExact.exact

---

← Back to Index