Localization

📁 Source: Mathlib/CategoryTheory/Abelian/SerreClass/Localization.lean

Statistics

Metric	Count
Definitions abelian, fullyFaithfulWhiskeringLeft, whiskeringLeft	3
Theorems epi_iff, epi_map_iff, epi_map_tfae, essImage_whiskeringLeft, exactFunctor_comp_iff, hasBinaryProducts, hasCoequalizers, hasCokernels, hasEqualizers, hasFiniteProducts, hasKernels, hasZeroObject, instFaithfulExactFunctorWhiskeringLeft, instFullExactFunctorWhiskeringLeft, instHasLeftCalculusOfFractionsIsoModSerre, instHasRightCalculusOfFractionsIsoModSerre, inverseImage_epimorphisms, inverseImage_isomorphisms, inverseImage_monomorphisms, isIso_map_iff, isNormalEpiCategory, isNormalMonoCategory, isZero_obj_iff, map_comp_eq_zero_iff_of_epi_mono, map_eq_zero_iff, mono_iff, mono_map_iff, mono_map_tfae, preservesCokernel, preservesEpimorphisms, preservesFiniteColimits, preservesFiniteColimits_comp_iff, preservesFiniteLimits, preservesFiniteLimits_comp_iff, preservesKernel, preservesMonomorphisms, whiskeringLeft_obj_obj, isoModSerre_image_ι, exists_comp_isoModSerre_eq_zero_iff, exists_comp_monoModSerre_eq_zero_iff, exists_epiModSerre_comp_eq_zero_iff, exists_isoModSerre_comp_eq_zero_iff, isoModSerre_factorThruImage	43
Total	46

CategoryTheory.ObjectProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_comp_isoModSerre_eq_zero_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct isoModSerre CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.image CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels exists_comp_monoModSerre_eq_zero_iff isoModSerre_iff_of_epi CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Limits.cokernel.condition
exists_comp_monoModSerre_eq_zero_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct monoModSerre CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.image CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels prop_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeMonoModSerre monoModSerre_of_mono CategoryTheory.Abelian.instMonoFactorThruCoimage monoModSerre_zero_iff CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.cokernel.π_desc_assoc CategoryTheory.Limits.comp_zero CategoryTheory.Limits.cokernel.condition
exists_epiModSerre_comp_eq_zero_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct epiModSerre CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.image CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeEpiModSerre epiModSerre_of_epi CategoryTheory.Abelian.instEpiFactorThruImage epiModSerre_zero_iff CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp prop_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.kernel.condition
exists_isoModSerre_comp_eq_zero_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct isoModSerre CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.image CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels exists_epiModSerre_comp_eq_zero_iff CategoryTheory.Limits.equalizer.ι_mono prop_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.kernel.condition

CategoryTheory.ObjectProperty.SerreClassLocalization

Definitions

Name	Category	Theorems
abelian 📖	CompOp	—
fullyFaithfulWhiskeringLeft 📖	CompOp	—
whiskeringLeft 📖	CompOp	4 math math: instFaithfulExactFunctorWhiskeringLeft, whiskeringLeft_obj_obj, instFullExactFunctorWhiskeringLeft, essImage_whiskeringLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff 📖	mathematical	—	CategoryTheory.Epi Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	preservesEpimorphisms CategoryTheory.Localization.essSurj_mapArrow instHasLeftCalculusOfFractionsIsoModSerre CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.Localization.inverts CategoryTheory.ObjectProperty.epiModSerre.isoModSerre_image_ι epi_map_iff CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition CategoryTheory.MorphismProperty.arrow_iso_iff CategoryTheory.MorphismProperty.RespectsIso.epimorphisms CategoryTheory.MorphismProperty.epimorphisms.infer_property CategoryTheory.MorphismProperty.arrow_mk_iso_iff
epi_map_iff 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.ObjectProperty.epiModSerre	—	List.TFAE.out epi_map_tfae
epi_map_tfae 📖	mathematical	—	List.TFAE CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.ObjectProperty.epiModSerre	—	CategoryTheory.Localization.essSurj CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.cancel_epi CategoryTheory.Limits.comp_zero CategoryTheory.Functor.map_comp CategoryTheory.Limits.cokernel.condition CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id map_comp_eq_zero_iff_of_epi_mono CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.instMonoId CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels map_eq_zero_iff CategoryTheory.ObjectProperty.exists_epiModSerre_comp_eq_zero_iff CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition CategoryTheory.ObjectProperty.instIsMultiplicativeEpiModSerre CategoryTheory.Category.assoc CategoryTheory.Preadditive.epi_iff_cancel_zero CategoryTheory.Localization.inverts CategoryTheory.Localization.exists_leftFraction instHasLeftCalculusOfFractionsIsoModSerre CategoryTheory.MorphismProperty.LeftFraction.hs CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.zero_comp CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s Mathlib.Tactic.Reassoc.eq_whisker' List.tfae_of_cycle
essImage_whiskeringLeft 📖	mathematical	—	CategoryTheory.Functor.essImage CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.exactFunctor whiskeringLeft CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso CategoryTheory.MorphismProperty.IsInvertedBy.of_comp CategoryTheory.Localization.inverts exactFunctor_comp_iff CategoryTheory.ObjectProperty.prop_of_iso CategoryTheory.instIsClosedUnderIsomorphismsFunctorExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.property
exactFunctor_comp_iff 📖	mathematical	—	CategoryTheory.exactFunctor CategoryTheory.Functor.comp	—	preservesFiniteLimits_comp_iff preservesFiniteColimits_comp_iff
hasBinaryProducts 📖	mathematical	—	CategoryTheory.Limits.HasBinaryProducts	—	CategoryTheory.Localization.essSurj CategoryTheory.Limits.hasLimit_of_iso CategoryTheory.Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Functor.preservesFiniteProductsOfAdditive CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair
hasCoequalizers 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizers	—	hasCokernels CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
hasCokernels 📖	mathematical	—	CategoryTheory.Limits.HasCokernels CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Functor.EssSurj.mem_essImage CategoryTheory.Localization.essSurj_mapArrow instHasLeftCalculusOfFractionsIsoModSerre preservesCokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.hasColimit_of_iso CategoryTheory.Arrow.w_mk_right CategoryTheory.Limits.comp_zero
hasEqualizers 📖	mathematical	—	CategoryTheory.Limits.HasEqualizers	—	hasKernels CategoryTheory.Preadditive.hasEqualizer_of_hasKernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
hasFiniteProducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteProducts	—	hasZeroObject hasBinaryProducts CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal CategoryTheory.Limits.HasZeroObject.hasTerminal
hasKernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Functor.EssSurj.mem_essImage CategoryTheory.Localization.essSurj_mapArrow instHasLeftCalculusOfFractionsIsoModSerre preservesKernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.hasLimit_of_iso CategoryTheory.Arrow.w_mk_right CategoryTheory.Limits.zero_comp
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject	—	CategoryTheory.Abelian.hasZeroObject isZero_obj_iff CategoryTheory.ObjectProperty.prop_zero CategoryTheory.ObjectProperty.IsSerreClass.toContainsZero CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderQuotients
instFaithfulExactFunctorWhiskeringLeft 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.exactFunctor whiskeringLeft	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullExactFunctorWhiskeringLeft 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.exactFunctor whiskeringLeft	—	CategoryTheory.Functor.FullyFaithful.full
instHasLeftCalculusOfFractionsIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions CategoryTheory.ObjectProperty.isoModSerre	—	CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.MorphismProperty.pushout_inl CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeIsoModSerre CategoryTheory.MorphismProperty.RightFraction.hs CategoryTheory.Limits.pushout.condition CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff CategoryTheory.Preadditive.comp_sub CategoryTheory.Preadditive.sub_comp CategoryTheory.Limits.cokernel.condition
instHasRightCalculusOfFractionsIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.HasRightCalculusOfFractions CategoryTheory.ObjectProperty.isoModSerre	—	CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.MorphismProperty.pullback_fst CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeIsoModSerre CategoryTheory.MorphismProperty.LeftFraction.hs CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.ObjectProperty.prop_of_iso CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff CategoryTheory.Preadditive.sub_comp CategoryTheory.Preadditive.comp_sub CategoryTheory.Limits.kernel.condition
inverseImage_epimorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.epimorphisms CategoryTheory.ObjectProperty.epiModSerre	—	CategoryTheory.MorphismProperty.ext epi_map_iff
inverseImage_isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.ObjectProperty.isoModSerre	—	CategoryTheory.MorphismProperty.ext isIso_map_iff
inverseImage_monomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.inverseImage CategoryTheory.MorphismProperty.monomorphisms CategoryTheory.ObjectProperty.monoModSerre	—	CategoryTheory.MorphismProperty.ext mono_map_iff
isIso_map_iff 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.ObjectProperty.isoModSerre	—	CategoryTheory.isIso_iff_mono_and_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory mono_map_iff epi_map_iff CategoryTheory.ObjectProperty.isoModSerre_iff
isNormalEpiCategory 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	epi_iff CategoryTheory.Abelian.toIsNormalEpiCategory preservesCokernel CategoryTheory.Functor.map_comp CategoryTheory.NormalEpi.w CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive
isNormalMonoCategory 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mono_iff CategoryTheory.Abelian.toIsNormalMonoCategory preservesKernel CategoryTheory.Functor.map_comp CategoryTheory.NormalMono.w CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive
isZero_obj_iff 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.MorphismProperty.map_eq_iff_precomp instHasRightCalculusOfFractionsIsoModSerre CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero
map_comp_eq_zero_iff_of_epi_mono 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Functor.map_comp CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels map_eq_zero_iff CategoryTheory.strongEpi_of_epi CategoryTheory.strongEpiCategory_of_regularEpiCategory CategoryTheory.regularEpiCategoryOfNormalEpiCategory CategoryTheory.Abelian.toIsNormalEpiCategory CategoryTheory.ObjectProperty.prop_iff_of_iso CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations
map_eq_zero_iff 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.image CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.MorphismProperty.map_eq_iff_precomp instHasRightCalculusOfFractionsIsoModSerre CategoryTheory.Limits.comp_zero CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff
mono_iff 📖	mathematical	—	CategoryTheory.Mono Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	preservesMonomorphisms CategoryTheory.Localization.essSurj_mapArrow instHasLeftCalculusOfFractionsIsoModSerre CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Localization.inverts CategoryTheory.ObjectProperty.monoModSerre.isoModSerre_factorThruImage mono_map_iff CategoryTheory.Functor.map_comp CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition CategoryTheory.Category.comp_id CategoryTheory.MorphismProperty.arrow_iso_iff CategoryTheory.MorphismProperty.RespectsIso.monomorphisms CategoryTheory.MorphismProperty.monomorphisms.infer_property CategoryTheory.MorphismProperty.arrow_mk_iso_iff
mono_map_iff 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.ObjectProperty.monoModSerre	—	List.TFAE.out mono_map_tfae
mono_map_tfae 📖	mathematical	—	List.TFAE CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.ObjectProperty.monoModSerre	—	CategoryTheory.Localization.essSurj CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.cancel_mono CategoryTheory.Limits.zero_comp CategoryTheory.Functor.map_comp CategoryTheory.Limits.kernel.condition CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_id CategoryTheory.Limits.comp_zero map_comp_eq_zero_iff_of_epi_mono CategoryTheory.instEpiId CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels map_eq_zero_iff CategoryTheory.ObjectProperty.exists_comp_monoModSerre_eq_zero_iff CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition CategoryTheory.ObjectProperty.instIsMultiplicativeMonoModSerre CategoryTheory.Category.assoc CategoryTheory.Preadditive.mono_iff_cancel_zero CategoryTheory.Localization.inverts CategoryTheory.Localization.exists_rightFraction instHasRightCalculusOfFractionsIsoModSerre CategoryTheory.MorphismProperty.RightFraction.hs CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map List.tfae_of_cycle
preservesCokernel 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesEpimorphisms CategoryTheory.Localization.essSurj CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp map_eq_zero_iff CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff CategoryTheory.Localization.inverts CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.Limits.cokernel.π_desc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Localization.exists_leftFraction instHasLeftCalculusOfFractionsIsoModSerre CategoryTheory.MorphismProperty.LeftFraction.hs CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.cokernel.condition CategoryTheory.Functor.preservesZeroMorphisms_of_additive existsUnique_of_exists_of_unique CategoryTheory.Limits.CokernelCofork.condition CategoryTheory.Functor.map_epi CategoryTheory.Limits.coequalizer.π_epi
preservesEpimorphisms 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms	—	epi_map_iff CategoryTheory.ObjectProperty.epiModSerre_of_epi
preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits	—	List.TFAE.out CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.preservesFiniteColimits_tfae preservesCokernel
preservesFiniteColimits_comp_iff 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Functor.comp	—	preservesFiniteColimits CategoryTheory.Localization.functor_additive_iff instHasLeftCalculusOfFractionsIsoModSerre CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts CategoryTheory.Functor.additive_of_preservesBinaryBiproducts CategoryTheory.Abelian.hasBinaryBiproducts List.TFAE.out CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.preservesFiniteColimits_tfae CategoryTheory.Functor.EssSurj.mem_essImage CategoryTheory.Localization.essSurj_mapArrow CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Limits.preservesColimit_of_iso_diagram CategoryTheory.Arrow.w_mk_right CategoryTheory.Limits.comp_zero CategoryTheory.Limits.comp_preservesFiniteColimits
preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits	—	List.TFAE.out CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.preservesFiniteLimits_tfae preservesKernel
preservesFiniteLimits_comp_iff 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor.comp	—	preservesFiniteLimits CategoryTheory.Localization.functor_additive_iff instHasLeftCalculusOfFractionsIsoModSerre CategoryTheory.Functor.additive_of_preserves_binary_products CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Abelian.has_finite_products Finite.of_fintype CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit List.TFAE.out CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.preservesFiniteLimits_tfae CategoryTheory.Functor.EssSurj.mem_essImage CategoryTheory.Localization.essSurj_mapArrow CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Limits.preservesLimit_of_iso_diagram CategoryTheory.Arrow.w_mk_right CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_preservesFiniteLimits
preservesKernel 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesMonomorphisms CategoryTheory.Localization.essSurj CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp map_eq_zero_iff CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff CategoryTheory.Localization.inverts CategoryTheory.Category.assoc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Localization.exists_rightFraction instHasRightCalculusOfFractionsIsoModSerre CategoryTheory.MorphismProperty.RightFraction.hs CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Limits.comp_zero CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.kernel.condition CategoryTheory.Functor.preservesZeroMorphisms_of_additive existsUnique_of_exists_of_unique CategoryTheory.Limits.KernelFork.condition CategoryTheory.Functor.map_mono CategoryTheory.Limits.equalizer.ι_mono
preservesMonomorphisms 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms	—	mono_map_iff CategoryTheory.ObjectProperty.monoModSerre_of_mono
whiskeringLeft_obj_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.exactFunctor CategoryTheory.Functor.obj CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category whiskeringLeft CategoryTheory.Functor.comp	—	—

CategoryTheory.ObjectProperty.epiModSerre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isoModSerre_image_ι 📖	mathematical	CategoryTheory.ObjectProperty.epiModSerre	CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.image.ι	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.ObjectProperty.prop_of_iso CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Category.comp_id CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.instIsIsoMapOfEpi CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.IsIso.id

CategoryTheory.ObjectProperty.monoModSerre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isoModSerre_factorThruImage 📖	mathematical	CategoryTheory.ObjectProperty.monoModSerre	CategoryTheory.ObjectProperty.isoModSerre CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.factorThruImage	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.ObjectProperty.prop_of_iso CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition CategoryTheory.Category.id_comp CategoryTheory.Limits.instIsIsoMapOfMono CategoryTheory.IsIso.id CategoryTheory.Limits.equalizer.ι_mono

---

← Back to Index