MorphismProperty

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

Statistics

Metric	Count
Definitions epiModSerre, isoModSerre, monoModSerre	3
Theorems epiModSerre_iff, epiModSerre_of_epi, epiModSerre_zero_iff, epimorphisms_le_epiModSerre, instHasTwoOutOfThreePropertyIsoModSerre, instIsMultiplicativeEpiModSerre, instIsMultiplicativeIsoModSerre, instIsMultiplicativeMonoModSerre, instIsStableUnderBaseChangeEpiModSerre, instIsStableUnderBaseChangeIsoModSerre, instIsStableUnderBaseChangeMonoModSerre, instIsStableUnderCobaseChangeEpiModSerre, instIsStableUnderCobaseChangeIsoModSerre, instIsStableUnderCobaseChangeMonoModSerre, instIsStableUnderRetractsEpiModSerre, instIsStableUnderRetractsIsoModSerre, instIsStableUnderRetractsMonoModSerre, isoModSerre_iff, isoModSerre_iff_of_epi, isoModSerre_iff_of_mono, isoModSerre_isInvertedBy_iff, isoModSerre_of_epi, isoModSerre_of_isIso, isoModSerre_of_mono, isoModSerre_zero_iff, isomorphisms_le_isoModSerre, le_kernel_of_isoModSerre_isInvertedBy, monoModSerre_iff, monoModSerre_of_mono, monoModSerre_zero_iff, monomorphisms_le_monoModSerre	31
Total	34

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
epiModSerre 📖	CompOp	10 math math: instIsStableUnderCobaseChangeEpiModSerre, epiModSerre_of_epi, epiModSerre_zero_iff, instIsStableUnderRetractsEpiModSerre, epimorphisms_le_epiModSerre, epiModSerre_iff, instIsStableUnderBaseChangeEpiModSerre, isoModSerre_iff, isoModSerre_iff_of_mono, instIsMultiplicativeEpiModSerre
isoModSerre 📖	CompOp	18 math math: isoModSerre_isInvertedBy_iff, isoModSerre_zero_iff, instIsStableUnderRetractsIsoModSerre, isoModSerre_of_isIso, isomorphisms_le_isoModSerre, CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint, instIsMultiplicativeIsoModSerre, isoModSerre_of_mono, instHasTwoOutOfThreePropertyIsoModSerre, instIsStableUnderBaseChangeIsoModSerre, CategoryTheory.Abelian.isoModSerre_kernel_eq_leftBousfield_W_of_rightAdjoint, isoModSerre_iff_of_epi, isoModSerre_iff, CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint, isoModSerre_iff_of_mono, instIsStableUnderCobaseChangeIsoModSerre, CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms, isoModSerre_of_epi
monoModSerre 📖	CompOp	10 math math: monoModSerre_of_mono, instIsMultiplicativeMonoModSerre, instIsStableUnderBaseChangeMonoModSerre, monoModSerre_zero_iff, monoModSerre_iff, instIsStableUnderRetractsMonoModSerre, instIsStableUnderCobaseChangeMonoModSerre, monomorphisms_le_monoModSerre, isoModSerre_iff_of_epi, isoModSerre_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epiModSerre_iff 📖	mathematical	—	epiModSerre CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels	—	—
epiModSerre_of_epi 📖	mathematical	—	epiModSerre	—	epimorphisms_le_epiModSerre CategoryTheory.MorphismProperty.epimorphisms.infer_property
epiModSerre_zero_iff 📖	mathematical	—	epiModSerre Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	prop_iff_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients
epimorphisms_le_epiModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.epimorphisms epiModSerre	—	prop_of_isZero IsSerreClass.toContainsZero instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.isZero_cokernel_of_epi CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels
instHasTwoOutOfThreePropertyIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty isoModSerre	—	CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeIsoModSerre prop_of_mono IsSerreClass.toIsClosedUnderSubobjects CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.id_comp CategoryTheory.Limits.kernel.lift_mono CategoryTheory.mono_comp CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.instMonoId prop_X₂_of_exact CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.kernelCokernelCompSequence_exact CategoryTheory.ComposableArrows.Exact.exact prop_of_epi IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Category.comp_id CategoryTheory.Limits.cokernel.desc_epi CategoryTheory.epi_comp CategoryTheory.instEpiId CategoryTheory.Limits.coequalizer.π_epi
instIsMultiplicativeEpiModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative epiModSerre	—	epiModSerre_of_epi CategoryTheory.instEpiId prop_X₂_of_exact CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.kernelCokernelCompSequence_exact CategoryTheory.ComposableArrows.Exact.exact
instIsMultiplicativeIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative isoModSerre	—	CategoryTheory.MorphismProperty.IsMultiplicative.inf instIsMultiplicativeMonoModSerre instIsMultiplicativeEpiModSerre
instIsMultiplicativeMonoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative monoModSerre	—	monoModSerre_of_mono CategoryTheory.instMonoId prop_X₂_of_exact CategoryTheory.ComposableArrows.Exact.toIsComplex CategoryTheory.kernelCokernelCompSequence_exact CategoryTheory.ComposableArrows.Exact.exact
instIsStableUnderBaseChangeEpiModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange epiModSerre	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.flip CategoryTheory.Abelian.mono_cokernel_map_of_isPullback prop_of_mono IsSerreClass.toIsClosedUnderSubobjects
instIsStableUnderBaseChangeIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange isoModSerre	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf instIsStableUnderBaseChangeMonoModSerre instIsStableUnderBaseChangeEpiModSerre
instIsStableUnderBaseChangeMonoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange monoModSerre	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.flip CategoryTheory.Limits.isIso_kernel_map_of_isPullback prop_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients
instIsStableUnderCobaseChangeEpiModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange epiModSerre	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.CommSq.w CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPushout.flip CategoryTheory.Limits.isIso_cokernel_map_of_isPushout prop_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients
instIsStableUnderCobaseChangeIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange isoModSerre	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.inf instIsStableUnderCobaseChangeMonoModSerre instIsStableUnderCobaseChangeEpiModSerre
instIsStableUnderCobaseChangeMonoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange monoModSerre	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.CommSq.w CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPushout.flip CategoryTheory.Abelian.epi_kernel_map_of_isPushout prop_of_epi IsSerreClass.toIsClosedUnderQuotients
instIsStableUnderRetractsEpiModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts epiModSerre	—	prop_of_epi IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Arrow.w_mk_right CategoryTheory.Limits.cokernel.desc_epi CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsRegularEpi CategoryTheory.instIsRegularEpiOfIsSplitEpi CategoryTheory.Retract.instIsSplitEpiR CategoryTheory.Limits.coequalizer.π_epi
instIsStableUnderRetractsIsoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts isoModSerre	—	CategoryTheory.MorphismProperty.instIsStableUnderRetractsMin instIsStableUnderRetractsMonoModSerre instIsStableUnderRetractsEpiModSerre
instIsStableUnderRetractsMonoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts monoModSerre	—	prop_of_mono IsSerreClass.toIsClosedUnderSubobjects CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Arrow.w_mk_right CategoryTheory.Limits.kernel.lift_mono CategoryTheory.mono_comp CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Retract.instIsSplitMonoI
isoModSerre_iff 📖	mathematical	—	isoModSerre monoModSerre epiModSerre	—	—
isoModSerre_iff_of_epi 📖	mathematical	—	isoModSerre monoModSerre	—	epiModSerre_of_epi isoModSerre_iff
isoModSerre_iff_of_mono 📖	mathematical	—	isoModSerre epiModSerre	—	monoModSerre_of_mono isoModSerre_iff
isoModSerre_isInvertedBy_iff 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy isoModSerre CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.Functor.kernel	—	le_kernel_of_isoModSerre_isInvertedBy CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.ShortComplex.Exact.mono_g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.ShortComplex.Exact.map CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.ShortComplex.Exact.epi_f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.condition CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory
isoModSerre_of_epi 📖	mathematical	monoModSerre	isoModSerre	—	isoModSerre_iff_of_epi
isoModSerre_of_isIso 📖	mathematical	—	isoModSerre	—	isomorphisms_le_isoModSerre CategoryTheory.MorphismProperty.isomorphisms.infer_property
isoModSerre_of_mono 📖	mathematical	epiModSerre	isoModSerre	—	isoModSerre_iff_of_mono
isoModSerre_zero_iff 📖	mathematical	—	isoModSerre Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	—
isomorphisms_le_isoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isomorphisms isoModSerre	—	monoModSerre_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso epiModSerre_of_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso
le_kernel_of_isoModSerre_isInvertedBy 📖	mathematical	CategoryTheory.MorphismProperty.IsInvertedBy isoModSerre	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.Functor.kernel	—	CategoryTheory.Abelian.hasZeroObject isoModSerre_iff_of_mono CategoryTheory.Limits.HasZeroObject.instMono CategoryTheory.Limits.hasCoequalizer_of_self prop_iff_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Iso.isZero_iff CategoryTheory.Functor.map_isZero CategoryTheory.Limits.isZero_zero
monoModSerre_iff 📖	mathematical	—	monoModSerre CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels	—	—
monoModSerre_of_mono 📖	mathematical	—	monoModSerre	—	monomorphisms_le_monoModSerre CategoryTheory.MorphismProperty.monomorphisms.infer_property
monoModSerre_zero_iff 📖	mathematical	—	monoModSerre Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	prop_iff_of_iso instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients
monomorphisms_le_monoModSerre 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.monomorphisms monoModSerre	—	prop_of_isZero IsSerreClass.toContainsZero instIsClosedUnderIsomorphisms_1 IsSerreClass.toIsClosedUnderQuotients CategoryTheory.Limits.isZero_kernel_of_mono CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels

---

← Back to Index