Documentation Verification Report

Pairwise

📁 Source: Mathlib/CategoryTheory/Category/Pairwise.lean

Statistics

Metric	Count
Definitions `Pairwise`, `cocone`, `coconeIsColimit`, `coconeιApp`, `comp`, `diagram`, `diagramMap`, `diagramObj`, `homInhabited`, `id`, `instCategory`, `instCategoryStruct`, `instDecidableEqHom`, `decEq`, `instDecidableEqHom_1`, `instFinCategoryOfFintypeOfDecidableEq`, `pairwiseCases`, `pairwiseInhabited`, `instDecidableEqPairwise`, `decEq`, `instFintypePairwise`	21
Theorems `cocone_pt`, `cocone_ι_app`, `diagram_map`, `diagram_obj`	4
Total	25

CategoryTheory

Definitions

Name	Category	Theorems
`Pairwise` 📖	CompData	31 math math: `Pairwise.diagram_obj`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app`, `TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_map`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom`, `Pairwise.cocone_pt`, `TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_obj`, `Pairwise.diagram_map`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt`, `TopCat.Presheaf.SheafCondition.instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse`, `Pairwise.cocone_ι_app`, `TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom`, `TopCat.Presheaf.SheafCondition.instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom`, `TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections`, `TopCat.Presheaf.isGluing_iff_pairwise`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt`
`instDecidableEqPairwise` 📖	CompOp	—
`instFintypePairwise` 📖	CompOp	—

CategoryTheory.Pairwise

Definitions

Name	Category	Theorems
`cocone` 📖	CompOp	4 math math: `cocone_pt`, `cocone_ι_app`, `TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections`, `TopCat.Presheaf.isGluing_iff_pairwise`
`coconeIsColimit` 📖	CompOp	—
`coconeιApp` 📖	CompOp	1 math math: `cocone_ι_app`
`comp` 📖	CompOp	—
`diagram` 📖	CompOp	27 math math: `diagram_obj`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom`, `cocone_pt`, `diagram_map`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse`, `cocone_ι_app`, `TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom`, `TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections`, `TopCat.Presheaf.isGluing_iff_pairwise`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt`
`diagramMap` 📖	CompOp	1 math math: `diagram_map`
`diagramObj` 📖	CompOp	1 math math: `diagram_obj`
`homInhabited` 📖	CompOp	—
`id` 📖	CompOp	—
`instCategory` 📖	CompOp	31 math math: `diagram_obj`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app`, `TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_map`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom`, `cocone_pt`, `TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_obj`, `diagram_map`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt`, `TopCat.Presheaf.SheafCondition.instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse`, `cocone_ι_app`, `TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom`, `TopCat.Presheaf.SheafCondition.instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom`, `TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections`, `TopCat.Presheaf.isGluing_iff_pairwise`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso`, `TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt`
`instCategoryStruct` 📖	CompOp	—
`instDecidableEqHom` 📖	CompOp	—
`instDecidableEqHom_1` 📖	CompOp	—
`instFinCategoryOfFintypeOfDecidableEq` 📖	CompOp	—
`pairwiseCases` 📖	CompOp	—
`pairwiseInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Pairwise` `instCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `diagram` `cocone` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	—
`cocone_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Pairwise` `instCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `diagram` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.Limits.Cocone.ι` `cocone` `coconeιApp`	—	—
`diagram_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Pairwise` `instCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `diagram` `diagramMap`	—	—
`diagram_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Pairwise` `instCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `diagram` `diagramObj`	—	—

CategoryTheory.Pairwise.instDecidableEqHom

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

CategoryTheory.instDecidableEqPairwise

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index