EpiMono

📁 Source: Mathlib/Algebra/Category/ModuleCat/Presheaf/EpiMono.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_iff_surjective, epi_of_surjective, injective_of_mono, instEpiModuleCatCarrierObjOppositeRingCatApp, instMonoModuleCatCarrierObjOppositeRingCatApp, mono_iff_surjective, mono_of_injective, surjective_of_epi	8
Total	8

PresheafOfModules

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_surjective 📖	mathematical	—	CategoryTheory.Epi PresheafOfModules instCategory ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring obj DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	—	surjective_of_epi epi_of_surjective
epi_of_surjective 📖	mathematical	ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring obj DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	CategoryTheory.Epi PresheafOfModules instCategory	—	hom_ext ModuleCat.hom_ext LinearMap.ext CategoryTheory.Functor.congr_map
injective_of_mono 📖	mathematical	—	ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring obj DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	—	ModuleCat.mono_iff_injective instMonoModuleCatCarrierObjOppositeRingCatApp
instEpiModuleCatCarrierObjOppositeRingCatApp 📖	mathematical	—	CategoryTheory.Epi ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj Hom.app	—	CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape evaluation_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits AddCommGrpCat.hasColimitsOfSize UnivLE.self
instMonoModuleCatCarrierObjOppositeRingCatApp 📖	mathematical	—	CategoryTheory.Mono ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj Hom.app	—	CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation UnivLE.small univLE_of_max UnivLE.self
mono_iff_surjective 📖	mathematical	—	CategoryTheory.Mono PresheafOfModules instCategory ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring obj DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	—	injective_of_mono mono_of_injective
mono_of_injective 📖	mathematical	ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring obj DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	CategoryTheory.Mono PresheafOfModules instCategory	—	hom_ext ModuleCat.hom_ext LinearMap.ext CategoryTheory.Functor.congr_map
surjective_of_epi 📖	mathematical	—	ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring obj DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	—	ModuleCat.epi_iff_surjective instEpiModuleCatCarrierObjOppositeRingCatApp

---

← Back to Index