Colim

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean

Statistics

Metric	Count
Definitions mapShortComplex	1
Theorems mono_ι_app_of_isFiltered, exact_mapShortComplex, mapShortComplex_X₁, mapShortComplex_X₂, mapShortComplex_X₃, mapShortComplex_f, mapShortComplex_g, map_epi', map_mono', instIsStableUnderCoproductsMonomorphismsOfAB4OfSize, instIsStableUnderFilteredColimitsMonomorphismsOfAB5OfSize, isStableUnderColimitsOfShape_monomorphisms	12
Total	13

CategoryTheory.Limits.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono_ι_app_of_isFiltered 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Under.w CategoryTheory.NatTrans.mono_of_mono_app CategoryTheory.Limits.colim.map_mono' CategoryTheory.IsFiltered.isConnected CategoryTheory.IsFiltered.under CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Under.final_forget CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id

CategoryTheory.Limits.colim

Definitions

Name	Category	Theorems
mapShortComplex 📖	CompOp	6 math math: mapShortComplex_g, mapShortComplex_f, mapShortComplex_X₃, exact_mapShortComplex, mapShortComplex_X₁, mapShortComplex_X₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_mapShortComplex 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₂ CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	mapShortComplex	—	CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint CategoryTheory.Limits.instIsLeftAdjointFunctorColim CategoryTheory.ShortComplex.exact_iff_of_iso CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.Limits.colimit.cocone_ι CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.ShortComplex.Exact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Adjunction.colim_preservesColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
mapShortComplex_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₂ CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	mapShortComplex	—	—
mapShortComplex_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₂ CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	mapShortComplex	—	—
mapShortComplex_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₂ CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	mapShortComplex	—	—
mapShortComplex_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₂ CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	mapShortComplex	—	—
mapShortComplex_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₂ CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	mapShortComplex	—	—
map_epi' 📖	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.cancel_epi CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
map_mono' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.Mono	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.monomorphisms CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.Limits.colimit.cocone_ι CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Functor.map_mono

CategoryTheory.MorphismProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStableUnderCoproductsMonomorphismsOfAB4OfSize 📖	mathematical	CategoryTheory.Limits.HasCoproducts	IsStableUnderCoproducts monomorphisms	—	isStableUnderColimitsOfShape_monomorphisms CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits CategoryTheory.AB4OfSize.ofShape
instIsStableUnderFilteredColimitsMonomorphismsOfAB5OfSize 📖	mathematical	—	IsStableUnderFilteredColimits monomorphisms	—	isStableUnderColimitsOfShape_monomorphisms CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits CategoryTheory.AB5OfSize.ofShape
isStableUnderColimitsOfShape_monomorphisms 📖	mathematical	—	IsStableUnderColimitsOfShape monomorphisms	—	CategoryTheory.NatTrans.mono_of_mono_app CategoryTheory.Limits.colim.map_mono'

---

← Back to Index