FullyFaithful

📁 Source: Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Statistics

Metric	Count
Definitions `div`, `FullyFaithful`, `comp`, `homEquiv`, `id`, `isoEquiv`, `ofCompFaithful`, `ofFullyFaithful`, `ofIso`, `preimage`, `preimageIso`, `fullyFaithfulCancelRight`, `preimage`, `preimageIso`	14
Theorems `comp`, `div_comp`, `div_faithful`, `id`, `map_injective`, `of_comp`, `of_comp_eq`, `of_comp_iso`, `of_iso`, `comp`, `id`, `map_surjective`, `of_comp_faithful`, `of_comp_faithful_iso`, `of_iso`, `comp_preimage`, `faithful`, `full`, `homEquiv_apply`, `homEquiv_symm_apply`, `id_preimage`, `instSubsingleton`, `isIso_of_isIso_map`, `isoEquiv_apply`, `isoEquiv_symm_apply`, `map_bijective`, `map_injective`, `map_preimage`, `map_surjective`, `nonempty_iff_map_bijective`, `preimageIso_hom`, `preimageIso_inv`, `preimage_comp`, `preimage_comp_assoc`, `preimage_id`, `preimage_map`, `fullyFaithfulCancelRight_hom_app`, `fullyFaithfulCancelRight_inv_app`, `instFaithfulOfIsThin`, `mapIso_injective`, `map_injective`, `map_injective_iff`, `map_preimage`, `map_surjective`, `preimageIso_hom`, `preimageIso_inv`, `preimageIso_mapIso`, `preimage_comp`, `preimage_id`, `preimage_map`, `faithful_of_comp`, `isIso_of_fully_faithful`, `faithful_of_comp`	53
Total	67

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_of_fully_faithful` 📖	mathematical	—	`IsIso`	—	`Functor.map_injective` `Functor.map_comp` `Functor.map_preimage` `IsIso.hom_inv_id` `Functor.map_id` `IsIso.inv_hom_id`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`FullyFaithful` 📖	CompData	7 math math: `FullyFaithful.instSubsingleton`, `FullyFaithful.nonempty_iff_map_bijective`, `CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq`, `isDense_iff_fullyFaithful_restrictedULiftYoneda`, `CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff`, `CategoryTheory.Pseudofunctor.isPrestackFor_iff`, `CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful`
`fullyFaithfulCancelRight` 📖	CompOp	3 math math: `fullyFaithfulCancelRight_inv_app`, `fullyFaithfulCancelRight_hom_app`, `CategoryTheory.equivEssImageOfReflective_counitIso`
`preimage` 📖	CompOp	13 math math: `preimage_map`, `fullyFaithfulCancelRight_inv_app`, `CategoryTheory.MonoOver.image_map`, `preimage_comp`, `IsCoverDense.presheafIso_hom_app`, `fullyFaithfulCancelRight_hom_app`, `CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app`, `preimageIso_inv`, `preimageIso_hom`, `essImage.liftFunctor_map`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app`, `map_preimage`, `preimage_id`
`preimageIso` 📖	CompOp	3 math math: `preimageIso_inv`, `preimageIso_hom`, `preimageIso_mapIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fullyFaithfulCancelRight_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `fullyFaithfulCancelRight` `preimage` `obj` `comp`	—	—
`fullyFaithfulCancelRight_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `fullyFaithfulCancelRight` `preimage` `obj` `comp`	—	—
`instFaithfulOfIsThin` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`Faithful`	—	—
`mapIso_injective` 📖	mathematical	—	`CategoryTheory.Iso` `obj` `mapIso`	—	`CategoryTheory.Iso.ext` `map_injective`
`map_injective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `map`	—	`Faithful.map_injective`
`map_injective_iff` 📖	mathematical	—	`map`	—	`map_injective`
`map_preimage` 📖	mathematical	—	`map` `preimage`	—	`map_surjective`
`map_surjective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `map`	—	`Full.map_surjective`
`preimageIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `preimageIso` `preimage` `obj`	—	—
`preimageIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `preimageIso` `preimage` `obj`	—	—
`preimageIso_mapIso` 📖	mathematical	—	`preimageIso` `mapIso`	—	`CategoryTheory.Iso.ext` `preimage_map`
`preimage_comp` 📖	mathematical	—	`preimage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj`	—	`map_injective` `map_preimage` `map_comp`
`preimage_id` 📖	mathematical	—	`preimage` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `obj`	—	`map_injective` `map_preimage` `map_id`
`preimage_map` 📖	mathematical	—	`preimage` `map`	—	`map_injective` `map_preimage`

CategoryTheory.Functor.Faithful

Definitions

Name	Category	Theorems
`div` 📖	CompOp	2 math math: `div_faithful`, `div_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Functor.comp`	—	`CategoryTheory.Functor.map_injective`
`div_comp` 📖	mathematical	`CategoryTheory.Functor.obj` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map`	`CategoryTheory.Functor.comp` `div`	—	—
`div_faithful` 📖	mathematical	`CategoryTheory.Functor.obj` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map`	`CategoryTheory.Functor.Faithful` `div`	—	`Eq.faithful_of_comp` `div_comp`
`id` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Functor.id`	—	—
`map_injective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	—
`of_comp` 📖	mathematical	—	`CategoryTheory.Functor.Faithful`	—	`Function.Injective.of_comp` `CategoryTheory.Functor.map_injective`
`of_comp_eq` 📖	mathematical	`CategoryTheory.Functor.comp`	`CategoryTheory.Functor.Faithful`	—	`of_comp`
`of_comp_iso` 📖	mathematical	—	`CategoryTheory.Functor.Faithful`	—	`of_comp` `of_iso`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.Faithful`	—	`CategoryTheory.Functor.map_injective` `CategoryTheory.NatIso.naturality_1`

CategoryTheory.Functor.Full

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Functor.comp`	—	`CategoryTheory.Functor.map_preimage`
`id` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Functor.id`	—	—
`map_surjective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	—
`of_comp_faithful` 📖	mathematical	—	`CategoryTheory.Functor.Full`	—	`CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.map_preimage`
`of_comp_faithful_iso` 📖	mathematical	—	`CategoryTheory.Functor.Full`	—	`of_iso` `of_comp_faithful`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.Full`	—	`CategoryTheory.NatIso.naturality_1` `CategoryTheory.Functor.map_preimage` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_app_assoc`

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_preimage`
`homEquiv` 📖	CompOp	5 math math: `homEquiv_apply`, `homEquiv_symm_apply`, `CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app`, `CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app`, `CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app`
`id` 📖	CompOp	1 math math: `id_preimage`
`isoEquiv` 📖	CompOp	2 math math: `isoEquiv_apply`, `isoEquiv_symm_apply`
`ofCompFaithful` 📖	CompOp	—
`ofFullyFaithful` 📖	CompOp	—
`ofIso` 📖	CompOp	—
`preimage` 📖	CompOp	44 math math: `preimage_map`, `mapMon_preimage_hom`, `CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl_preimage`, `CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv`, `mapGrp_preimage`, `homNatIsoMaxRight_hom_app_down`, `monObj_mul`, `autMulEquivOfFullyFaithful_symm_apply_hom`, `compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down`, `preimage_comp`, `grpObj_inv`, `preimageIso_inv`, `preimageIso_hom`, `homEquiv_symm_apply`, `AlgebraicGeometry.Spec.map_preimage_unop`, `CategoryTheory.fullyFaithfulSheafToPresheaf_preimage_val`, `CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply`, `mulEquivEnd_symm_apply`, `whiskeringRight_preimage_app`, `homNatIso'_hom_app_down`, `AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace_preimage_hom`, `SheafOfModules.fullyFaithfulForget_preimage_val`, `monObj_one`, `comp_preimage`, `homMulEquiv_symm_apply`, `mapCommMon_preimage`, `CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom`, `AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom`, `autMulEquivOfFullyFaithful_symm_apply_inv`, `compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down`, `isMonHom_preimage`, `mapCommGrp_preimage`, `compUliftYonedaCompWhiskeringLeft_hom_app_app_down`, `CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom`, `CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv`, `grpObj_mul`, `preimage_comp_assoc`, `CategoryTheory.Coyoneda.fullyFaithful_preimage`, `CategoryTheory.Yoneda.fullyFaithful_preimage`, `grpObj_one`, `map_preimage`, `homNatIso_hom_app_down`, `id_preimage`, `preimage_id`
`preimageIso` 📖	CompOp	6 math math: `CategoryTheory.Equivalence.congrFullSubcategory_counitIso`, `preimageIso_inv`, `preimageIso_hom`, `CategoryTheory.Equivalence.congrFullSubcategory_unitIso`, `isoEquiv_symm_apply`, `CategoryTheory.Limits.CategoricalPullback.mkNatIso_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_preimage` 📖	mathematical	—	`preimage` `CategoryTheory.Functor.comp` `comp` `CategoryTheory.Functor.obj`	—	—
`faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful`	—	`map_injective`
`full` 📖	mathematical	—	`CategoryTheory.Functor.Full`	—	`map_surjective`
`homEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.Functor.map`	—	—
`homEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `preimage`	—	—
`id_preimage` 📖	mathematical	—	`preimage` `CategoryTheory.Functor.id` `id`	—	—
`instSubsingleton` 📖	mathematical	—	`CategoryTheory.Functor.FullyFaithful`	—	`faithful` `CategoryTheory.Functor.map_injective`
`isIso_of_isIso_map` 📖	mathematical	—	`CategoryTheory.IsIso`	—	`preimage_map` `CategoryTheory.Iso.isIso_hom`
`isoEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Iso` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `isoEquiv` `CategoryTheory.Functor.mapIso`	—	—
`isoEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Iso` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `isoEquiv` `preimageIso`	—	—
`map_bijective` 📖	mathematical	—	`Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`Equiv.bijective`
`map_injective` 📖	—	`CategoryTheory.Functor.map`	—	—	`Equiv.injective`
`map_preimage` 📖	mathematical	—	`CategoryTheory.Functor.map` `preimage`	—	—
`map_surjective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`Equiv.surjective`
`nonempty_iff_map_bijective` 📖	mathematical	—	`CategoryTheory.Functor.FullyFaithful` `Function.Bijective` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`map_bijective` `Function.Bijective.injective` `Function.Bijective.surjective`
`preimageIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `preimageIso` `preimage` `CategoryTheory.Functor.obj`	—	—
`preimageIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `preimageIso` `preimage` `CategoryTheory.Functor.obj`	—	—
`preimage_comp` 📖	mathematical	—	`preimage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`map_injective` `map_preimage` `CategoryTheory.Functor.map_comp`
`preimage_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `preimage` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `preimage_comp`
`preimage_id` 📖	mathematical	—	`preimage` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`map_injective` `map_preimage` `CategoryTheory.Functor.map_id`
`preimage_map` 📖	mathematical	—	`preimage` `CategoryTheory.Functor.map`	—	—

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithful_of_comp` 📖	mathematical	—	`CategoryTheory.Functor.Faithful`	—	`CategoryTheory.Functor.Faithful.of_comp_iso`

Eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithful_of_comp` 📖	mathematical	`CategoryTheory.Functor.comp`	`CategoryTheory.Functor.Faithful`	—	`CategoryTheory.Functor.Faithful.of_comp_eq`

---

← Back to Index