EqualizerProducts

📁 Source: Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean

Statistics

Metric	Count
Definitions IsSheafEqualizerProducts, diagram, isoOfIso, fork, isoOfIso, leftRes, piInters, isoOfIso, piOpens, isoOfIso, res, rightRes, coneEquiv, coneEquivCounitIso, coneEquivFunctor, coneEquivFunctorObj, coneEquivInverse, coneEquivInverseObj, coneEquivUnitIso, coneEquivUnitIsoApp, isLimitMapConeOfIsLimitSheafConditionFork, isLimitSheafConditionForkOfIsLimitMapCone	22
Theorems fork_pt, fork_ι, fork_π_app_walkingParallelPair_one, fork_π_app_walkingParallelPair_zero, hom_ext, hom_ext_iff, hom_ext, hom_ext_iff, res_π, res_π_apply, w, w_apply, coneEquivCounitIso_hom_app_hom, coneEquivCounitIso_inv_app_hom, coneEquivFunctorObj_pt, coneEquivFunctorObj_π_app, coneEquivFunctor_map_hom, coneEquivFunctor_obj_pt, coneEquivFunctor_obj_π_app, coneEquivInverseObj_pt, coneEquivInverseObj_π_app, coneEquivInverse_map_hom, coneEquivInverse_obj_pt, coneEquivInverse_obj_π_app, coneEquivUnitIsoApp_hom_hom, coneEquivUnitIsoApp_inv_hom, coneEquivUnitIso_hom_app_hom, coneEquivUnitIso_inv_app_hom, coneEquiv_counitIso, coneEquiv_functor, coneEquiv_inverse, coneEquiv_unitIso, isSheaf_iff_isSheafEqualizerProducts	33
Total	55

TopCat.Presheaf

Definitions

Name	Category	Theorems
IsSheafEqualizerProducts 📖	MathDef	1 math math: isSheaf_iff_isSheafEqualizerProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff_isSheafEqualizerProducts 📖	mathematical	CategoryTheory.Limits.HasProducts	IsSheaf IsSheafEqualizerProducts	—	isSheaf_iff_isSheafPairwiseIntersections

TopCat.Presheaf.SheafConditionEqualizerProducts

Definitions

Name	Category	Theorems
diagram 📖	CompOp	20 math math: 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, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, 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.SheafConditionPairwiseIntersections.coneEquiv_functor, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt
fork 📖	CompOp	4 math math: fork_π_app_walkingParallelPair_one, fork_ι, fork_pt, fork_π_app_walkingParallelPair_zero
leftRes 📖	CompOp	7 math math: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, fork_π_app_walkingParallelPair_one, fork_ι, w, fork_pt, w_apply, fork_π_app_walkingParallelPair_zero
piInters 📖	CompOp	8 math math: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, fork_π_app_walkingParallelPair_one, fork_ι, w, piInters.hom_ext_iff, fork_pt, w_apply, fork_π_app_walkingParallelPair_zero
piOpens 📖	CompOp	10 math math: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, piOpens.hom_ext_iff, fork_π_app_walkingParallelPair_one, fork_ι, w, res_π, fork_pt, w_apply, fork_π_app_walkingParallelPair_zero, res_π_apply
res 📖	CompOp	7 math math: fork_π_app_walkingParallelPair_one, fork_ι, w, res_π, w_apply, fork_π_app_walkingParallelPair_zero, res_π_apply
rightRes 📖	CompOp	7 math math: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, fork_π_app_walkingParallelPair_one, fork_ι, w, fork_pt, w_apply, fork_π_app_walkingParallelPair_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fork_pt 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair piOpens piInters leftRes rightRes fork CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	—	—
fork_ι 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.Fork.ι piOpens piInters leftRes rightRes fork res	—	—
fork_π_app_walkingParallelPair_one 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair piOpens piInters leftRes rightRes fork CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice res	—	—
fork_π_app_walkingParallelPair_zero 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair piOpens piInters leftRes rightRes fork CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.zero res	—	—
res_π 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice piOpens CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor res CategoryTheory.Limits.limit.π CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver TopologicalSpace.Opens.leSupr	—	res.eq_1 CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.Fan.mk_π_app
res_π_apply 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe piOpens CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.limit.π CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice res CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopologicalSpace.Opens.leSupr	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise res_π
w 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice piOpens piInters res leftRes rightRes	—	piInters.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Functor.map_comp
w_apply 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe piOpens piInters CategoryTheory.ConcreteCategory.hom leftRes CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice res rightRes	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise w

TopCat.Presheaf.SheafConditionEqualizerProducts.diagram

Definitions

Name	Category	Theorems
isoOfIso 📖	CompOp	—

TopCat.Presheaf.SheafConditionEqualizerProducts.fork

Definitions

Name	Category	Theorems
isoOfIso 📖	CompOp	—

TopCat.Presheaf.SheafConditionEqualizerProducts.piInters

Definitions

Name	Category	Theorems
isoOfIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.Limits.HasProducts CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.SheafConditionEqualizerProducts.piInters CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Limits.limit.π	—	—	CategoryTheory.Limits.limit.hom_ext
hom_ext_iff 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.SheafConditionEqualizerProducts.piInters CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Limits.limit.π	—	hom_ext

TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens

Definitions

Name	Category	Theorems
isoOfIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.Limits.HasProducts CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.Limits.limit.π	—	—	CategoryTheory.Limits.limit.hom_ext
hom_ext_iff 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.Limits.limit.π	—	hom_ext

TopCat.Presheaf.SheafConditionPairwiseIntersections

Definitions

Name	Category	Theorems
coneEquiv 📖	CompOp	4 math math: coneEquiv_counitIso, coneEquiv_inverse, coneEquiv_functor, coneEquiv_unitIso
coneEquivCounitIso 📖	CompOp	3 math math: coneEquivCounitIso_hom_app_hom, coneEquiv_counitIso, coneEquivCounitIso_inv_app_hom
coneEquivFunctor 📖	CompOp	10 math math: coneEquivCounitIso_hom_app_hom, coneEquivCounitIso_inv_app_hom, coneEquivFunctor_obj_pt, coneEquivUnitIso_inv_app_hom, coneEquivFunctor_obj_π_app, coneEquivFunctor_map_hom, coneEquivUnitIso_hom_app_hom, coneEquivUnitIsoApp_hom_hom, coneEquivUnitIsoApp_inv_hom, coneEquiv_functor
coneEquivFunctorObj 📖	CompOp	3 math math: coneEquivFunctorObj_π_app, coneEquivFunctor_map_hom, coneEquivFunctorObj_pt
coneEquivInverse 📖	CompOp	10 math math: coneEquivInverse_obj_π_app, coneEquivCounitIso_hom_app_hom, coneEquivCounitIso_inv_app_hom, coneEquiv_inverse, coneEquivUnitIso_inv_app_hom, coneEquivInverse_obj_pt, coneEquivUnitIso_hom_app_hom, coneEquivUnitIsoApp_hom_hom, coneEquivInverse_map_hom, coneEquivUnitIsoApp_inv_hom
coneEquivInverseObj 📖	CompOp	3 math math: coneEquivInverseObj_π_app, coneEquivInverse_map_hom, coneEquivInverseObj_pt
coneEquivUnitIso 📖	CompOp	3 math math: coneEquivUnitIso_inv_app_hom, coneEquivUnitIso_hom_app_hom, coneEquiv_unitIso
coneEquivUnitIsoApp 📖	CompOp	2 math math: coneEquivUnitIsoApp_hom_hom, coneEquivUnitIsoApp_inv_hom
isLimitMapConeOfIsLimitSheafConditionFork 📖	CompOp	—
isLimitSheafConditionForkOfIsLimitMapCone 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneEquivCounitIso_hom_app_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.comp Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram coneEquivInverse coneEquivFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category coneEquivCounitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquivCounitIso_inv_app_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram coneEquivInverse coneEquivFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category coneEquivCounitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquivFunctorObj_pt 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram coneEquivFunctorObj Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram	—	—
coneEquivFunctorObj_π_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.π coneEquivFunctorObj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Pi.lift TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Pairwise.single SemilatticeInf.toMin CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Pairwise.pair	—	—
coneEquivFunctor_map_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram coneEquivFunctorObj CategoryTheory.Functor.map CategoryTheory.Limits.Cone Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.Cone.category coneEquivFunctor	—	—
coneEquivFunctor_obj_pt 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.Cone.category coneEquivFunctor	—	—
coneEquivFunctor_obj_π_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category coneEquivFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Pi.lift TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.Pairwise.single SemilatticeInf.toMin CategoryTheory.Pairwise.pair	—	—
coneEquivInverseObj_pt 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram coneEquivInverseObj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram	—	—
coneEquivInverseObj_π_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.Cone.π coneEquivInverseObj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.CategoryStruct.comp CategoryTheory.Pairwise.single CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Pi.π TopologicalSpace.Opens.instPartialOrder CategoryTheory.Pairwise.pair CategoryTheory.Limits.WalkingParallelPair.one SemilatticeInf.toMin	—	—
coneEquivInverse_map_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram coneEquivInverseObj CategoryTheory.Functor.map CategoryTheory.Limits.Cone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.category coneEquivInverse	—	—
coneEquivInverse_obj_pt 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.category coneEquivInverse	—	—
coneEquivInverse_obj_π_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category coneEquivInverse Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op SemilatticeInf.toMin CategoryTheory.CategoryStruct.comp TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens CategoryTheory.Limits.Fork.ι TopCat.Presheaf.SheafConditionEqualizerProducts.piInters TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes CategoryTheory.Limits.Pi.π TopologicalSpace.Opens.instPartialOrder Opposite.unop	—	CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left CategoryTheory.Category.assoc
coneEquivUnitIsoApp_hom_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.id CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram coneEquivFunctor coneEquivInverse CategoryTheory.Iso.hom coneEquivUnitIsoApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquivUnitIsoApp_inv_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram coneEquivFunctor coneEquivInverse CategoryTheory.Functor.id CategoryTheory.Iso.inv coneEquivUnitIsoApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquivUnitIso_hom_app_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.id CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram coneEquivFunctor coneEquivInverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category coneEquivUnitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquivUnitIso_inv_app_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.ConeMorphism.hom Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram coneEquivFunctor coneEquivInverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category coneEquivUnitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquiv_counitIso 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Equivalence.counitIso CategoryTheory.Limits.Cone Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.category coneEquiv coneEquivCounitIso	—	—
coneEquiv_functor 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cone Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.category coneEquiv coneEquivFunctor	—	—
coneEquiv_inverse 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Equivalence.inverse CategoryTheory.Limits.Cone Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.category coneEquiv coneEquivInverse	—	—
coneEquiv_unitIso 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Equivalence.unitIso CategoryTheory.Limits.Cone Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.op CategoryTheory.Pairwise.diagram CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat.Presheaf.SheafConditionEqualizerProducts.diagram CategoryTheory.Limits.Cone.category coneEquiv coneEquivUnitIso	—	—

---

← Back to Index