Documentation Verification Report

Cocartesian

📁 Source: Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean

Statistics

Metric	Count
Definitions `IsCocartesian`, `codomainUniqueUpToIso`, `map`, `IsStronglyCocartesian`, `codomainIsoOfBaseIso`, `map`	6
Theorems `ext`, `fac`, `fac_assoc`, `map_isHomLift`, `map_self`, `map_uniq`, `of_comp_iso`, `of_iso_comp`, `toIsHomLift`, `universal_property`, `comp`, `ext`, `fac`, `fac_assoc`, `isCocartesian_of_isStronglyCocartesian`, `isIso_of_base_isIso`, `map_comp_map`, `map_comp_map_assoc`, `map_isHomLift`, `map_self`, `map_uniq`, `of_comp`, `of_isIso`, `of_iso`, `toIsHomLift`, `universal_property`, `universal_property'`	27
Total	33

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`IsCocartesian` 📖	CompData	3 math math: `IsCocartesian.of_iso_comp`, `IsStronglyCocartesian.isCocartesian_of_isStronglyCocartesian`, `IsCocartesian.of_comp_iso`
`IsStronglyCocartesian` 📖	CompData	4 math math: `IsStronglyCocartesian.of_comp`, `IsStronglyCocartesian.comp`, `IsStronglyCocartesian.of_isIso`, `IsStronglyCocartesian.of_iso`

CategoryTheory.Functor.IsCocartesian

Definitions

Name	Category	Theorems
`codomainUniqueUpToIso` 📖	CompOp	—
`map` 📖	CompOp	5 math math: `map_isHomLift`, `fac_assoc`, `map_self`, `fac`, `map_uniq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—	`CategoryTheory.IsHomLift.comp_lift_id_right` `toIsHomLift` `map_uniq`
`fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `map`	—	`universal_property`
`fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`map_isHomLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `map`	—	`universal_property`
`map_self` 📖	mathematical	—	`map` `toIsHomLift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`toIsHomLift` `map_uniq` `CategoryTheory.IsHomLift.instIsHomLiftIdObj` `CategoryTheory.Category.comp_id`
`map_uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`map`	—	`universal_property`
`of_comp_iso` 📖	mathematical	—	`CategoryTheory.Functor.IsCocartesian` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom`	—	`CategoryTheory.IsHomLift.comp_lift_id_right` `toIsHomLift` `CategoryTheory.IsHomLift.comp_of_lift_id` `CategoryTheory.IsHomLift.lift_id_inv` `map_isHomLift` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `fac` `CategoryTheory.Iso.eq_inv_comp` `map_uniq`
`of_iso_comp` 📖	mathematical	—	`CategoryTheory.Functor.IsCocartesian` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom`	—	`CategoryTheory.IsHomLift.comp_lift_id_left` `toIsHomLift` `CategoryTheory.IsHomLift.lift_id_inv` `map_isHomLift` `CategoryTheory.Category.assoc` `fac` `CategoryTheory.Iso.hom_inv_id_assoc` `map_uniq`
`toIsHomLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift`	—	—
`universal_property` 📖	mathematical	—	`ExistsUnique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.IsHomLift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.comp`	—	—

CategoryTheory.Functor.IsStronglyCocartesian

Definitions

Name	Category	Theorems
`codomainIsoOfBaseIso` 📖	CompOp	—
`map` 📖	CompOp	7 math math: `map_comp_map_assoc`, `fac_assoc`, `map_comp_map`, `fac`, `map_isHomLift`, `map_uniq`, `map_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`CategoryTheory.Functor.IsStronglyCocartesian` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.IsHomLift.comp` `toIsHomLift` `CategoryTheory.Category.assoc` `map_isHomLift` `map.congr_simp` `fac` `map_uniq`
`ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—	`CategoryTheory.IsHomLift.comp` `toIsHomLift` `map_uniq`
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`map`	—	`universal_property`
`fac_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`isCocartesian_of_isStronglyCocartesian` 📖	mathematical	—	`CategoryTheory.Functor.IsCocartesian`	—	`toIsHomLift` `universal_property` `CategoryTheory.Category.comp_id`
`isIso_of_base_isIso` 📖	mathematical	—	`CategoryTheory.IsIso`	—	`toIsHomLift` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.IsHomLift.instIsHomLiftIdObj` `fac` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.IsHomLift.comp` `map_isHomLift` `CategoryTheory.IsHomLift.map` `ext` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`map_comp_map` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`map` `toIsHomLift`	—	`map_uniq` `toIsHomLift` `CategoryTheory.IsHomLift.comp` `map_isHomLift` `fac_assoc` `fac`
`map_comp_map_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`map` `toIsHomLift`	—	`toIsHomLift` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_comp_map`
`map_isHomLift` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.IsHomLift` `map`	—	`universal_property`
`map_self` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.comp_id` `toIsHomLift`	—	`toIsHomLift` `CategoryTheory.Category.comp_id` `map_uniq` `CategoryTheory.IsHomLift.instIsHomLiftIdObj`
`map_uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`map`	—	`universal_property`
`of_comp` 📖	mathematical	—	`CategoryTheory.Functor.IsStronglyCocartesian`	—	`CategoryTheory.Category.assoc` `CategoryTheory.IsHomLift.comp` `toIsHomLift` `map_isHomLift` `ext` `map.congr_simp` `fac` `map_uniq`
`of_isIso` 📖	mathematical	—	`CategoryTheory.Functor.IsStronglyCocartesian`	—	`of_iso`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.IsStronglyCocartesian` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.id_comp` `CategoryTheory.IsHomLift.isoOfIsoLift_inv_hom_id` `CategoryTheory.IsHomLift.comp` `CategoryTheory.IsHomLift.inv_lift` `CategoryTheory.Iso.inv_hom_id_assoc`
`toIsHomLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift`	—	—
`universal_property` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`ExistsUnique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.IsHomLift`	—	`universal_property'`
`universal_property'` 📖	mathematical	—	`ExistsUnique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.IsHomLift` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp`	—	—

---

← Back to Index