MonoCoprod

📁 Source: Mathlib/CategoryTheory/Limits/MonoCoprod.lean

Statistics

Metric	Count
Definitions MonoCoprod, binaryCofanSum, isColimitBinaryCofanSum	3
Theorems binaryCofan_inl, binaryCofan_inr, instMonoInl, instMonoInr, instOfPreservesColimitsOfShapeDiscreteWalkingPairOfReflectsMonomorphismsForget, mk', monoCoprodType, monoCoprod_of_preservesCoprod_of_reflectsMono, mono_binaryCofanSum_inl, mono_binaryCofanSum_inl', mono_binaryCofanSum_inr, mono_binaryCofanSum_inr', mono_inj, mono_inl_iff, mono_map'_of_injective, mono_of_injective, mono_of_injective', mono_of_injective_aux, mono_ι, instPreservesMonomorphismsObjFunctorTypeSigmaConst, monoCoprodOfHasZeroMorphisms	21
Total	24

CategoryTheory.Limits

Definitions

Name	Category	Theorems
MonoCoprod 📖	CompData	9 math math: CategoryTheory.instMonoCoprodOfFinitaryExtensive, MonoCoprod.instOfPreservesColimitsOfShapeDiscreteWalkingPairOfReflectsMonomorphismsForget, CategoryTheory.IsCartesianDistributive.monoCoprod, MonoCoprod.mk', MonoCoprod.monoCoprodType, AlgebraicGeometry.instMonoCoprodScheme, monoCoprodOfHasZeroMorphisms, CategoryTheory.PreGaloisCategory.instMonoCoprod, MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesMonomorphismsObjFunctorTypeSigmaConst 📖	mathematical	HasCoproducts	CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category sigmaConst	—	MonoCoprod.mono_map'_of_injective CategoryTheory.mono_iff_injective hasColimitOfHasColimitsOfShape
monoCoprodOfHasZeroMorphisms 📖	mathematical	—	MonoCoprod	—	CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.mk' IsColimit.fac

CategoryTheory.Limits.MonoCoprod

Definitions

Name	Category	Theorems
binaryCofanSum 📖	CompOp	2 math math: mono_binaryCofanSum_inr, mono_binaryCofanSum_inl
isColimitBinaryCofanSum 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binaryCofan_inl 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.BinaryCofan.inl	—	—
binaryCofan_inr 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.BinaryCofan.inr	—	binaryCofan_inl CategoryTheory.Limits.IsColimit.fac CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
instMonoInl 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.inl	—	binaryCofan_inl
instMonoInr 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.inr	—	binaryCofan_inr
instOfPreservesColimitsOfShapeDiscreteWalkingPairOfReflectsMonomorphismsForget 📖	mathematical	—	CategoryTheory.Limits.MonoCoprod	—	monoCoprod_of_preservesCoprod_of_reflectsMono monoCoprodType
mk' 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.BinaryCofan.inl	CategoryTheory.Limits.MonoCoprod	—	mono_inl_iff
monoCoprodType 📖	mathematical	—	CategoryTheory.Limits.MonoCoprod CategoryTheory.types	—	mk' CategoryTheory.mono_iff_injective
monoCoprod_of_preservesCoprod_of_reflectsMono 📖	mathematical	—	CategoryTheory.Limits.MonoCoprod	—	CategoryTheory.Functor.mono_of_mono_map binaryCofan_inl CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Category.comp_id
mono_binaryCofanSum_inl 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete.functor CategoryTheory.Limits.WalkingPair.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const binaryCofanSum CategoryTheory.Limits.BinaryCofan.inl	—	binaryCofan_inl
mono_binaryCofanSum_inl' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	CategoryTheory.Mono	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext CategoryTheory.Limits.Cofan.IsColimit.fac binaryCofan_inl
mono_binaryCofanSum_inr 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete.functor CategoryTheory.Limits.WalkingPair.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const binaryCofanSum CategoryTheory.Limits.BinaryCofan.inr	—	binaryCofan_inr
mono_binaryCofanSum_inr' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	CategoryTheory.Mono	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext CategoryTheory.Limits.Cofan.IsColimit.fac binaryCofan_inr
mono_inj 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	—	mono_of_injective CategoryTheory.Category.id_comp
mono_inl_iff 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.BinaryCofan.inl	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom
mono_map'_of_injective 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.map' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.Sigma.ι_comp_map' CategoryTheory.Category.id_comp CategoryTheory.Limits.colimit.ι_desc mono_of_injective'
mono_of_injective 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Cofan.IsColimit.desc	—	mono_of_injective_aux
mono_of_injective' 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.desc CategoryTheory.Limits.Sigma.ι	—	mono_of_injective
mono_of_injective_aux 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Cofan.IsColimit.desc	—	mono_binaryCofanSum_inl' CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Limits.Cofan.IsColimit.fac
mono_ι 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.ι	—	—

---

← Back to Index