Documentation Verification Report

ExactFunctor

📁 Source: Mathlib/CategoryTheory/Limits/ExactFunctor.lean

Statistics

Metric	Count
Definitions `ExactFunctor`, `forget`, `of`, `whiskeringLeft`, `whiskeringRight`, `forget`, `fullyFaithful`, `of`, `ofExact`, `whiskeringLeft`, `whiskeringRight`, `RightExactFunctor`, `forget`, `fullyFaithful`, `of`, `ofExact`, `whiskeringLeft`, `whiskeringRight`, `exactFunctor`, `leftExactFunctor`, `rightExactFunctor`, `«term_⥤ᵣ_»`, `«term_⥤ₑ_»`, `«term_⥤ₗ_»`	24
Theorems `forget_map`, `forget_obj`, `forget_obj_of`, `of_fst`, `whiskeringLeft_map_app`, `whiskeringLeft_obj_map`, `whiskeringLeft_obj_obj_obj`, `whiskeringRight_map_app`, `whiskeringRight_obj_map`, `whiskeringRight_obj_obj_obj`, `forget_map`, `forget_obj`, `forget_obj_of`, `ofExact_map`, `ofExact_map_hom`, `ofExact_obj`, `of_fst`, `whiskeringLeft_map_app`, `whiskeringLeft_obj_map`, `whiskeringLeft_obj_obj_obj`, `whiskeringRight_map_app`, `whiskeringRight_obj_map`, `whiskeringRight_obj_obj_obj`, `forget_map`, `forget_obj`, `forget_obj_of`, `ofExact_map`, `ofExact_map_hom`, `ofExact_obj`, `of_fst`, `whiskeringLeft_map_app`, `whiskeringLeft_obj_map`, `whiskeringLeft_obj_obj_obj`, `whiskeringRight_map_app`, `whiskeringRight_obj_map`, `whiskeringRight_obj_obj_obj`, `exactFunctor_iff`, `exactFunctor_le_leftExactFunctor`, `exactFunctor_le_rightExactFunctor`, `instPreservesFiniteColimitsObjFunctorExactFunctor`, `instPreservesFiniteColimitsObjFunctorRightExactFunctor`, `instPreservesFiniteLimitsObjFunctorExactFunctor`, `instPreservesFiniteLimitsObjFunctorLeftExactFunctor`, `leftExactFunctor_iff`, `rightExactFunctor_iff`	45
Total	69

CategoryTheory

Definitions

Name	Category	Theorems
`ExactFunctor` 📖	CompOp	18 math math: `LeftExactFunctor.ofExact_map`, `ExactFunctor.forget_map`, `AdditiveFunctor.ofExact_obj_fst`, `ExactFunctor.forget_obj`, `RightExactFunctor.ofExact_map_hom`, `AdditiveFunctor.ofExact_map`, `ExactFunctor.whiskeringLeft_map_app`, `LeftExactFunctor.ofExact_map_hom`, `ExactFunctor.whiskeringLeft_obj_obj_obj`, `ExactFunctor.whiskeringLeft_obj_map`, `ExactFunctor.whiskeringRight_obj_obj_obj`, `RightExactFunctor.ofExact_map`, `LeftExactFunctor.ofExact_obj`, `ExactFunctor.whiskeringRight_map_app`, `RightExactFunctor.ofExact_obj`, `ExactFunctor.forget_obj_of`, `AdditiveFunctor.ofExact_map_hom`, `ExactFunctor.whiskeringRight_obj_map`
`RightExactFunctor` 📖	CompOp	15 math math: `RightExactFunctor.whiskeringRight_obj_obj_obj`, `RightExactFunctor.whiskeringLeft_map_app`, `RightExactFunctor.whiskeringRight_map_app`, `RightExactFunctor.ofExact_map_hom`, `AdditiveFunctor.ofRightExact_map`, `RightExactFunctor.forget_map`, `RightExactFunctor.ofExact_map`, `AdditiveFunctor.ofRightExact_obj_fst`, `RightExactFunctor.ofExact_obj`, `RightExactFunctor.whiskeringLeft_obj_obj_obj`, `RightExactFunctor.forget_obj_of`, `RightExactFunctor.whiskeringLeft_obj_map`, `RightExactFunctor.forget_obj`, `AdditiveFunctor.ofRightExact_map_hom`, `RightExactFunctor.whiskeringRight_obj_map`
`exactFunctor` 📖	CompOp	25 math math: `LeftExactFunctor.ofExact_map`, `ExactFunctor.forget_map`, `exactFunctor_le_additiveFunctor`, `AdditiveFunctor.ofExact_obj_fst`, `ExactFunctor.forget_obj`, `RightExactFunctor.ofExact_map_hom`, `AdditiveFunctor.ofExact_map`, `ExactFunctor.whiskeringLeft_map_app`, `LeftExactFunctor.ofExact_map_hom`, `ExactFunctor.whiskeringLeft_obj_obj_obj`, `ExactFunctor.whiskeringLeft_obj_map`, `ExactFunctor.whiskeringRight_obj_obj_obj`, `RightExactFunctor.ofExact_map`, `LeftExactFunctor.ofExact_obj`, `ExactFunctor.whiskeringRight_map_app`, `exactFunctor_le_leftExactFunctor`, `RightExactFunctor.ofExact_obj`, `ExactFunctor.forget_obj_of`, `ExactFunctor.of_fst`, `instPreservesFiniteColimitsObjFunctorExactFunctor`, `AdditiveFunctor.ofExact_map_hom`, `exactFunctor_iff`, `ExactFunctor.whiskeringRight_obj_map`, `exactFunctor_le_rightExactFunctor`, `instPreservesFiniteLimitsObjFunctorExactFunctor`
`leftExactFunctor` 📖	CompOp	26 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_le_additiveFunctor`, `LeftExactFunctor.ofExact_map_hom`, `Functor.mapGrpFunctor_map_app`, `AdditiveFunctor.ofLeftExact_obj_fst`, `instPreservesFiniteLimitsObjFunctorLeftExactFunctor`, `LeftExactFunctor.ofExact_obj`, `AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux`, `leftExactFunctor_iff`, `LeftExactFunctor.of_fst`, `exactFunctor_le_leftExactFunctor`, `Functor.mapCommGrpFunctor_map`, `RightExactFunctor.ofExact_obj`, `LeftExactFunctor.whiskeringLeft_obj_map`, `AdditiveFunctor.ofLeftExact_map_hom`, `LeftExactFunctor.whiskeringRight_obj_obj_obj`, `LeftExactFunctor.forget_obj_of`
`rightExactFunctor` 📖	CompOp	21 math math: `RightExactFunctor.whiskeringRight_obj_obj_obj`, `RightExactFunctor.whiskeringLeft_map_app`, `RightExactFunctor.whiskeringRight_map_app`, `RightExactFunctor.ofExact_map_hom`, `AdditiveFunctor.ofRightExact_map`, `RightExactFunctor.forget_map`, `RightExactFunctor.ofExact_map`, `LeftExactFunctor.ofExact_obj`, `AdditiveFunctor.ofRightExact_obj_fst`, `RightExactFunctor.of_fst`, `instPreservesFiniteColimitsObjFunctorRightExactFunctor`, `RightExactFunctor.ofExact_obj`, `rightExactFunctor_iff`, `RightExactFunctor.whiskeringLeft_obj_obj_obj`, `RightExactFunctor.forget_obj_of`, `RightExactFunctor.whiskeringLeft_obj_map`, `rightExactFunctor_le_additiveFunctor`, `exactFunctor_le_rightExactFunctor`, `RightExactFunctor.forget_obj`, `AdditiveFunctor.ofRightExact_map_hom`, `RightExactFunctor.whiskeringRight_obj_map`
`«term_⥤ᵣ_»` 📖	CompOp	—
`«term_⥤ₑ_»` 📖	CompOp	—
`«term_⥤ₗ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exactFunctor_iff` 📖	mathematical	—	`exactFunctor` `Limits.PreservesFiniteLimits` `Limits.PreservesFiniteColimits`	—	—
`exactFunctor_le_leftExactFunctor` 📖	mathematical	—	`ObjectProperty` `Functor` `Category.toCategoryStruct` `Functor.category` `Pi.hasLe` `Prop.le` `exactFunctor` `leftExactFunctor`	—	—
`exactFunctor_le_rightExactFunctor` 📖	mathematical	—	`ObjectProperty` `Functor` `Category.toCategoryStruct` `Functor.category` `Pi.hasLe` `Prop.le` `exactFunctor` `rightExactFunctor`	—	—
`instPreservesFiniteColimitsObjFunctorExactFunctor` 📖	mathematical	—	`Limits.PreservesFiniteColimits` `ObjectProperty.FullSubcategory.obj` `Functor` `Functor.category` `exactFunctor`	—	`ObjectProperty.FullSubcategory.property`
`instPreservesFiniteColimitsObjFunctorRightExactFunctor` 📖	mathematical	—	`Limits.PreservesFiniteColimits` `ObjectProperty.FullSubcategory.obj` `Functor` `Functor.category` `rightExactFunctor`	—	`ObjectProperty.FullSubcategory.property`
`instPreservesFiniteLimitsObjFunctorExactFunctor` 📖	mathematical	—	`Limits.PreservesFiniteLimits` `ObjectProperty.FullSubcategory.obj` `Functor` `Functor.category` `exactFunctor`	—	`ObjectProperty.FullSubcategory.property`
`instPreservesFiniteLimitsObjFunctorLeftExactFunctor` 📖	mathematical	—	`Limits.PreservesFiniteLimits` `ObjectProperty.FullSubcategory.obj` `Functor` `Functor.category` `leftExactFunctor`	—	`ObjectProperty.FullSubcategory.property`
`leftExactFunctor_iff` 📖	mathematical	—	`leftExactFunctor` `Limits.PreservesFiniteLimits`	—	—
`rightExactFunctor_iff` 📖	mathematical	—	`rightExactFunctor` `Limits.PreservesFiniteColimits`	—	—

CategoryTheory.ExactFunctor

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	5 math math: `forget_map`, `forget_obj`, `whiskeringLeft_map_app`, `whiskeringRight_map_app`, `forget_obj_of`
`of` 📖	CompOp	2 math math: `forget_obj_of`, `of_fst`
`whiskeringLeft` 📖	CompOp	3 math math: `whiskeringLeft_map_app`, `whiskeringLeft_obj_obj_obj`, `whiskeringLeft_obj_map`
`whiskeringRight` 📖	CompOp	3 math math: `whiskeringRight_obj_obj_obj`, `whiskeringRight_map_app`, `whiskeringRight_obj_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `forget` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `forget` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`forget_obj_of` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `forget` `of`	—	—
`of_fst` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `of`	—	—
`whiskeringLeft_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `whiskeringLeft` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`whiskeringLeft_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor.obj` `whiskeringLeft` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`whiskeringLeft_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `whiskeringLeft` `CategoryTheory.Functor.comp`	—	—
`whiskeringRight_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `whiskeringRight` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`whiskeringRight_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor.obj` `whiskeringRight` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`whiskeringRight_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `whiskeringRight` `CategoryTheory.Functor.comp`	—	—

CategoryTheory.LeftExactFunctor

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	5 math math: `forget_map`, `forget_obj`, `whiskeringRight_map_app`, `whiskeringLeft_map_app`, `forget_obj_of`
`fullyFaithful` 📖	CompOp	—
`of` 📖	CompOp	2 math math: `of_fst`, `forget_obj_of`
`ofExact` 📖	CompOp	3 math math: `ofExact_map`, `ofExact_map_hom`, `ofExact_obj`
`whiskeringLeft` 📖	CompOp	3 math math: `whiskeringLeft_map_app`, `whiskeringLeft_obj_obj_obj`, `whiskeringLeft_obj_map`
`whiskeringRight` 📖	CompOp	3 math math: `whiskeringRight_map_app`, `whiskeringRight_obj_map`, `whiskeringRight_obj_obj_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `forget` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `forget` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`forget_obj_of` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `forget` `of`	—	—
`ofExact_map` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.exactFunctor` `CategoryTheory.LeftExactFunctor` `ofExact` `CategoryTheory.Functor.map`	—	`ofExact_map_hom`
`ofExact_map_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.exactFunctor` `CategoryTheory.LeftExactFunctor` `ofExact` `CategoryTheory.Functor.map`	—	—
`ofExact_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.LeftExactFunctor` `CategoryTheory.leftExactFunctor` `ofExact` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.property`	—	—
`of_fst` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `of`	—	—
`whiskeringLeft_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `whiskeringLeft` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`whiskeringLeft_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor.obj` `whiskeringLeft` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`whiskeringLeft_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `whiskeringLeft` `CategoryTheory.Functor.comp`	—	—
`whiskeringRight_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `whiskeringRight` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`whiskeringRight_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor.obj` `whiskeringRight` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`whiskeringRight_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.leftExactFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.LeftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `whiskeringRight` `CategoryTheory.Functor.comp`	—	—

CategoryTheory.RightExactFunctor

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	5 math math: `whiskeringLeft_map_app`, `whiskeringRight_map_app`, `forget_map`, `forget_obj_of`, `forget_obj`
`fullyFaithful` 📖	CompOp	—
`of` 📖	CompOp	2 math math: `of_fst`, `forget_obj_of`
`ofExact` 📖	CompOp	3 math math: `ofExact_map_hom`, `ofExact_map`, `ofExact_obj`
`whiskeringLeft` 📖	CompOp	3 math math: `whiskeringLeft_map_app`, `whiskeringLeft_obj_obj_obj`, `whiskeringLeft_obj_map`
`whiskeringRight` 📖	CompOp	3 math math: `whiskeringRight_obj_obj_obj`, `whiskeringRight_map_app`, `whiskeringRight_obj_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `forget` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `forget` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`forget_obj_of` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `forget` `of`	—	—
`ofExact_map` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.exactFunctor` `CategoryTheory.RightExactFunctor` `ofExact` `CategoryTheory.Functor.map`	—	`ofExact_map_hom`
`ofExact_map_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.exactFunctor` `CategoryTheory.RightExactFunctor` `ofExact` `CategoryTheory.Functor.map`	—	—
`ofExact_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.exactFunctor` `CategoryTheory.RightExactFunctor` `CategoryTheory.rightExactFunctor` `ofExact` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.leftExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.property`	—	—
`of_fst` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `of`	—	—
`whiskeringLeft_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `whiskeringLeft` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`whiskeringLeft_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor.obj` `whiskeringLeft` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`whiskeringLeft_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `whiskeringLeft` `CategoryTheory.Functor.comp`	—	—
`whiskeringRight_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `whiskeringRight` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`whiskeringRight_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor.obj` `whiskeringRight` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`whiskeringRight_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.rightExactFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.RightExactFunctor` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.FullSubcategory` `whiskeringRight` `CategoryTheory.Functor.comp`	—	—

---

← Back to Index