Documentation Verification Report

Adjunctions

📁 Source: Mathlib/Algebra/Category/MonCat/Adjunctions.lean

Statistics

Metric	Count
Definitions `adj`, `free`, `adj`, `adjoinZero`, `adjoinZeroAdj`, `free`, `hasForgetToAddSemigroup`, `adj`, `adjoinOne`, `adjoinOneAdj`, `free`, `hasForgetToSemigroup`	12
Theorems `free_map`, `free_obj_coe`, `instIsLeftAdjointFree`, `instIsRightAdjointForgetAddMonoidHomCarrier`, `adjoinZero_map`, `adjoinZero_obj_coe`, `instIsRightAdjointForgetMonoidHomCarrier`, `adjoinOne_map`, `adjoinOne_obj_coe`, `instIsRightAdjointForgetMonoidHomCarrier`	10
Total	22

AddCommMonCat

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`free` 📖	CompOp	3 math math: `free_obj_coe`, `free_map`, `instIsLeftAdjointFree`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`free_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.types` `AddCommMonCat` `instCategory` `free` `ofHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Finsupp.mapDomain.addMonoidHom`	—	—
`free_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `CategoryTheory.types` `AddCommMonCat` `instCategory` `free` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	—
`instIsLeftAdjointFree` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `CategoryTheory.types` `AddCommMonCat` `instCategory` `free`	—	—
`instIsRightAdjointForgetAddMonoidHomCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `AddCommMonCat` `instCategory` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	—

AddMonCat

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`adjoinZero` 📖	CompOp	2 math math: `adjoinZero_obj_coe`, `adjoinZero_map`
`adjoinZeroAdj` 📖	CompOp	—
`free` 📖	CompOp	—
`hasForgetToAddSemigroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoinZero_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddSemigrp` `AddSemigrp.instCategory` `AddMonCat` `instCategory` `adjoinZero` `ofHom` `WithZero` `AddSemigrp.carrier` `WithZero.instAddMonoid` `AddSemigrp.str` `WithZero.mapAddHom` `AddSemigroup.toAdd` `AddSemigrp.Hom.hom`	—	—
`adjoinZero_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `AddSemigrp` `AddSemigrp.instCategory` `AddMonCat` `instCategory` `adjoinZero` `WithZero` `AddSemigrp.carrier`	—	—

CommMonCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRightAdjointForgetMonoidHomCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `CommMonCat` `instCategory` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	—

MonCat

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`adjoinOne` 📖	CompOp	2 math math: `adjoinOne_obj_coe`, `adjoinOne_map`
`adjoinOneAdj` 📖	CompOp	—
`free` 📖	CompOp	—
`hasForgetToSemigroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoinOne_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Semigrp` `Semigrp.instCategory` `MonCat` `instCategory` `adjoinOne` `ofHom` `WithOne` `Semigrp.carrier` `WithOne.instMonoid` `Semigrp.str` `WithOne.mapMulHom` `Semigroup.toMul` `Semigrp.Hom.hom`	—	—
`adjoinOne_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `Semigrp` `Semigrp.instCategory` `MonCat` `instCategory` `adjoinOne` `WithOne` `Semigrp.carrier`	—	—
`instIsRightAdjointForgetMonoidHomCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `MonCat` `instCategory` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	—

---

← Back to Index