Documentation Verification Report

ConcreteCategory

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

Statistics

Metric	Count
Definitions `ConcreteCategory`, `instUniqueToTypeTerminal`, `multiequalizerEquiv`, `multiequalizerEquivAux`, `prodEquiv`, `productEquiv`, `pullbackEquiv`, `pullbackMk`, `terminalEquiv`, `terminalIffUnique`, `terminalOfUniqueOfReflects`, `uniqueOfTerminalOfPreserves`	12
Theorems `map_ext`, `cokernel_funext`, `empty_of_initial_of_preserves`, `initial_iff_empty_of_preserves_of_reflects`, `initial_of_empty_of_reflects`, `multiequalizerEquiv_apply`, `multiequalizer_ext`, `prodEquiv_apply_fst`, `prodEquiv_apply_snd`, `prodEquiv_symm_apply_fst`, `prodEquiv_symm_apply_snd`, `productEquiv_apply_apply`, `productEquiv_symm_apply_π`, `pullbackMk_fst`, `pullbackMk_snd`, `pullbackMk_surjective`, `widePullback_ext`, `widePullback_ext'`, `widePushout_exists_rep`, `widePushout_exists_rep'`	20
Total	32

CategoryTheory

Definitions

Name	Category	Theorems
`ConcreteCategory` 📖	CompData	—

CategoryTheory.Limits.Concrete

Definitions

Name	Category	Theorems
`instUniqueToTypeTerminal` 📖	CompOp	—
`multiequalizerEquiv` 📖	CompOp	1 math math: `multiequalizerEquiv_apply`
`multiequalizerEquivAux` 📖	CompOp	—
`prodEquiv` 📖	CompOp	4 math math: `prodEquiv_apply_fst`, `prodEquiv_symm_apply_snd`, `prodEquiv_symm_apply_fst`, `prodEquiv_apply_snd`
`productEquiv` 📖	CompOp	2 math math: `productEquiv_symm_apply_π`, `productEquiv_apply_apply`
`pullbackEquiv` 📖	CompOp	—
`pullbackMk` 📖	CompOp	3 math math: `pullbackMk_snd`, `pullbackMk_fst`, `pullbackMk_surjective`
`terminalEquiv` 📖	CompOp	—
`terminalIffUnique` 📖	CompOp	—
`terminalOfUniqueOfReflects` 📖	CompOp	—
`uniqueOfTerminalOfPreserves` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cokernel_funext` 📖	—	`DFunLike.coe` `CategoryTheory.Limits.cokernel` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.cokernel.π`	—	—	`CategoryTheory.Limits.coequalizer.hom_ext` `CategoryTheory.ConcreteCategory.hom_ext` `CategoryTheory.comp_apply`
`empty_of_initial_of_preserves` 📖	mathematical	—	`IsEmpty` `CategoryTheory.ToType`	—	`CategoryTheory.Limits.Types.initial_iff_empty` `Nonempty.map`
`initial_iff_empty_of_preserves_of_reflects` 📖	mathematical	—	`CategoryTheory.Limits.IsInitial` `IsEmpty` `CategoryTheory.ToType`	—	`CategoryTheory.Limits.Types.initial_iff_empty` `Equiv.nonempty_congr`
`initial_of_empty_of_reflects` 📖	mathematical	—	`CategoryTheory.Limits.IsInitial`	—	`Nonempty.map` `CategoryTheory.Limits.Types.initial_iff_empty`
`multiequalizerEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.ToType` `CategoryTheory.Limits.multiequalizer` `EquivLike.toFunLike` `Equiv.instEquivLike` `multiequalizerEquiv` `CategoryTheory.Limits.MulticospanIndex.left` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.Multiequalizer.ι`	—	—
`multiequalizer_ext` 📖	—	`DFunLike.coe` `CategoryTheory.Limits.multiequalizer` `CategoryTheory.Limits.MulticospanIndex.left` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.Multiequalizer.ι`	—	—	`limit_ext` `CategoryTheory.Limits.limit.w` `CategoryTheory.ConcreteCategory.comp_apply`
`prodEquiv_apply_fst` 📖	mathematical	—	`CategoryTheory.ToType` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.prod` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.prod.fst`	—	`CategoryTheory.Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair` `CategoryTheory.Limits.prodComparison_fst`
`prodEquiv_apply_snd` 📖	mathematical	—	`CategoryTheory.ToType` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.prod` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.prod.snd`	—	`CategoryTheory.Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair` `CategoryTheory.Limits.prodComparison_snd`
`prodEquiv_symm_apply_fst` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Limits.prod` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.prod.fst` `Equiv` `CategoryTheory.ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodEquiv`	—	`Equiv.surjective` `Equiv.symm_apply_apply` `prodEquiv_apply_fst`
`prodEquiv_symm_apply_snd` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Limits.prod` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.prod.snd` `Equiv` `CategoryTheory.ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodEquiv`	—	`Equiv.surjective` `Equiv.symm_apply_apply` `prodEquiv_apply_snd`
`productEquiv_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.ToType` `CategoryTheory.Limits.piObj` `EquivLike.toFunLike` `Equiv.instEquivLike` `productEquiv` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.Pi.π`	—	`CategoryTheory.Limits.Types.hasLimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.piComparison_comp_π`
`productEquiv_symm_apply_π` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Limits.piObj` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.Pi.π` `Equiv` `CategoryTheory.ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `productEquiv`	—	`productEquiv_apply_apply` `Equiv.apply_symm_apply`
`pullbackMk_fst` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.fst` `pullbackMk`	—	`CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.PreservesPullback.iso_inv_fst` `CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst`
`pullbackMk_snd` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.snd` `pullbackMk`	—	`CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.PreservesPullback.iso_inv_snd` `CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd`
`pullbackMk_surjective` 📖	mathematical	—	`pullbackMk`	—	`Equiv.surjective`
`widePullback_ext` 📖	—	`DFunLike.coe` `CategoryTheory.Limits.widePullback` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.WidePullback.base` `CategoryTheory.Limits.WidePullback.π`	—	—	`limit_ext`
`widePullback_ext'` 📖	—	`DFunLike.coe` `CategoryTheory.Limits.widePullback` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.WidePullback.π`	—	—	`widePullback_ext` `CategoryTheory.Limits.WidePullback.π_arrow` `CategoryTheory.ConcreteCategory.comp_apply`
`widePushout_exists_rep` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Limits.widePushout` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.WidePushout.head` `CategoryTheory.Limits.WidePushout.ι`	—	`colimit_exists_rep`
`widePushout_exists_rep'` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Limits.widePushout` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Limits.WidePushout.ι`	—	`widePushout_exists_rep` `CategoryTheory.Limits.WidePushout.arrow_ι` `CategoryTheory.ConcreteCategory.comp_apply`

CategoryTheory.Limits.Concrete.Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_ext` 📖	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.piObj` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Pi.π`	—	—	`CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.Concrete.limit_ext` `CategoryTheory.ConcreteCategory.comp_apply` `CategoryTheory.Limits.piComparison_comp_π`

---

← Back to Index