Documentation Verification Report

Adjunctions

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

Statistics

Metric	Count
Definitions `adj`, `coyoneda`, `coyonedaAdj`, `coyonedaUnique`, `forget₂Adj`, `free`, `monoidAlgebra`, `monoidAlgebraAdj`	8
Theorems `coyonedaUnique_hom_app_hom_apply`, `coyonedaUnique_inv_app_hom_apply`, `coyoneda_map_app`, `coyoneda_obj_map`, `coyoneda_obj_obj_carrier`, `free_map_coe`, `free_obj_coe`, `instIsLeftAdjointCommMonCatUnderMonoidAlgebra`, `instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier`, `instIsRightAdjointForgetRingHomCarrier`, `instIsRightAdjointOppositeObjFunctorTypeYoneda`, `monoidAlgebra_map`, `monoidAlgebra_obj`	13
Total	21

CommRingCat

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`coyoneda` 📖	CompOp	5 math math: `coyoneda_map_app`, `coyoneda_obj_obj_carrier`, `coyoneda_obj_map`, `coyonedaUnique_inv_app_hom_apply`, `coyonedaUnique_hom_app_hom_apply`
`coyonedaAdj` 📖	CompOp	—
`coyonedaUnique` 📖	CompOp	2 math math: `coyonedaUnique_inv_app_hom_apply`, `coyonedaUnique_hom_app_hom_apply`
`forget₂Adj` 📖	CompOp	—
`free` 📖	CompOp	2 math math: `free_obj_coe`, `free_map_coe`
`monoidAlgebra` 📖	CompOp	3 math math: `monoidAlgebra_map`, `instIsLeftAdjointCommMonCatUnderMonoidAlgebra`, `monoidAlgebra_obj`
`monoidAlgebraAdj` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coyonedaUnique_hom_app_hom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.commRing` `Opposite.unop` `Opposite.op` `commRing` `RingHom.instFunLike` `Hom.hom` `CategoryTheory.Functor.obj` `CommRingCat` `instCategory` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `coyoneda` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `coyonedaUnique` `Unique.instInhabited`	—	—
`coyonedaUnique_inv_app_hom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Pi.commRing` `Opposite.unop` `Opposite.op` `RingHom.instFunLike` `Hom.hom` `CategoryTheory.Functor.obj` `CommRingCat` `instCategory` `CategoryTheory.Functor.id` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `coyoneda` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `coyonedaUnique`	—	—
`coyoneda_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CommRingCat` `instCategory` `of` `Pi.commRing` `Opposite.unop` `carrier` `commRing` `ofHom` `Pi.ringHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp` `Hom.hom` `Pi.evalRingHom` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `coyoneda` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`coyoneda_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CommRingCat` `instCategory` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `coyoneda` `ofHom` `Pi.commRing` `Opposite.unop` `carrier` `commRing` `Pi.ringHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp` `Hom.hom` `Pi.evalRingHom`	—	—
`coyoneda_obj_obj_carrier` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `CommRingCat` `instCategory` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `coyoneda`	—	—
`free_map_coe` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CommRingCat` `instCategory` `free` `carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.rename`	—	—
`free_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CommRingCat` `instCategory` `free` `MvPolynomial` `Int.instCommSemiring`	—	—
`instIsLeftAdjointCommMonCatUnderMonoidAlgebra` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `CommMonCat` `CommMonCat.instCategory` `CategoryTheory.Under` `CommRingCat` `instCategory` `CategoryTheory.instCategoryUnder` `monoidAlgebra`	—	—
`instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CommMonCat` `CommMonCat.instCategory` `CommRingCat` `instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `MonoidHom` `CommMonCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CommMonCat.str` `MonoidHom.instFunLike` `CommMonCat.instConcreteCategoryMonoidHomCarrier` `instHasForget₂RingHomCarrierCommMonCatMonoidHomCarrier`	—	`CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `CategoryTheory.Limits.hasSmallestColimitsOfHasColimits` `Colimits.hasColimits_commRingCat`
`instIsRightAdjointForgetRingHomCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `CommRingCat` `instCategory` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	—
`instIsRightAdjointOppositeObjFunctorTypeYoneda` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `Opposite` `CommRingCat` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.yoneda`	—	—
`monoidAlgebra_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CommMonCat` `CommMonCat.instCategory` `CategoryTheory.Under` `CommRingCat` `instCategory` `CategoryTheory.instCategoryUnder` `monoidAlgebra` `CategoryTheory.Under.homMk` `of` `MonoidAlgebra` `carrier` `CommMonCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `MonoidAlgebra.commRing` `CommMonCat.str` `ofHom` `MonoidAlgebra.singleOneRingHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidAlgebra.mapDomainRingHom` `CommMonCat.Hom.hom`	—	—
`monoidAlgebra_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CommMonCat` `CommMonCat.instCategory` `CategoryTheory.Under` `CommRingCat` `instCategory` `CategoryTheory.instCategoryUnder` `monoidAlgebra` `of` `MonoidAlgebra` `carrier` `CommMonCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `MonoidAlgebra.commRing` `CommMonCat.str` `ofHom` `MonoidAlgebra.singleOneRingHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—

---

← Back to Index