Documentation Verification Report

EssentialImage

📁 Source: Mathlib/CategoryTheory/EssentialImage.lean

Statistics

Metric	Count
Definitions `EssImageSubcategory`, `essImage`, `getIso`, `liftFunctor`, `liftFunctorCompIso`, `witness`, `objObjPreimageIso`, `objPreimage`, `toEssImage`, `toEssImageCompι`	10
Theorems `mem_essImage`, `toEssImage`, `toEssImage`, `toEssImage`, `liftFunctorCompIso_hom_app`, `liftFunctorCompIso_inv_app`, `liftFunctor_map`, `liftFunctor_obj`, `ofIso`, `ofNatIso`, `essImage_comp_apply_of_essSurj`, `essImage_comp_of_essSurj`, `essImage_eq_of_natIso`, `essImage_ext`, `essImage_ι_comp`, `essSurj_comp`, `essSurj_of_comp_fully_faithful`, `essSurj_of_iso`, `essSurj_of_surj`, `instEssSurjId`, `instIsClosedUnderIsomorphismsEssImage`, `obj_mem_essImage`, `toEssImageCompι_hom_app`, `toEssImageCompι_inv_app`, `toEssImage_map_hom`, `toEssImage_obj_obj`	26
Total	36

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`EssImageSubcategory` 📖	CompOp	21 math math: `CategoryTheory.equivEssImageOfReflective_unitIso`, `EssImageSubcategory.associator_inv_def`, `EssImageSubcategory.associator_hom_def`, `Faithful.toEssImage`, `EssImageSubcategory.tensor_obj`, `essImage.liftFunctorCompIso_hom_app`, `toEssImage_map_hom`, `CategoryTheory.equivEssImageOfReflective_functor`, `EssImageSubcategory.toUnit_def`, `essImage.liftFunctorCompIso_inv_app`, `CategoryTheory.equivEssImageOfReflective_inverse`, `essImage.liftFunctor_obj`, `CategoryTheory.Equivalence.fullyFaithfulToEssImage`, `toEssImageCompι_inv_app`, `EssSurj.toEssImage`, `toEssImageCompι_hom_app`, `CategoryTheory.equivEssImageOfReflective_counitIso`, `toEssImage_obj_obj`, `essImage.liftFunctor_map`, `EssImageSubcategory.lift_def`, `Full.toEssImage`
`essImage` 📖	CompOp	56 math math: `CategoryTheory.ObjectProperty.instIsTriangulatedEssImageOfIsTriangulatedOfFull`, `CategoryTheory.equivEssImageOfReflective_unitIso`, `CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone`, `EssImageSubcategory.associator_inv_def`, `CategoryTheory.mem_essImage_of_unit_isSplitMono`, `CondensedMod.isDiscrete_tfae`, `EssImageSubcategory.associator_hom_def`, `Faithful.toEssImage`, `LightCondMod.isDiscrete_tfae`, `AlgebraicGeometry.AffineScheme.mk_obj`, `CategoryTheory.Sheaf.mem_essImage_of_isConstant`, `obj_mem_essImage`, `CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful`, `EssImageSubcategory.tensor_obj`, `CategoryTheory.essImage_yonedaMon`, `essImage_ι_comp`, `essImage_mapGrp`, `essImage_comp_of_essSurj`, `CategoryTheory.essImage_yonedaGrp`, `essImage_underPost`, `toEssImage_map_hom`, `CategoryTheory.Adjunction.mem_essImage_of_counit_isIso`, `CategoryTheory.equivEssImageOfReflective_functor`, `CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage`, `essImage_eq_of_natIso`, `EssSurj.mem_essImage`, `essImage_comp_apply_of_essSurj`, `AlgebraicGeometry.AffineScheme.forgetToScheme_map`, `CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage`, `AlgebraicGeometry.isAffine_affineScheme`, `EssImageSubcategory.toUnit_def`, `CondensedSet.isDiscrete_tfae`, `CategoryTheory.Sheaf.isConstant_iff_mem_essImage`, `CategoryTheory.Limits.instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful`, `CategoryTheory.equivEssImageOfReflective_inverse`, `LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone`, `essImage_mapMon`, `instIsClosedUnderIsomorphismsEssImage`, `LightCondSet.isDiscrete_tfae`, `CategoryTheory.Equivalence.fullyFaithfulToEssImage`, `toEssImageCompι_inv_app`, `AlgebraicGeometry.AffineScheme.forgetToScheme_obj`, `EssSurj.toEssImage`, `toEssImageCompι_hom_app`, `CategoryTheory.equivEssImageOfReflective_counitIso`, `essImage_overPost`, `toEssImage_obj_obj`, `AlgebraicGeometry.isIso_fromTildeΓ_iff`, `EssImageSubcategory.lift_def`, `CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage`, `Full.toEssImage`, `CategoryTheory.Sheaf.IsConstant.mem_essImage`, `AlgebraicGeometry.essImage_Spec`, `CategoryTheory.mem_essImage_of_counit_isSplitEpi`, `essImage_ext_iff`, `CategoryTheory.Adjunction.mem_essImage_of_unit_isIso`
`objObjPreimageIso` 📖	CompOp	3 math math: `essImage.liftFunctorCompIso_hom_app`, `essImage.liftFunctorCompIso_inv_app`, `essImage.liftFunctor_map`
`objPreimage` 📖	CompOp	4 math math: `essImage.liftFunctorCompIso_hom_app`, `essImage.liftFunctorCompIso_inv_app`, `essImage.liftFunctor_obj`, `essImage.liftFunctor_map`
`toEssImage` 📖	CompOp	14 math math: `Faithful.toEssImage`, `essImage.liftFunctorCompIso_hom_app`, `toEssImage_map_hom`, `CategoryTheory.equivEssImageOfReflective_functor`, `essImage.liftFunctorCompIso_inv_app`, `essImage.liftFunctor_obj`, `CategoryTheory.Equivalence.fullyFaithfulToEssImage`, `toEssImageCompι_inv_app`, `EssSurj.toEssImage`, `toEssImageCompι_hom_app`, `CategoryTheory.equivEssImageOfReflective_counitIso`, `toEssImage_obj_obj`, `essImage.liftFunctor_map`, `Full.toEssImage`
`toEssImageCompι` 📖	CompOp	2 math math: `toEssImageCompι_inv_app`, `toEssImageCompι_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essImage_comp_apply_of_essSurj` 📖	mathematical	—	`essImage` `comp`	—	`EssSurj.mem_essImage`
`essImage_comp_of_essSurj` 📖	mathematical	—	`essImage` `comp`	—	`essImage_comp_apply_of_essSurj`
`essImage_eq_of_natIso` 📖	mathematical	—	`essImage`	—	`essImage.ofNatIso`
`essImage_ext` 📖	—	`map` `CategoryTheory.ObjectProperty.FullSubcategory` `essImage` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι`	—	—	`map_injective` `CategoryTheory.ObjectProperty.faithful_ι`
`essImage_ι_comp` 📖	mathematical	—	`essImage` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `comp` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.ObjectProperty.map`	—	`CategoryTheory.ObjectProperty.FullSubcategory.property`
`essSurj_comp` 📖	mathematical	—	`EssSurj` `comp`	—	—
`essSurj_of_comp_fully_faithful` 📖	mathematical	—	`EssSurj`	—	—
`essSurj_of_iso` 📖	mathematical	—	`EssSurj`	—	`essImage.ofNatIso` `EssSurj.mem_essImage`
`essSurj_of_surj` 📖	mathematical	`obj`	`EssSurj`	—	`obj_mem_essImage`
`instEssSurjId` 📖	mathematical	—	`EssSurj` `id`	—	—
`instIsClosedUnderIsomorphismsEssImage` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `essImage`	—	`essImage.ofIso`
`obj_mem_essImage` 📖	mathematical	—	`essImage` `obj`	—	—
`toEssImageCompι_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.ObjectProperty.FullSubcategory` `essImage` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.lift` `obj_mem_essImage` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `EssImageSubcategory` `toEssImage` `toEssImageCompι` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `obj`	—	`obj_mem_essImage`
`toEssImageCompι_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.ObjectProperty.FullSubcategory` `essImage` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.lift` `obj_mem_essImage` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `EssImageSubcategory` `toEssImage` `toEssImageCompι` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `obj`	—	`obj_mem_essImage`
`toEssImage_map_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `essImage` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `obj_mem_essImage` `map` `EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `toEssImage`	—	`obj_mem_essImage`
`toEssImage_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `essImage` `obj` `EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `toEssImage`	—	—

CategoryTheory.Functor.EssSurj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_essImage` 📖	mathematical	—	`CategoryTheory.Functor.essImage`	—	—
`toEssImage` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.essImage` `CategoryTheory.Functor.toEssImage`	—	—

CategoryTheory.Functor.Faithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toEssImage` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.essImage` `CategoryTheory.Functor.toEssImage`	—	`CategoryTheory.Functor.obj_mem_essImage` `CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift`

CategoryTheory.Functor.Full

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toEssImage` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.essImage` `CategoryTheory.Functor.toEssImage`	—	`CategoryTheory.Functor.obj_mem_essImage` `CategoryTheory.ObjectProperty.instFullFullSubcategoryLift`

CategoryTheory.Functor.essImage

Definitions

Name	Category	Theorems
`getIso` 📖	CompOp	—
`liftFunctor` 📖	CompOp	4 math math: `liftFunctorCompIso_hom_app`, `liftFunctorCompIso_inv_app`, `liftFunctor_obj`, `liftFunctor_map`
`liftFunctorCompIso` 📖	CompOp	2 math math: `liftFunctorCompIso_hom_app`, `liftFunctorCompIso_inv_app`
`witness` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftFunctorCompIso_hom_app` 📖	mathematical	`CategoryTheory.Functor.essImage` `CategoryTheory.Functor.obj`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `liftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `liftFunctorCompIso` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.toEssImage` `CategoryTheory.Functor.objPreimage` `CategoryTheory.Functor.EssSurj.toEssImage` `CategoryTheory.Functor.objObjPreimageIso`	—	—
`liftFunctorCompIso_inv_app` 📖	mathematical	`CategoryTheory.Functor.essImage` `CategoryTheory.Functor.obj`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `liftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `liftFunctorCompIso` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.toEssImage` `CategoryTheory.Functor.objPreimage` `CategoryTheory.Functor.EssSurj.toEssImage` `CategoryTheory.Functor.objObjPreimageIso`	—	—
`liftFunctor_map` 📖	mathematical	`CategoryTheory.Functor.essImage` `CategoryTheory.Functor.obj`	`CategoryTheory.Functor.map` `liftFunctor` `CategoryTheory.Functor.preimage` `CategoryTheory.Functor.objPreimage` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.toEssImage` `CategoryTheory.Functor.EssSurj.toEssImage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.objObjPreimageIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.EssSurj.toEssImage`
`liftFunctor_obj` 📖	mathematical	`CategoryTheory.Functor.essImage` `CategoryTheory.Functor.obj`	`liftFunctor` `CategoryTheory.Functor.objPreimage` `CategoryTheory.Functor.EssImageSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.toEssImage` `CategoryTheory.Functor.EssSurj.toEssImage`	—	—
`ofIso` 📖	—	`CategoryTheory.Functor.essImage`	—	—	`Nonempty.map`
`ofNatIso` 📖	—	`CategoryTheory.Functor.essImage`	—	—	`Nonempty.map`

---

← Back to Index