Documentation Verification Report

EventuallyConstant

📁 Source: Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean

Statistics

Metric	Count
Definitions `IsEventuallyConstantFrom`, `cocone`, `coconeιApp`, `isColimitCocone`, `isColimitOfIsIso`, `isoMap`, `IsEventuallyConstantTo`, `cone`, `coneπApp`, `isLimitCone`, `isLimitOfIsIso`, `isoMap`, `IsEventuallyConstant`, `IsEventuallyConstant`	14
Theorems `cocone_pt`, `cocone_ι_app`, `coconeιApp_eq`, `coconeιApp_eq_id`, `hasColimit`, `isIso_map`, `isIso_ι_of_isColimit`, `isIso_ι_of_isColimit'`, `isoMap_hom`, `isoMap_hom_inv_id`, `isoMap_hom_inv_id_assoc`, `isoMap_inv_hom_id`, `isoMap_inv_hom_id_assoc`, `postcomp`, `cone_pt`, `cone_π_app`, `coneπApp_eq`, `coneπApp_eq_id`, `hasLimit`, `isIso_map`, `isIso_π_of_isLimit`, `isIso_π_of_isLimit'`, `isoMap_hom`, `isoMap_hom_inv_id`, `isoMap_hom_inv_id_assoc`, `isoMap_inv_hom_id`, `isoMap_inv_hom_id_assoc`, `precomp`, `exists_isEventuallyConstantTo`, `instHasLimitOfIsEventuallyConstant`, `exists_isEventuallyConstantFrom`, `instHasColimitOfIsEventuallyConstant`	32
Total	46

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`IsEventuallyConstantFrom` 📖	MathDef	1 math math: `CategoryTheory.IsFiltered.IsEventuallyConstant.exists_isEventuallyConstantFrom`
`IsEventuallyConstantTo` 📖	MathDef	1 math math: `CategoryTheory.IsCofiltered.IsEventuallyConstant.exists_isEventuallyConstantTo`

CategoryTheory.Functor.IsEventuallyConstantFrom

Definitions

Name	Category	Theorems
`cocone` 📖	CompOp	2 math math: `cocone_ι_app`, `cocone_pt`
`coconeιApp` 📖	CompOp	3 math math: `cocone_ι_app`, `coconeιApp_eq`, `coconeιApp_eq_id`
`isColimitCocone` 📖	CompOp	—
`isColimitOfIsIso` 📖	CompOp	—
`isoMap` 📖	CompOp	6 math math: `isoMap_hom_inv_id`, `isoMap_inv_hom_id_assoc`, `isoMap_inv_hom_id`, `isoMap_hom`, `coconeιApp_eq`, `isoMap_hom_inv_id_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_pt` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.Limits.Cocone.pt` `cocone` `CategoryTheory.Functor.obj`	—	—
`cocone_ι_app` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `cocone` `coconeιApp`	—	—
`coconeιApp_eq` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`coconeιApp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `isoMap` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `CategoryTheory.IsFiltered.bowtie` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.assoc` `isoMap_hom` `isoMap_inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.map_comp` `isoMap_inv_hom_id_assoc`
`coconeιApp_eq_id` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`coconeιApp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`coconeιApp_eq` `isoMap_hom_inv_id`
`hasColimit` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.Limits.HasColimit`	—	—
`isIso_map` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsIso.of_isIso_fac_left` `CategoryTheory.Functor.map_comp`
`isIso_ι_of_isColimit` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv` `coconeιApp_eq_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.isIso_inv`
`isIso_ι_of_isColimit'` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`isIso_ι_of_isColimit` `postcomp`
`isoMap_hom` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `isoMap` `CategoryTheory.Functor.map`	—	—
`isoMap_hom_inv_id` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `isoMap` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Iso.hom_inv_id`
`isoMap_hom_inv_id_assoc` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `isoMap`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `isoMap_hom_inv_id`
`isoMap_inv_hom_id` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `isoMap` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Iso.inv_hom_id`
`isoMap_inv_hom_id_assoc` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantFrom`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `isoMap` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `isoMap_inv_hom_id`
`postcomp` 📖	—	`CategoryTheory.Functor.IsEventuallyConstantFrom`	—	—	`isIso_map`

CategoryTheory.Functor.IsEventuallyConstantTo

Definitions

Name	Category	Theorems
`cone` 📖	CompOp	2 math math: `cone_π_app`, `cone_pt`
`coneπApp` 📖	CompOp	3 math math: `coneπApp_eq`, `cone_π_app`, `coneπApp_eq_id`
`isLimitCone` 📖	CompOp	—
`isLimitOfIsIso` 📖	CompOp	—
`isoMap` 📖	CompOp	6 math math: `coneπApp_eq`, `isoMap_inv_hom_id`, `isoMap_hom`, `isoMap_hom_inv_id`, `isoMap_hom_inv_id_assoc`, `isoMap_inv_hom_id_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cone_pt` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.Limits.Cone.pt` `cone` `CategoryTheory.Functor.obj`	—	—
`cone_π_app` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π` `cone` `coneπApp`	—	—
`coneπApp_eq` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`coneπApp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `isoMap` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty` `CategoryTheory.IsCofiltered.bowtie` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `isoMap_hom` `isoMap_hom_inv_id_assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.map_comp_assoc`
`coneπApp_eq_id` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`coneπApp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`coneπApp_eq` `isoMap_inv_hom_id`
`hasLimit` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.Limits.HasLimit`	—	—
`isIso_map` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsIso.of_isIso_fac_right` `CategoryTheory.Functor.map_comp`
`isIso_π_of_isLimit` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	—	`CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp` `coneπApp_eq_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.isIso_hom`
`isIso_π_of_isLimit'` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	—	`isIso_π_of_isLimit` `precomp`
`isoMap_hom` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `isoMap` `CategoryTheory.Functor.map`	—	—
`isoMap_hom_inv_id` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `isoMap` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Iso.hom_inv_id`
`isoMap_hom_inv_id_assoc` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `isoMap`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `isoMap_hom_inv_id`
`isoMap_inv_hom_id` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `isoMap` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Iso.inv_hom_id`
`isoMap_inv_hom_id_assoc` 📖	mathematical	`CategoryTheory.Functor.IsEventuallyConstantTo`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `isoMap` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `isoMap_inv_hom_id`
`precomp` 📖	—	`CategoryTheory.Functor.IsEventuallyConstantTo`	—	—	`isIso_map`

CategoryTheory.IsCofiltered

Definitions

Name	Category	Theorems
`IsEventuallyConstant` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasLimitOfIsEventuallyConstant` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit`	—	`IsEventuallyConstant.exists_isEventuallyConstantTo` `CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit`

CategoryTheory.IsCofiltered.IsEventuallyConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isEventuallyConstantTo` 📖	mathematical	—	`CategoryTheory.Functor.IsEventuallyConstantTo`	—	—

CategoryTheory.IsFiltered

Definitions

Name	Category	Theorems
`IsEventuallyConstant` 📖	CompData	4 math math: `CategoryTheory.isEventuallyConstant_of_isArtinianObject`, `CategoryTheory.isEventuallyConstant_of_isNoetherianObject`, `CategoryTheory.isNoetherianObject_iff_isEventuallyConstant`, `CategoryTheory.isArtinianObject_iff_isEventuallyConstant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasColimitOfIsEventuallyConstant` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit`	—	`IsEventuallyConstant.exists_isEventuallyConstantFrom` `CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit`

CategoryTheory.IsFiltered.IsEventuallyConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isEventuallyConstantFrom` 📖	mathematical	—	`CategoryTheory.Functor.IsEventuallyConstantFrom`	—	—

---

← Back to Index