EpiMono

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

Statistics

Metric	Count
Definitions `PreservesEpimorphisms`, `PreservesMonomorphisms`, `ReflectsEpimorphisms`, `ReflectsMonomorphisms`, `splitEpiEquiv`, `splitMonoEquiv`	6
Theorems `instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms`, `strongEpi_map_of_isEquivalence`, `strongEpi_map_of_strongEpi`, `preserves`, `preserves`, `reflects`, `reflects`, `epi_map_iff_epi`, `epi_of_epi_map`, `instIsSplitEpiApp`, `instIsSplitMonoApp`, `isSplitEpi_iff`, `isSplitMono_iff`, `map_epi`, `map_mono`, `mono_map_iff_mono`, `mono_of_mono_map`, `iso_iff`, `ofRetract`, `of_iso`, `of_natTrans`, `preservesEpimorphisms_comp`, `preservesEpimorphisms_of_adjunction`, `preservesEpimorphisms_of_isLeftAdjoint`, `preservesEpimorphisms_of_preserves_of_reflects`, `iso_iff`, `ofRetract`, `of_iso`, `of_natTrans`, `preservesMonomorphisms_comp`, `preservesMonomorphisms_of_adjunction`, `preservesMonomorphisms_of_isRightAdjoint`, `preservesMonomorphisms_of_preserves_of_reflects`, `iso_iff`, `of_iso`, `reflectsEpimorphisms_comp`, `reflectsEpimorphisms_of_faithful`, `reflectsEpimorphisms_of_preserves_of_reflects`, `iso_iff`, `of_iso`, `reflectsMonomorphisms_comp`, `reflectsMonomorphisms_of_faithful`, `reflectsMonomorphisms_of_preserves_of_reflects`, `splitEpiCategoryImpOfIsEquivalence`, `strongEpi_map_iff_strongEpi_of_isEquivalence`	45
Total	51

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.mono_of_mono_fac` `Equiv.symm_apply_apply` `homEquiv_counit`
`strongEpi_map_of_isEquivalence` 📖	mathematical	—	`CategoryTheory.StrongEpi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`strongEpi_map_of_strongEpi` `CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor`
`strongEpi_map_of_strongEpi` 📖	mathematical	—	`CategoryTheory.StrongEpi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.map_epi` `CategoryTheory.epi_of_strongEpi` `hasLiftingProperty_iff` `CategoryTheory.StrongEpi.llp` `CategoryTheory.Functor.map_mono`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`PreservesEpimorphisms` 📖	CompData	38 math math: `preservesEpimorphisms_of_map_exact`, `AddGrpCat.forget_grp_preserves_epi`, `preservesEpimorphisms_of_preserves_of_reflects`, `preservesEpimorphisms.of_iso`, `preservesEpimorphisms_of_preserves_shortExact_right`, `LightCondMod.instPreservesEpimorphismsLightCondSetForget`, `ModuleCat.forget_preservesEpimorphisms`, `instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet`, `instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed`, `preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects`, `preservesEpimorphisms.of_natTrans`, `instPreservesEpimorphisms`, `preservesEpimorphisms_of_isLeftAdjoint`, `AddCommGrpCat.forget_commGrp_preserves_epi`, `LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite`, `CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj`, `preservesEpimorphisms.iso_iff`, `CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj'`, `LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim`, `CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj`, `CategoryTheory.ConcreteCategory.forget₂_preservesEpimorphisms`, `preservesEpimorphisms_comp`, `CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj`, `preservesEpimorphisms.ofRetract`, `CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff`, `GrpCat.forget_grp_preserves_epi`, `preservesEpimorphisms_of_adjunction`, `CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape`, `CategoryTheory.ShortComplex.preservesEpimorphisms_π₂`, `CategoryTheory.InternallyProjective.preserves_epi`, `Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype`, `CommGrpCat.forget_commGrp_preserves_epi`, `CategoryTheory.ShortComplex.preservesEpimorphisms_π₁`, `CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj`, `CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj`, `CategoryTheory.Idempotents.instPreservesEpimorphismsKaroubiToKaroubi`, `CategoryTheory.ShortComplex.preservesEpimorphisms_π₃`, `CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis`
`PreservesMonomorphisms` 📖	CompData	29 math math: `ModuleCat.instPreservesMonomorphismsRestrictScalars`, `CategoryTheory.Limits.instPreservesMonomorphismsObjFunctorTypeSigmaConst`, `AddCommGrpCat.instPreservesMonomorphismsFree`, `preservesMonomorphisms.of_iso`, `ModuleCat.forget_preservesMonomorphisms`, `AddGrpCat.forget_grp_preserves_mono`, `CommGrpCat.forget_commGrp_preserves_mono`, `preservesMonomorphisms_of_preserves_of_reflects`, `preservesMonomorphisms_comp`, `preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects`, `instPreservesMonomorphisms`, `preservesMonomorphisms_of_preserves_shortExact_left`, `AddCommGrpCat.forget_commGrp_preserves_mono`, `preservesMonomorphisms_of_isRightAdjoint`, `preservesMonomorphisms_of_adjunction`, `CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff`, `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape`, `CategoryTheory.ShortComplex.preservesMonomorphisms_π₁`, `preservesMonomorphisms.of_natTrans`, `CategoryTheory.ShortComplex.preservesMonomorphisms_π₂`, `TopCat.Presheaf.stalkFunctor_preserves_mono`, `CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction`, `CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms`, `CategoryTheory.Idempotents.instPreservesMonomorphismsKaroubiToKaroubi`, `preservesMonomorphisms_of_map_exact`, `preservesMonomorphisms.ofRetract`, `GrpCat.forget_grp_preserves_mono`, `preservesMonomorphisms.iso_iff`, `CategoryTheory.ShortComplex.preservesMonomorphisms_π₃`
`ReflectsEpimorphisms` 📖	CompData	7 math math: `LightCondMod.instReflectsEpimorphismsLightCondSetForget`, `reflectsEpimorphisms.iso_iff`, `reflectsEpimorphisms_of_faithful`, `CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape`, `reflectsEpimorphisms_of_preserves_of_reflects`, `reflectsEpimorphisms.of_iso`, `reflectsEpimorphisms_comp`
`ReflectsMonomorphisms` 📖	CompData	8 math math: `reflectsMonomorphisms.iso_iff`, `CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCat`, `reflectsMonomorphisms_of_faithful`, `CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape`, `reflectsMonomorphisms.of_iso`, `reflectsMonomorphisms_comp`, `reflectsMonomorphisms_of_preserves_of_reflects`, `CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction`
`splitEpiEquiv` 📖	CompOp	—
`splitMonoEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_map_iff_epi` 📖	mathematical	—	`CategoryTheory.Epi` `obj` `map`	—	`epi_of_epi_map` `map_epi`
`epi_of_epi_map` 📖	mathematical	—	`CategoryTheory.Epi`	—	`ReflectsEpimorphisms.reflects`
`instIsSplitEpiApp` 📖	mathematical	—	`CategoryTheory.IsSplitEpi` `obj` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.instIsSplitEpiMap`
`instIsSplitMonoApp` 📖	mathematical	—	`CategoryTheory.IsSplitMono` `obj` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.instIsSplitMonoMap`
`isSplitEpi_iff` 📖	mathematical	—	`CategoryTheory.IsSplitEpi` `obj` `map`	—	`CategoryTheory.IsSplitEpi.mk'` `CategoryTheory.IsSplitEpi.exists_splitEpi`
`isSplitMono_iff` 📖	mathematical	—	`CategoryTheory.IsSplitMono` `obj` `map`	—	`CategoryTheory.IsSplitMono.mk'` `CategoryTheory.IsSplitMono.exists_splitMono`
`map_epi` 📖	mathematical	—	`CategoryTheory.Epi` `obj` `map`	—	`PreservesEpimorphisms.preserves`
`map_mono` 📖	mathematical	—	`CategoryTheory.Mono` `obj` `map`	—	`PreservesMonomorphisms.preserves`
`mono_map_iff_mono` 📖	mathematical	—	`CategoryTheory.Mono` `obj` `map`	—	`mono_of_mono_map` `map_mono`
`mono_of_mono_map` 📖	mathematical	—	`CategoryTheory.Mono`	—	`ReflectsMonomorphisms.reflects`
`preservesEpimorphisms_comp` 📖	mathematical	—	`PreservesEpimorphisms` `comp`	—	`comp_map` `map_epi`
`preservesEpimorphisms_of_adjunction` 📖	mathematical	—	`PreservesEpimorphisms`	—	`Equiv.apply_eq_iff_eq` `CategoryTheory.cancel_epi` `CategoryTheory.Adjunction.homEquiv_naturality_left`
`preservesEpimorphisms_of_isLeftAdjoint` 📖	mathematical	—	`PreservesEpimorphisms`	—	`preservesEpimorphisms_of_adjunction`
`preservesEpimorphisms_of_preserves_of_reflects` 📖	mathematical	—	`PreservesEpimorphisms`	—	`epi_of_epi_map` `map_epi`
`preservesMonomorphisms_comp` 📖	mathematical	—	`PreservesMonomorphisms` `comp`	—	`comp_map` `map_mono`
`preservesMonomorphisms_of_adjunction` 📖	mathematical	—	`PreservesMonomorphisms`	—	`Equiv.apply_eq_iff_eq` `CategoryTheory.cancel_mono` `CategoryTheory.Adjunction.homEquiv_naturality_right_symm`
`preservesMonomorphisms_of_isRightAdjoint` 📖	mathematical	—	`PreservesMonomorphisms`	—	`preservesMonomorphisms_of_adjunction`
`preservesMonomorphisms_of_preserves_of_reflects` 📖	mathematical	—	`PreservesMonomorphisms`	—	`mono_of_mono_map` `map_mono`
`reflectsEpimorphisms_comp` 📖	mathematical	—	`ReflectsEpimorphisms` `comp`	—	`epi_of_epi_map`
`reflectsEpimorphisms_of_faithful` 📖	mathematical	—	`ReflectsEpimorphisms`	—	`map_injective` `CategoryTheory.cancel_epi` `map_comp`
`reflectsEpimorphisms_of_preserves_of_reflects` 📖	mathematical	—	`ReflectsEpimorphisms`	—	`epi_of_epi_map` `map_epi`
`reflectsMonomorphisms_comp` 📖	mathematical	—	`ReflectsMonomorphisms` `comp`	—	`mono_of_mono_map`
`reflectsMonomorphisms_of_faithful` 📖	mathematical	—	`ReflectsMonomorphisms`	—	`map_injective` `CategoryTheory.cancel_mono` `map_comp`
`reflectsMonomorphisms_of_preserves_of_reflects` 📖	mathematical	—	`ReflectsMonomorphisms`	—	`mono_of_mono_map` `map_mono`
`splitEpiCategoryImpOfIsEquivalence` 📖	mathematical	—	`CategoryTheory.SplitEpiCategory`	—	`isSplitEpi_iff` `IsEquivalence.full` `isEquivalence_inv` `IsEquivalence.faithful` `CategoryTheory.isSplitEpi_of_epi` `map_epi` `preservesEpimorphisms_of_isLeftAdjoint` `isLeftAdjoint_of_isEquivalence`
`strongEpi_map_iff_strongEpi_of_isEquivalence` 📖	mathematical	—	`CategoryTheory.StrongEpi` `obj` `map`	—	`CategoryTheory.StrongEpi.iff_of_arrow_iso` `CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence` `isEquivalence_inv`

CategoryTheory.Functor.PreservesEpimorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preserves` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	—

CategoryTheory.Functor.PreservesMonomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preserves` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	—

CategoryTheory.Functor.ReflectsEpimorphisms

Theorems

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

CategoryTheory.Functor.ReflectsMonomorphisms

Theorems

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

CategoryTheory.Functor.preservesEpimorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_iff` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms`	—	`of_iso`
`ofRetract` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms`	—	`CategoryTheory.Functor.PreservesEpimorphisms.preserves` `of_natTrans` `CategoryTheory.IsSplitEpi.epi` `CategoryTheory.Functor.instIsSplitEpiApp` `CategoryTheory.Retract.instIsSplitEpiR`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms`	—	`of_natTrans` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.NatIso.hom_app_isIso`
`of_natTrans` 📖	mathematical	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app`	`CategoryTheory.Functor.PreservesEpimorphisms`	—	`CategoryTheory.NatTrans.naturality` `CategoryTheory.epi_comp` `CategoryTheory.Functor.map_epi` `CategoryTheory.epi_of_epi`

CategoryTheory.Functor.preservesMonomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_iff` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms`	—	`of_iso`
`ofRetract` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms`	—	`CategoryTheory.Functor.PreservesMonomorphisms.preserves` `of_natTrans` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.Functor.instIsSplitMonoApp` `CategoryTheory.Retract.instIsSplitMonoI`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms`	—	`of_natTrans` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.inv_app_isIso`
`of_natTrans` 📖	mathematical	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app`	`CategoryTheory.Functor.PreservesMonomorphisms`	—	`CategoryTheory.NatTrans.naturality` `CategoryTheory.mono_comp` `CategoryTheory.Functor.map_mono` `CategoryTheory.mono_of_mono`

CategoryTheory.Functor.reflectsEpimorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_iff` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsEpimorphisms`	—	`of_iso`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsEpimorphisms`	—	`CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.eq_comp_inv` `CategoryTheory.Iso.app_hom` `CategoryTheory.NatTrans.naturality` `CategoryTheory.epi_comp` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.isIso_inv`

CategoryTheory.Functor.reflectsMonomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_iff` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsMonomorphisms`	—	`of_iso`
`of_iso` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsMonomorphisms`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.eq_comp_inv` `CategoryTheory.Iso.app_hom` `CategoryTheory.NatTrans.naturality` `CategoryTheory.mono_comp` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.isIso_inv`

---

← Back to Index