HomologicalComplexLimits

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

Statistics

Metric	Count
Definitions `coconeOfHasColimitEval`, `coneOfHasLimitEval`, `isColimitCoconeOfHasColimitEval`, `isColimitOfEval`, `isLimitConeOfHasLimitEval`, `isLimitOfEval`	6
Theorems `coconeOfHasColimitEval_pt_X`, `coconeOfHasColimitEval_pt_d`, `coconeOfHasColimitEval_ι_app_f`, `coneOfHasLimitEval_pt_X`, `coneOfHasLimitEval_pt_d`, `coneOfHasLimitEval_π_app_f`, `instEpiFOfHasFiniteColimits`, `instHasColimit`, `instHasColimitsOfShape`, `instHasFiniteColimits`, `instHasFiniteLimits`, `instHasLimit`, `instHasLimitsOfShape`, `instMonoFOfHasFiniteLimits`, `instPreservesColimitEval`, `instPreservesColimitsOfShapeEvalOfHasColimitsOfShape`, `instPreservesColimitsOfShapeSingle`, `instPreservesFiniteColimitsEvalOfHasFiniteColimits`, `instPreservesFiniteColimitsSingle`, `instPreservesFiniteLimitsEvalOfHasFiniteLimits`, `instPreservesFiniteLimitsSingle`, `instPreservesLimitEval`, `instPreservesLimitsOfShapeEvalOfHasLimitsOfShape`, `instPreservesLimitsOfShapeSingle`, `preservesColimitsOfShape_of_eval`, `preservesLimitsOfShape_of_eval`	26
Total	32

HomologicalComplex

Definitions

Name	Category	Theorems
`coconeOfHasColimitEval` 📖	CompOp	3 math math: `coconeOfHasColimitEval_pt_d`, `coconeOfHasColimitEval_pt_X`, `coconeOfHasColimitEval_ι_app_f`
`coneOfHasLimitEval` 📖	CompOp	3 math math: `coneOfHasLimitEval_pt_d`, `coneOfHasLimitEval_pt_X`, `coneOfHasLimitEval_π_app_f`
`isColimitCoconeOfHasColimitEval` 📖	CompOp	—
`isColimitOfEval` 📖	CompOp	—
`isLimitConeOfHasLimitEval` 📖	CompOp	—
`isLimitOfEval` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconeOfHasColimitEval_pt_X` 📖	mathematical	`CategoryTheory.Limits.HasColimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`X` `CategoryTheory.Limits.Cocone.pt` `coconeOfHasColimitEval` `CategoryTheory.Limits.colimit`	—	—
`coconeOfHasColimitEval_pt_d` 📖	mathematical	`CategoryTheory.Limits.HasColimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`d` `CategoryTheory.Limits.Cocone.pt` `coconeOfHasColimitEval` `CategoryTheory.Limits.colimMap` `CategoryTheory.Functor.obj`	—	—
`coconeOfHasColimitEval_ι_app_f` 📖	mathematical	`CategoryTheory.Limits.HasColimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.colimit` `CategoryTheory.Limits.colimMap` `d` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `coconeOfHasColimitEval` `CategoryTheory.Limits.colimit.ι`	—	—
`coneOfHasLimitEval_pt_X` 📖	mathematical	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`X` `CategoryTheory.Limits.Cone.pt` `coneOfHasLimitEval` `CategoryTheory.Limits.limit`	—	—
`coneOfHasLimitEval_pt_d` 📖	mathematical	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`d` `CategoryTheory.Limits.Cone.pt` `coneOfHasLimitEval` `CategoryTheory.Limits.limMap` `CategoryTheory.Functor.obj`	—	—
`coneOfHasLimitEval_π_app_f` 📖	mathematical	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.limit` `CategoryTheory.Limits.limMap` `d` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π` `coneOfHasLimitEval` `CategoryTheory.Limits.limit.π`	—	—
`instEpiFOfHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Epi` `X` `Hom.f`	—	`CategoryTheory.Functor.map_epi` `CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape` `instPreservesColimitsOfShapeEvalOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits`
`instHasColimit` 📖	—	`CategoryTheory.Limits.HasColimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	—	—	—
`instHasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `HomologicalComplex` `instCategory`	—	`instHasColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape`
`instHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteColimits` `HomologicalComplex` `instCategory`	—	`instHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits`
`instHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `HomologicalComplex` `instCategory`	—	`instHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits`
`instHasLimit` 📖	—	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	—	—	—
`instHasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `HomologicalComplex` `instCategory`	—	`instHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape`
`instMonoFOfHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Mono` `X` `Hom.f`	—	`CategoryTheory.Functor.map_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `instPreservesLimitsOfShapeEvalOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits`
`instPreservesColimitEval` 📖	mathematical	`CategoryTheory.Limits.HasColimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`CategoryTheory.Limits.PreservesColimit`	—	`CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone`
`instPreservesColimitsOfShapeEvalOfHasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `HomologicalComplex` `instCategory` `eval`	—	`instPreservesColimitEval` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape`
`instPreservesColimitsOfShapeSingle` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `HomologicalComplex` `instCategory` `single`	—	`preservesColimitsOfShape_of_eval` `CategoryTheory.Limits.preservesColimitsOfShape_of_natIso` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Functor.isEquivalence_refl` `CategoryTheory.Functor.preservesColimitsOfShape_of_isZero` `isZero_single_comp_eval`
`instPreservesFiniteColimitsEvalOfHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `HomologicalComplex` `instCategory` `eval`	—	`instPreservesColimitsOfShapeEvalOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits`
`instPreservesFiniteColimitsSingle` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `HomologicalComplex` `instCategory` `single`	—	`instPreservesColimitsOfShapeSingle`
`instPreservesFiniteLimitsEvalOfHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `HomologicalComplex` `instCategory` `eval`	—	`instPreservesLimitsOfShapeEvalOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits`
`instPreservesFiniteLimitsSingle` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `HomologicalComplex` `instCategory` `single`	—	`instPreservesLimitsOfShapeSingle`
`instPreservesLimitEval` 📖	mathematical	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	`CategoryTheory.Limits.PreservesLimit`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone`
`instPreservesLimitsOfShapeEvalOfHasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `HomologicalComplex` `instCategory` `eval`	—	`instPreservesLimitEval` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape`
`instPreservesLimitsOfShapeSingle` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `HomologicalComplex` `instCategory` `single`	—	`preservesLimitsOfShape_of_eval` `CategoryTheory.Limits.preservesLimitsOfShape_of_natIso` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Functor.isEquivalence_refl` `CategoryTheory.Functor.preservesLimitsOfShape_of_isZero` `isZero_single_comp_eval`
`preservesColimitsOfShape_of_eval` 📖	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	—	—	`CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit`
`preservesLimitsOfShape_of_eval` 📖	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `CategoryTheory.Functor.comp` `HomologicalComplex` `instCategory` `eval`	—	—	`CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit`

---

← Back to Index