Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean

Statistics

Metric	Count
Definitions `ReflectsIsomorphisms`	1
Theorems `reflectsIsomorphisms`, `reflects`, `instReflectsIsomorphismsFunctorObjWhiskeringRight`, `isIso_iff_of_reflects_iso`, `isIso_of_reflects_iso`, `reflectsIsomorphisms_comp`, `reflectsIsomorphisms_of_comp`, `reflectsIsomorphisms_of_full_and_faithful`	8
Total	9

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instReflectsIsomorphismsFunctorObjWhiskeringRight` 📖	mathematical	—	`Functor.ReflectsIsomorphisms` `Functor` `Functor.category` `Functor.obj` `Functor.whiskeringRight`	—	`NatTrans.isIso_iff_isIso_app` `isIso_iff_of_reflects_iso` `NatIso.isIso_app_of_isIso`
`isIso_iff_of_reflects_iso` 📖	mathematical	—	`IsIso` `Functor.obj` `Functor.map`	—	`isIso_of_reflects_iso` `Functor.map_isIso`
`isIso_of_reflects_iso` 📖	mathematical	—	`IsIso`	—	`Functor.ReflectsIsomorphisms.reflects`
`reflectsIsomorphisms_comp` 📖	mathematical	—	`Functor.ReflectsIsomorphisms` `Functor.comp`	—	`isIso_of_reflects_iso`
`reflectsIsomorphisms_of_comp` 📖	mathematical	—	`Functor.ReflectsIsomorphisms`	—	`isIso_iff_of_reflects_iso` `Functor.map_isIso`
`reflectsIsomorphisms_of_full_and_faithful` 📖	mathematical	—	`Functor.ReflectsIsomorphisms`	—	`Functor.FullyFaithful.reflectsIsomorphisms`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`ReflectsIsomorphisms` 📖	CompData	80 math math: `ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier`, `CategoryTheory.reflectsIsomorphisms_comp`, `ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `CommRingCat.forgetReflectIsos`, `CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms`, `CategoryTheory.Monad.forget_reflects_iso`, `MonCat.forget_reflects_isos`, `CategoryTheory.instReflectsIsomorphismsMonadFunctorMonadToFunctor`, `SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `TopCommRingCat.instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `AddMonCat.forget_reflects_isos`, `GrpCat.forget_reflects_isos`, `CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos`, `AddMagmaCat.forgetReflectsIsos`, `CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms`, `SemimoduleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier`, `HopfAlgCat.forget_reflects_isos`, `CategoryTheory.Endofunctor.Algebra.forget_reflects_iso`, `BialgCat.forget_reflects_isos`, `CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight`, `CategoryTheory.HasClassifier.reflectsIsomorphismsOp`, `CommSemiRingCat.forgetReflectIsos`, `SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget`, `mapHomologicalComplex_reflects_iso`, `CategoryTheory.reflectsIsomorphisms_forget₂`, `CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms`, `CommBialgCat.reflectsIsomorphisms_forget`, `CategoryTheory.Mon.instReflectsIsomorphismsForget`, `CategoryTheory.isDetector_iff_reflectsIsomorphisms_coyoneda_obj`, `CategoryTheory.HasClassifier.reflectsIsomorphisms`, `CategoryTheory.Center.instReflectsIsomorphismsForget`, `AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace`, `Semigrp.forgetReflectsIsos`, `CategoryTheory.Limits.Cocones.reflects_cocone_isomorphism`, `CoalgCat.forget_reflects_isos`, `FullyFaithful.reflectsIsomorphisms`, `CommGrpCat.forget_reflects_isos`, `ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat`, `CategoryTheory.isCodetector_iff_reflectsIsomorphisms_yoneda_obj`, `CategoryTheory.CategoryOfElements.instReflectsIsomorphismsElementsπ`, `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful`, `ModuleCat.instReflectsIsomorphismsRestrictScalars`, `PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf`, `LightProfinite.forget_reflectsIsomorphisms`, `CompHausLike.forget_reflectsIsomorphisms`, `CategoryTheory.instReflectsIsomorphismsSheafSheafCompose`, `CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf`, `SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat`, `SemiRingCat.forgetReflectIsos`, `instReflectsIsomorphismsDiscreteObjWhiskeringLeftIncl`, `AddGrpCat.forget_reflects_isos`, `ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `RingCat.forgetReflectIsos`, `CommMonCat.forget_reflects_isos`, `AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForget₂AddMonoidHomCarrierCarrier`, `AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁`, `CategoryTheory.Comon.instReflectsIsomorphismsForget`, `CategoryTheory.Over.forget_reflects_iso`, `CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction`, `CategoryTheory.instReflectsIsomorphismsComonadFunctorComonadToFunctor`, `AlgCat.forget_reflects_isos`, `CommAlgCat.reflectsIsomorphisms_forget`, `CategoryTheory.MorphismProperty.Comma.instReflectsIsomorphismsCommaForgetOfRespectsIso`, `TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier`, `PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf`, `CommGrpCat.instReflectsIsomorphismsGrpCatForget₂MonoidHomCarrierCarrier`, `AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf`, `AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂`, `CategoryTheory.BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful`, `CategoryTheory.Limits.Cones.reflects_cone_isomorphism`, `MagmaCat.forgetReflectsIsos`, `AddCommMonCat.forget_reflects_isos`, `CategoryTheory.instReflectsIsomorphismsForgetTypeHom`, `CategoryTheory.Comonad.forget_reflects_iso`, `CategoryTheory.Under.forget_reflects_iso`, `AddSemigrp.forgetReflectsIsos`, `CategoryTheory.reflectsIsomorphisms_of_comp`, `CategoryTheory.Endofunctor.Coalgebra.forget_reflects_iso`, `AddCommGrpCat.forget_reflects_isos`, `ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite`

CategoryTheory.Functor.FullyFaithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflectsIsomorphisms` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms`	—	`isIso_of_isIso_map`

CategoryTheory.Functor.ReflectsIsomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflects` 📖	mathematical	—	`CategoryTheory.IsIso`	—	—

---

← Back to Index