Documentation Verification Report

ParallelPair

📁 Source: Mathlib/CategoryTheory/Limits/Indization/ParallelPair.lean

Statistics

Metric	Count
Definitions `IndParallelPairPresentation`, `F₁`, `F₂`, `I`, `isColimit₁`, `isColimit₂`, `parallelPairIsoParallelPairCompYoneda`, `ι₁`, `ι₂`, `φ`, `ψ`, `ℐ`, `F₁`, `F₂`, `K`, `isColimit₁`, `isColimit₂`, `presentation`, `ι₁`, `ι₂`, `ψ`, `ϕ`, `instSmallCategoryI`	23
Theorems `hI`, `hf`, `hg`, `hf`, `hg`, `instIsFilteredI`, `nonempty_indParallelPairPresentation`	7
Total	30

CategoryTheory

Definitions

Name	Category	Theorems
`IndParallelPairPresentation` 📖	CompData	1 math math: `nonempty_indParallelPairPresentation`
`instSmallCategoryI` 📖	CompOp	1 math math: `instIsFilteredI`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFilteredI` 📖	mathematical	—	`IsFiltered` `IndParallelPairPresentation.I` `instSmallCategoryI`	—	`IndParallelPairPresentation.hI`
`nonempty_indParallelPairPresentation` 📖	mathematical	`Limits.IsIndObject`	`IndParallelPairPresentation`	—	—

CategoryTheory.IndParallelPairPresentation

Definitions

Name	Category	Theorems
`F₁` 📖	CompOp	2 math math: `hf`, `hg`
`F₂` 📖	CompOp	2 math math: `hf`, `hg`
`I` 📖	CompOp	4 math math: `hf`, `CategoryTheory.instIsFilteredI`, `hg`, `hI`
`isColimit₁` 📖	CompOp	2 math math: `hf`, `hg`
`isColimit₂` 📖	CompOp	—
`parallelPairIsoParallelPairCompYoneda` 📖	CompOp	—
`ι₁` 📖	CompOp	2 math math: `hf`, `hg`
`ι₂` 📖	CompOp	2 math math: `hf`, `hg`
`φ` 📖	CompOp	1 math math: `hf`
`ψ` 📖	CompOp	1 math math: `hg`
`ℐ` 📖	CompOp	3 math math: `hf`, `hg`, `hI`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hI` 📖	mathematical	—	`CategoryTheory.IsFiltered` `I` `ℐ`	—	—
`hf` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.map` `I` `ℐ` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `F₁` `CategoryTheory.yoneda` `F₂` `ι₁` `isColimit₁` `ι₂` `CategoryTheory.Functor.whiskerRight` `φ`	—	—
`hg` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.map` `I` `ℐ` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `F₁` `CategoryTheory.yoneda` `F₂` `ι₁` `isColimit₁` `ι₂` `CategoryTheory.Functor.whiskerRight` `ψ`	—	—

CategoryTheory.NonemptyParallelPairPresentationAux

Definitions

Name	Category	Theorems
`F₁` 📖	CompOp	2 math math: `hf`, `hg`
`F₂` 📖	CompOp	2 math math: `hf`, `hg`
`K` 📖	CompOp	2 math math: `hf`, `hg`
`isColimit₁` 📖	CompOp	2 math math: `hf`, `hg`
`isColimit₂` 📖	CompOp	—
`presentation` 📖	CompOp	—
`ι₁` 📖	CompOp	2 math math: `hf`, `hg`
`ι₂` 📖	CompOp	2 math math: `hf`, `hg`
`ψ` 📖	CompOp	1 math math: `hg`
`ϕ` 📖	CompOp	1 math math: `hf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hf` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.map` `K` `CategoryTheory.commaCategory` `CategoryTheory.Limits.IndObjectPresentation.I` `CategoryTheory.Limits.IndObjectPresentation.instSmallCategoryI` `CategoryTheory.CostructuredArrow` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.prod'` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.Functor.prod'` `CategoryTheory.Functor.comp` `CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow` `CategoryTheory.CostructuredArrow.map` `F₁` `F₂` `ι₁` `isColimit₁` `ι₂` `CategoryTheory.Functor.whiskerRight` `ϕ`	—	`CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.ι_map` `CategoryTheory.Discrete.functor_map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.CommaMorphism.w`
`hg` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.map` `K` `CategoryTheory.commaCategory` `CategoryTheory.Limits.IndObjectPresentation.I` `CategoryTheory.Limits.IndObjectPresentation.instSmallCategoryI` `CategoryTheory.CostructuredArrow` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.prod'` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.Functor.prod'` `CategoryTheory.Functor.comp` `CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow` `CategoryTheory.CostructuredArrow.map` `F₁` `F₂` `ι₁` `isColimit₁` `ι₂` `CategoryTheory.Functor.whiskerRight` `ψ`	—	`CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.ι_map` `CategoryTheory.Discrete.functor_map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.CommaMorphism.w`

---

← Back to Index