Documentation Verification Report

Adjunctions

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

Statistics

Metric	Count
Definitions `adj`, `free`, `forget₂CommMonAdj`, `units`, `abelianize`, `abelianizeAdj`, `adj`, `forget₂MonAdj`, `free`, `units`	10
Theorems `free_map_coe`, `free_obj_coe`, `instIsLeftAdjointFree`, `instIsRightAdjointForgetAddMonoidHomCarrier`, `instPreservesMonomorphismsFree`, `units_obj_coe`, `val_inv_units_map_hom_apply`, `val_units_map_hom_apply`, `instIsRightAdjointForgetMonoidHomCarrier`, `units_obj_coe`, `val_inv_units_map_hom_apply`, `val_units_map_hom_apply`, `instIsRightAdjointCommGrpCatCommMonCatUnits`, `instIsRightAdjointGrpCatMonCatUnits`	14
Total	24

AddCommGrpCat

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`free` 📖	CompOp	12 math math: `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃`, `instPreservesMonomorphismsFree`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply`, `free_map_coe`, `free_obj_coe`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf`, `instIsLeftAdjointFree`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`free_map_coe` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CategoryTheory.types` `AddCommGrpCat` `instCategory` `free` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Functor.map` `FreeAbelianGroup` `FreeAbelianGroup.instMonad`	—	—
`free_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `CategoryTheory.types` `AddCommGrpCat` `instCategory` `free` `FreeAbelianGroup`	—	—
`instIsLeftAdjointFree` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `CategoryTheory.types` `AddCommGrpCat` `instCategory` `free`	—	—
`instIsRightAdjointForgetAddMonoidHomCarrier` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CategoryTheory.types` `AddCommGrpCat` `instCategory` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	—
`instPreservesMonomorphismsFree` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `CategoryTheory.types` `AddCommGrpCat` `instCategory` `free`	—	`CategoryTheory.Limits.IsZero.eq_of_tgt` `CategoryTheory.Limits.IsInitial.isZero` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `instIsLeftAdjointFree` `CategoryTheory.Limits.Types.initial_iff_empty` `CategoryTheory.mono_iff_injective` `Function.Injective.hasLeftInverse` `CategoryTheory.IsSplitMono.mk'` `CategoryTheory.types_ext` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.instIsSplitMonoMap`

CommGrpCat

Definitions

Name	Category	Theorems
`forget₂CommMonAdj` 📖	CompOp	—

CommMonCat

Definitions

Name	Category	Theorems
`units` 📖	CompOp	4 math math: `val_units_map_hom_apply`, `val_inv_units_map_hom_apply`, `instIsRightAdjointCommGrpCatCommMonCatUnits`, `units_obj_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`units_obj_coe` 📖	mathematical	—	`CommGrpCat.carrier` `CategoryTheory.Functor.obj` `CommMonCat` `instCategory` `CommGrpCat` `CommGrpCat.instCategory` `units` `Units` `carrier` `CommMonoid.toMonoid` `str`	—	—
`val_inv_units_map_hom_apply` 📖	mathematical	—	`Units.val` `carrier` `CommMonoid.toMonoid` `str` `Units` `Units.instInv` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `CommGrpCat.Hom.hom` `CommGrpCat.of` `Units.instCommGroupUnits` `CategoryTheory.Functor.map` `CommMonCat` `instCategory` `CommGrpCat` `CommGrpCat.instCategory` `units` `Monoid.toMulOneClass` `Hom.hom`	—	—
`val_units_map_hom_apply` 📖	mathematical	—	`Units.val` `carrier` `CommMonoid.toMonoid` `str` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `CommGrpCat.Hom.hom` `CommGrpCat.of` `Units.instCommGroupUnits` `CategoryTheory.Functor.map` `CommMonCat` `instCategory` `CommGrpCat` `CommGrpCat.instCategory` `units` `Monoid.toMulOneClass` `Hom.hom`	—	—

GrpCat

Definitions

Name	Category	Theorems
`abelianize` 📖	CompOp	—
`abelianizeAdj` 📖	CompOp	—
`adj` 📖	CompOp	—
`forget₂MonAdj` 📖	CompOp	—
`free` 📖	CompOp	—

Theorems

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

MonCat

Definitions

Name	Category	Theorems
`units` 📖	CompOp	4 math math: `val_units_map_hom_apply`, `val_inv_units_map_hom_apply`, `units_obj_coe`, `instIsRightAdjointGrpCatMonCatUnits`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`units_obj_coe` 📖	mathematical	—	`GrpCat.carrier` `CategoryTheory.Functor.obj` `MonCat` `instCategory` `GrpCat` `GrpCat.instCategory` `units` `Units` `carrier` `str`	—	—
`val_inv_units_map_hom_apply` 📖	mathematical	—	`Units.val` `carrier` `str` `Units` `Units.instInv` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `GrpCat.Hom.hom` `GrpCat.of` `Units.instGroup` `CategoryTheory.Functor.map` `MonCat` `instCategory` `GrpCat` `GrpCat.instCategory` `units` `Monoid.toMulOneClass` `Hom.hom`	—	—
`val_units_map_hom_apply` 📖	mathematical	—	`Units.val` `carrier` `str` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `GrpCat.Hom.hom` `GrpCat.of` `Units.instGroup` `CategoryTheory.Functor.map` `MonCat` `instCategory` `GrpCat` `GrpCat.instCategory` `units` `Monoid.toMulOneClass` `Hom.hom`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRightAdjointCommGrpCatCommMonCatUnits` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `CommGrpCat` `CommGrpCat.instCategory` `CommMonCat` `CommMonCat.instCategory` `CommMonCat.units`	—	—
`instIsRightAdjointGrpCatMonCatUnits` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `GrpCat` `GrpCat.instCategory` `MonCat` `MonCat.instCategory` `MonCat.units`	—	—

---

← Back to Index