Documentation Verification Report

LeftExactFunctor

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

Statistics

Metric	Count
Definitions `leftExactFunctorForgetEquivalence`, `inverse`, `inverseAux`, `unitIso`, `unitIsoAux`, `LeftExactFunctor`	6
Theorems `instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux`	1
Total	7

AddCommGrpCat

Definitions

Name	Category	Theorems
`leftExactFunctorForgetEquivalence` 📖	CompOp	—

AddCommGrpCat.leftExactFunctorForgetEquivalence

Definitions

Name	Category	Theorems
`inverse` 📖	CompOp	—
`inverseAux` 📖	CompOp	1 math math: `instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux`
`unitIso` 📖	CompOp	—
`unitIsoAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.LeftExactFunctor` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `inverseAux`	—	`CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.instPreservesFiniteLimitsObjFunctorLeftExactFunctor` `CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms` `AddCommGrpCat.forget_reflects_isos` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `AddCommGrpCat.forget_preservesLimits`

CategoryTheory

Definitions

Name	Category	Theorems
`LeftExactFunctor` 📖	CompOp	20 math math: `LeftExactFunctor.ofExact_map`, `LeftExactFunctor.forget_map`, `LeftExactFunctor.forget_obj`, `Functor.mapGrpFunctor_obj`, `Functor.mapCommGrpFunctor_obj`, `AdditiveFunctor.ofLeftExact_map`, `LeftExactFunctor.whiskeringRight_map_app`, `LeftExactFunctor.whiskeringRight_obj_map`, `LeftExactFunctor.whiskeringLeft_map_app`, `LeftExactFunctor.whiskeringLeft_obj_obj_obj`, `LeftExactFunctor.ofExact_map_hom`, `Functor.mapGrpFunctor_map_app`, `AdditiveFunctor.ofLeftExact_obj_fst`, `LeftExactFunctor.ofExact_obj`, `AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux`, `Functor.mapCommGrpFunctor_map`, `LeftExactFunctor.whiskeringLeft_obj_map`, `AdditiveFunctor.ofLeftExact_map_hom`, `LeftExactFunctor.whiskeringRight_obj_obj_obj`, `LeftExactFunctor.forget_obj_of`

---

← Back to Index