Documentation Verification Report

CodiscreteCategory

📁 Source: Mathlib/CategoryTheory/CodiscreteCategory.lean

Statistics

Metric	Count
Definitions `Codiscrete`, `adj`, `as`, `counitApp`, `equivFunctorToCodiscrete`, `functor`, `functorOfFun`, `functorToCat`, `instCategory`, `invFunctor`, `natIso`, `natIsoFunctor`, `natTrans`, `oppositeEquivalence`, `unitApp`, `codiscreteEquiv`, `instDecidableEqCodiscrete`	17
Theorems `adj_counit_app`, `adj_unit_app`, `ext`, `ext_iff`, `left_triangle_components`, `mk_as`, `natIsoFunctor_hom_app`, `natIsoFunctor_inv_app`, `right_triangle_components`, `codiscreteEquiv_apply`, `codiscreteEquiv_symm_apply_as`	11
Total	28

CategoryTheory

Definitions

Name	Category	Theorems
`Codiscrete` 📖	CompData	7 math math: `Codiscrete.left_triangle_components`, `Codiscrete.natIsoFunctor_hom_app`, `Codiscrete.right_triangle_components`, `Codiscrete.natIsoFunctor_inv_app`, `codiscreteEquiv_apply`, `codiscreteEquiv_symm_apply_as`, `Codiscrete.adj_unit_app`
`codiscreteEquiv` 📖	CompOp	2 math math: `codiscreteEquiv_apply`, `codiscreteEquiv_symm_apply_as`
`instDecidableEqCodiscrete` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codiscreteEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Codiscrete` `EquivLike.toFunLike` `Equiv.instEquivLike` `codiscreteEquiv` `Codiscrete.as`	—	—
`codiscreteEquiv_symm_apply_as` 📖	mathematical	—	`Codiscrete.as` `DFunLike.coe` `Equiv` `Codiscrete` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `codiscreteEquiv`	—	—

CategoryTheory.Codiscrete

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	2 math math: `adj_counit_app`, `adj_unit_app`
`as` 📖	CompOp	6 math math: `natIsoFunctor_hom_app`, `mk_as`, `natIsoFunctor_inv_app`, `CategoryTheory.codiscreteEquiv_apply`, `CategoryTheory.codiscreteEquiv_symm_apply_as`, `ext_iff`
`counitApp` 📖	CompOp	3 math math: `left_triangle_components`, `right_triangle_components`, `adj_counit_app`
`equivFunctorToCodiscrete` 📖	CompOp	—
`functor` 📖	CompOp	2 math math: `natIsoFunctor_hom_app`, `natIsoFunctor_inv_app`
`functorOfFun` 📖	CompOp	1 math math: `right_triangle_components`
`functorToCat` 📖	CompOp	2 math math: `adj_counit_app`, `adj_unit_app`
`instCategory` 📖	CompOp	5 math math: `left_triangle_components`, `natIsoFunctor_hom_app`, `right_triangle_components`, `natIsoFunctor_inv_app`, `adj_unit_app`
`invFunctor` 📖	CompOp	—
`natIso` 📖	CompOp	—
`natIsoFunctor` 📖	CompOp	2 math math: `natIsoFunctor_hom_app`, `natIsoFunctor_inv_app`
`natTrans` 📖	CompOp	—
`oppositeEquivalence` 📖	CompOp	—
`unitApp` 📖	CompOp	3 math math: `left_triangle_components`, `right_triangle_components`, `adj_unit_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_counit_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `functorToCat` `CategoryTheory.Cat.objects` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `adj` `counitApp`	—	—
`adj_unit_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.Cat.objects` `functorToCat` `CategoryTheory.Adjunction.unit` `adj` `CategoryTheory.Functor.toCatHom` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Codiscrete` `CategoryTheory.Cat.str` `instCategory` `unitApp`	—	—
`ext` 📖	—	`as`	—	—	—
`ext_iff` 📖	mathematical	—	`as`	—	`ext`
`left_triangle_components` 📖	mathematical	—	`CategoryTheory.Codiscrete` `counitApp` `CategoryTheory.Functor.obj` `instCategory` `unitApp`	—	—
`mk_as` 📖	mathematical	—	`as`	—	—
`natIsoFunctor_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Codiscrete` `instCategory` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functor` `as` `CategoryTheory.Functor.obj` `natIsoFunctor` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`natIsoFunctor_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Codiscrete` `instCategory` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functor` `as` `CategoryTheory.Functor.obj` `natIsoFunctor` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`right_triangle_components` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.Codiscrete` `instCategory` `unitApp` `functorOfFun` `counitApp` `CategoryTheory.Functor.id`	—	—

---

← Back to Index