Documentation Verification Report

Directed

📁 Source: Mathlib/CategoryTheory/Presentable/Directed.lean

Statistics

Metric	Count
Definitions `Diagram`, `ofExistsUnique`, `P`, `iSup`, `single`, `sup`, `DiagramWithUniqueTerminal`, `isTerminal`, `single`, `toDiagram`, `top`, `D₁`, `D₂`, `D₃`, `D₄`, `functor`, `functorMap`, `instPartialOrderDiagramWithUniqueTerminal`	18
Theorems `exists_cardinal_directed`, `comm`, `comm_assoc`, `hlift`, `instSubsingleton`, `lift_self`, `prop`, `prop_id`, `uniq`, `ext`, `ext_iff`, `hP`, `hW`, `iSup_P`, `iSup_W`, `single_P`, `single_W`, `src`, `sup_P`, `sup_W`, `tgt`, `ext`, `ext_iff`, `uniq_terminal`, `D₁_P`, `D₁_W`, `D₂_P`, `D₂_W`, `D₃_P`, `D₃_W`, `D₄_P`, `D₄_W`, `aux`, `eq_id_of_D₂_W`, `final_functor`, `functorMap_comp`, `functorMap_comp_assoc`, `functorMap_id`, `functor_map`, `functor_obj`, `instFiniteSubtypePSingle`, `isCardinalFiltered`, `isCardinalFiltered_aux`, `exists_directed`	44
Total	62

CategoryTheory.IsCardinalFiltered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_cardinal_directed` 📖	mathematical	—	`CategoryTheory.Functor.Final` `Preorder.smallCategory` `PartialOrder.toPreorder`	—	`CategoryTheory.isFiltered_of_isCardinalFiltered` `CategoryTheory.instIsCardinalFilteredToTypeOrd` `exists_cardinal_directed.aux` `CategoryTheory.isCardinalFiltered_prod` `Order.le_succ` `Cardinal.noMaxOrder` `Cardinal.IsRegular.aleph0_le` `Fact.out` `not_isMax` `Order.max_of_succ_le` `CategoryTheory.leOfHom` `CategoryTheory.Functor.final_comp` `CategoryTheory.IsFiltered.final_fst`

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed

Definitions

Name	Category	Theorems
`Diagram` 📖	CompData	—
`DiagramWithUniqueTerminal` 📖	CompData	5 math math: `functorMap_id`, `functor_obj`, `final_functor`, `isCardinalFiltered`, `functor_map`
`D₁` 📖	CompOp	2 math math: `D₁_W`, `D₁_P`
`D₂` 📖	CompOp	2 math math: `D₂_W`, `D₂_P`
`D₃` 📖	CompOp	2 math math: `D₃_P`, `D₃_W`
`D₄` 📖	CompOp	2 math math: `D₄_P`, `D₄_W`
`functor` 📖	CompOp	3 math math: `functor_obj`, `final_functor`, `functor_map`
`functorMap` 📖	CompOp	4 math math: `functorMap_comp`, `functorMap_id`, `functorMap_comp_assoc`, `functor_map`
`instPartialOrderDiagramWithUniqueTerminal` 📖	CompOp	5 math math: `functorMap_id`, `functor_obj`, `final_functor`, `isCardinalFiltered`, `functor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`D₁_P` 📖	mathematical	`HasCardinalLT`	`Diagram.P` `D₁` `DiagramWithUniqueTerminal.toDiagram`	—	—
`D₁_W` 📖	mathematical	`HasCardinalLT`	`Diagram.W` `D₁` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `DiagramWithUniqueTerminal.toDiagram` `CategoryTheory.MorphismProperty.ofHoms` `CategoryTheory.CategoryStruct.id`	—	—
`D₂_P` 📖	mathematical	`HasCardinalLT`	`Diagram.P` `D₂` `DiagramWithUniqueTerminal.toDiagram`	—	`D₁_P`
`D₂_W` 📖	mathematical	`HasCardinalLT`	`Diagram.W` `D₂` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `DiagramWithUniqueTerminal.toDiagram` `CategoryTheory.MorphismProperty.ofHoms` `CategoryTheory.CategoryStruct.id` `Diagram.P` `CategoryTheory.CategoryStruct.comp` `DiagramWithUniqueTerminal.top` `Diagram.IsTerminal.lift` `DiagramWithUniqueTerminal.isTerminal`	—	—
`D₃_P` 📖	mathematical	—	`Diagram.P` `D₃` `DiagramWithUniqueTerminal.toDiagram`	—	—
`D₃_W` 📖	mathematical	—	`Diagram.W` `D₃` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `DiagramWithUniqueTerminal.toDiagram` `CategoryTheory.MorphismProperty.ofHoms` `CategoryTheory.CategoryStruct.id`	—	—
`D₄_P` 📖	mathematical	—	`Diagram.P` `D₄` `DiagramWithUniqueTerminal.toDiagram`	—	`D₃_P`
`D₄_W` 📖	mathematical	—	`Diagram.W` `D₄` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `DiagramWithUniqueTerminal.toDiagram` `CategoryTheory.MorphismProperty.ofHoms` `CategoryTheory.CategoryStruct.id` `Diagram.P`	—	—
`aux` 📖	mathematical	`IsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.Final` `Preorder.smallCategory` `PartialOrder.toPreorder`	—	`isCardinalFiltered` `final_functor`
`eq_id_of_D₂_W` 📖	mathematical	`HasCardinalLT` `Diagram.P` `DiagramWithUniqueTerminal.toDiagram` `Diagram.W` `D₂`	`CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Diagram.src` `CategoryTheory.MorphismProperty.ofHoms_iff`
`final_functor` 📖	mathematical	`IsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.Final` `DiagramWithUniqueTerminal` `Preorder.smallCategory` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal` `functor`	—	`isCardinalFiltered` `CategoryTheory.isFiltered_of_isCardinalFiltered` `CategoryTheory.Functor.final_iff_of_isFiltered` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `CategoryTheory.Category.assoc` `CategoryTheory.IsFiltered.coeq_condition` `IsEmpty.false` `Diagram.tgt` `Diagram.src` `CategoryTheory.MorphismProperty.ofHoms_iff` `Diagram.IsTerminal.comm_assoc` `CategoryTheory.Category.comp_id` `Diagram.IsTerminal.uniq` `Diagram.IsTerminal.prop` `LE.le.trans` `le_sup_left` `Diagram.IsTerminal.lift_self` `CategoryTheory.Category.id_comp`
`functorMap_comp` 📖	mathematical	`DiagramWithUniqueTerminal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `DiagramWithUniqueTerminal.top` `functorMap` `LE.le.trans`	—	`Diagram.IsTerminal.comm` `Diagram.IsTerminal.hlift`
`functorMap_comp_assoc` 📖	mathematical	`DiagramWithUniqueTerminal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `DiagramWithUniqueTerminal.top` `functorMap` `LE.le.trans`	—	`LE.le.trans` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `functorMap_comp`
`functorMap_id` 📖	mathematical	—	`functorMap` `le_refl` `DiagramWithUniqueTerminal` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `DiagramWithUniqueTerminal.top`	—	`le_refl` `Diagram.IsTerminal.lift_self`
`functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `DiagramWithUniqueTerminal` `Preorder.smallCategory` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal` `functor` `functorMap`	—	—
`functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `DiagramWithUniqueTerminal` `Preorder.smallCategory` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal` `functor` `DiagramWithUniqueTerminal.top`	—	—
`instFiniteSubtypePSingle` 📖	mathematical	—	`Finite` `Diagram.P` `Diagram.single`	—	`Finite.of_surjective` `Finite.of_fintype`
`isCardinalFiltered` 📖	mathematical	`IsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.IsCardinalFiltered` `DiagramWithUniqueTerminal` `Preorder.smallCategory` `PartialOrder.toPreorder` `instPartialOrderDiagramWithUniqueTerminal`	—	`CategoryTheory.isCardinalFiltered_preorder` `isCardinalFiltered_aux` `hasCardinalLT_iff_cardinal_mk_lt` `IsEmpty.false` `Diagram.tgt` `D₂_P` `eq_id_of_D₂_W` `Diagram.src` `Diagram.IsTerminal.comm_assoc` `CategoryTheory.Category.comp_id` `Diagram.IsTerminal.prop` `le_trans` `le_refl` `le_iSup` `le_sup_left`
`isCardinalFiltered_aux` 📖	mathematical	`IsEmpty` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasCardinalLT`	`DiagramWithUniqueTerminal.top` `CategoryTheory.CategoryStruct.comp` `Diagram.IsTerminal.lift` `DiagramWithUniqueTerminal.toDiagram` `DiagramWithUniqueTerminal.isTerminal`	—	`Cardinal.IsRegular.aleph0_le` `Fact.out` `hasCardinalLT_prod` `hasCardinalLT_sigma` `Diagram.hP` `HasCardinalLT.of_injective` `hasCardinalLT_of_finite` `Finite.of_fintype` `hasCardinalLT_iff_of_equiv` `hasCardinalLT_sum_iff` `IsEmpty.false` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.Multicofork.condition`

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram

Definitions

Name	Category	Theorems
`P` 📖	CompOp	16 math math: `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.ext_iff`, `hP`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_P`, `src`, `ext_iff`, `tgt`, `IsTerminal.prop`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instFiniteSubtypePSingle`, `single_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W`, `iSup_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_P`, `sup_P`
`iSup` 📖	CompOp	2 math math: `iSup_W`, `iSup_P`
`single` 📖	CompOp	3 math math: `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instFiniteSubtypePSingle`, `single_P`, `single_W`
`sup` 📖	CompOp	2 math math: `sup_W`, `sup_P`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`W` `P`	—	—	—
`ext_iff` 📖	mathematical	—	`W` `P`	—	`ext`
`hP` 📖	mathematical	—	`CategoryTheory.ObjectProperty.HasCardinalLT` `P`	—	—
`hW` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasCardinalLT` `W`	—	—
`iSup_P` 📖	mathematical	`HasCardinalLT`	`P` `iSup` `iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	—
`iSup_W` 📖	mathematical	`HasCardinalLT`	`W` `iSup` `iSup` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`single_P` 📖	mathematical	—	`P` `single` `CategoryTheory.ObjectProperty.ofObj` `CategoryTheory.Category.toCategoryStruct`	—	—
`single_W` 📖	mathematical	—	`W` `single` `CategoryTheory.MorphismProperty.ofHoms` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`src` 📖	mathematical	`W`	`P`	—	—
`sup_P` 📖	mathematical	—	`P` `sup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	—
`sup_W` 📖	mathematical	—	`W` `sup` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`tgt` 📖	mathematical	`W`	`P`	—	—

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal

Definitions

Name	Category	Theorems
`ofExistsUnique` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src`	—	—
`comm_assoc` 📖	mathematical	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src`	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`hlift` 📖	mathematical	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P`	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W` `lift`	—	—
`instSubsingleton` 📖	mathematical	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal`	—	`uniq` `hlift` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src`
`lift_self` 📖	mathematical	—	`lift` `prop` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`uniq` `prop` `prop_id`
`prop` 📖	mathematical	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P`	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src` `prop_id`
`prop_id` 📖	mathematical	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`uniq` 📖	mathematical	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W`	`lift`	—	—

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal

Definitions

Name	Category	Theorems
`isTerminal` 📖	CompOp	2 math math: `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W`
`single` 📖	CompOp	—
`toDiagram` 📖	CompOp	10 math math: `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W`, `ext_iff`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_P`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_P`
`top` 📖	CompOp	7 math math: `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_comp`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_id`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_obj`, `uniq_terminal`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_comp_assoc`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W` `toDiagram` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P`	—	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.instSubsingleton` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.ext` `CategoryTheory.MorphismProperty.ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W` `toDiagram` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P`	—	`ext`
`uniq_terminal` 📖	mathematical	—	`top`	—	—

CategoryTheory.IsFiltered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_directed` 📖	mathematical	—	`CategoryTheory.Functor.Final` `Preorder.smallCategory` `PartialOrder.toPreorder`	—	`Cardinal.fact_isRegular_aleph0` `CategoryTheory.isCardinalFiltered_aleph0_iff` `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed` `isDirectedOrder` `nonempty`

---

← Back to Index