Extensions

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Extensions.lean

Statistics

Metric	Count
Definitions IsClosedUnderExtensions	1
Theorems prop_X₂_of_shortExact, instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits, instIsClosedUnderExtensionsIsZero, instIsClosedUnderExtensionsTop, prop_X₂_of_shortExact, prop_biprod	6
Total	7

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsClosedUnderExtensions 📖	CompData	4 math math: instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits, instIsClosedUnderExtensionsTop, instIsClosedUnderExtensionsIsZero, IsSerreClass.toIsClosedUnderExtensions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits 📖	mathematical	—	IsClosedUnderExtensions inverseImage	—	CategoryTheory.ShortComplex.ShortExact.mono_f CategoryTheory.ShortComplex.ShortExact.epi_g prop_X₂_of_shortExact CategoryTheory.ShortComplex.ShortExact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits
instIsClosedUnderExtensionsIsZero 📖	mathematical	—	IsClosedUnderExtensions CategoryTheory.Limits.IsZero	—	CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros CategoryTheory.ShortComplex.ShortExact.exact CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.IsZero.eq_of_tgt
instIsClosedUnderExtensionsTop 📖	mathematical	—	IsClosedUnderExtensions Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	—
prop_X₂_of_shortExact 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₃	CategoryTheory.ShortComplex.X₂	—	IsClosedUnderExtensions.prop_X₂_of_shortExact
prop_biprod 📖	mathematical	—	CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	prop_X₂_of_shortExact CategoryTheory.ShortComplex.Splitting.shortExact

CategoryTheory.ObjectProperty.IsClosedUnderExtensions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prop_X₂_of_shortExact 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₃	CategoryTheory.ShortComplex.X₂	—	—

---

← Back to Index