Simple

📁 Source: Mathlib/CategoryTheory/Simple.lean

Statistics

Metric	Count
Definitions Simple	1
Theorems isIso_inl_iff_isZero, iff_of_iso, mono_isIso_iff_nonzero, not_isZero, of_iso, cokernel_zero_of_nonzero_to_simple, epi_from_simple_zero_of_not_iso, epi_of_nonzero_to_simple, id_nonzero, indecomposable_of_simple, instIsSimpleOrderSubobjectOfSimple, instNontrivialEndOfSimple, instNontrivialSubobjectOfSimple, isIso_of_epi_of_nonzero, isIso_of_mono_of_nonzero, kernel_zero_of_nonzero_from_simple, mono_to_simple_zero_of_not_iso, simple_iff_subobject_isSimpleOrder, simple_of_cosimple, simple_of_isSimpleOrder_subobject, subobject_simple_iff_isAtom, zero_not_simple	22
Total	23

CategoryTheory

Definitions

Name	Category	Theorems
Simple 📖	CompData	14 math math: simple_of_finrank_eq_one, Simple.iff_of_iso, instSimpleSimpleSubobject, Simple.of_iso, simple_iff_subobject_isSimpleOrder, simple_of_cosimple, simple_iff_isSimpleModule, subobject_simple_iff_isAtom, simple_of_isSimpleModule, simple_of_isSimpleOrder_subobject, FDRep.simple_iff_end_is_rank_one, exists_simple_subobject, simple_iff_isSimpleModule', FDRep.simple_iff_char_is_norm_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokernel_zero_of_nonzero_to_simple 📖	mathematical	—	Limits.cokernel.π Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive Limits.HasCokernels.has_colimit Abelian.has_cokernels Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.cokernel Limits.HasZeroMorphisms.zero	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.eq_zero_of_mono_cokernel mono_of_strongMono instStrongMonoOfIsRegularMono instIsRegularMonoOfIsSplitMono IsSplitMono.of_iso isIso_of_epi_of_nonzero Limits.coequalizer.π_epi
epi_from_simple_zero_of_not_iso 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasZeroMorphisms.zero Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive	—	isIso_of_epi_of_nonzero
epi_of_nonzero_to_simple 📖	mathematical	—	Epi	—	Limits.image.fac epi_comp Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair Limits.hasLimitOfHasLimitsOfShape epi_of_effectiveEpi instEffectiveEpiOfIsIso isIso_of_mono_of_nonzero Limits.instMonoι Limits.eq_zero_of_image_eq_zero
id_nonzero 📖	—	—	—	—	Simple.mono_isIso_iff_nonzero instMonoId IsIso.id
indecomposable_of_simple 📖	mathematical	—	Indecomposable Preadditive.preadditiveHasZeroMorphisms	—	Limits.HasBinaryBiproducts.has_binary_biproduct Simple.not_isZero Simple.of_iso Biprod.isIso_inl_iff_isZero Simple.mono_isIso_iff_nonzero mono_of_strongMono instStrongMonoOfIsRegularMono instIsRegularMonoOfIsSplitMono Limits.biprod.inl_mono Limits.IsZero.iff_isSplitMono_eq_zero
instIsSimpleOrderSubobjectOfSimple 📖	mathematical	—	IsSimpleOrder Subobject Preorder.toLE PartialOrder.toPreorder instPartialOrderSubobject Subobject.boundedOrder Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass	—	Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass instNontrivialSubobjectOfSimple Subobject.mk_surjective Subobject.mk_eq_bot_iff_zero Subobject.isIso_iff_mk_eq_top Simple.mono_isIso_iff_nonzero
instNontrivialEndOfSimple 📖	mathematical	—	Nontrivial End Category.toCategoryStruct	—	nontrivial_of_ne id_nonzero
instNontrivialSubobjectOfSimple 📖	mathematical	—	Nontrivial Subobject	—	Subobject.nontrivial_of_not_isZero Simple.not_isZero
isIso_of_epi_of_nonzero 📖	mathematical	—	IsIso	—	isIso_of_mono_of_epi balanced_of_strongMonoCategory strongMonoCategory_of_regularMonoCategory regularMonoCategoryOfNormalMonoCategory Abelian.toIsNormalMonoCategory Preadditive.mono_of_kernel_zero Limits.HasKernels.has_limit Abelian.has_kernels mono_to_simple_zero_of_not_iso Limits.equalizer.ι_mono Limits.kernel_not_iso_of_nonzero
isIso_of_mono_of_nonzero 📖	mathematical	—	IsIso	—	Simple.mono_isIso_iff_nonzero
kernel_zero_of_nonzero_from_simple 📖	mathematical	—	Limits.kernel.ι Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.kernel Limits.HasZeroMorphisms.zero	—	Limits.eq_zero_of_epi_kernel epi_of_effectiveEpi instEffectiveEpiOfIsIso isIso_of_mono_of_nonzero Limits.equalizer.ι_mono
mono_to_simple_zero_of_not_iso 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasZeroMorphisms.zero	—	isIso_of_mono_of_nonzero
simple_iff_subobject_isSimpleOrder 📖	mathematical	—	Simple IsSimpleOrder Subobject Preorder.toLE PartialOrder.toPreorder instPartialOrderSubobject Subobject.boundedOrder Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass	—	Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass instIsSimpleOrderSubobjectOfSimple simple_of_isSimpleOrder_subobject
simple_of_cosimple 📖	mathematical	IsIso	Simple Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive	—	Limits.HasCokernels.has_colimit Abelian.has_cokernels Limits.cokernel.π_of_epi Abelian.hasZeroObject epi_of_effectiveEpi instEffectiveEpiOfIsIso Limits.hasCoequalizer_of_self Limits.coequalizer.π_epi Limits.cokernel.π_of_zero Preadditive.epi_of_cokernel_zero Limits.cokernel_not_iso_of_nonzero isIso_of_mono_of_epi balanced_of_strongMonoCategory strongMonoCategory_of_regularMonoCategory regularMonoCategoryOfNormalMonoCategory Abelian.toIsNormalMonoCategory
simple_of_isSimpleOrder_subobject 📖	mathematical	—	Simple	—	Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass IsSimpleOrder.bot_ne_top Subobject.mk_eq_bot_iff_zero Subobject.isIso_iff_mk_eq_top IsSimpleOrder.eq_bot_or_eq_top
subobject_simple_iff_isAtom 📖	mathematical	—	Simple Functor.obj Subobject Preorder.smallCategory PartialOrder.toPreorder instPartialOrderSubobject Subobject.underlying IsAtom Subobject.orderBot Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass	—	Limits.HasZeroObject.hasInitial Limits.HasZeroObject.initialMonoClass simple_iff_subobject_isSimpleOrder OrderIso.isSimpleOrder_iff Set.isSimpleOrder_Iic_iff_isAtom
zero_not_simple 📖	—	—	—	—	Simple.mono_isIso_iff_nonzero Limits.HasZeroObject.instMono Limits.comp_zero Limits.id_zero

CategoryTheory.Biprod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_inl_iff_isZero 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.biprod CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.IsZero	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl CategoryTheory.Limits.biprod.total add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd CategoryTheory.eq_whisker CategoryTheory.Category.assoc CategoryTheory.Limits.BinaryBicone.inr_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.zero_comp CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero CategoryTheory.Limits.biprod.snd_epi

CategoryTheory.Simple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_iso 📖	mathematical	—	CategoryTheory.Simple	—	of_iso
mono_isIso_iff_nonzero 📖	mathematical	—	CategoryTheory.IsIso	—	—
not_isZero 📖	mathematical	—	CategoryTheory.Limits.IsZero	—	CategoryTheory.id_nonzero
of_iso 📖	mathematical	—	CategoryTheory.Simple	—	CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.zero_comp mono_isIso_iff_nonzero CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.isIso_of_mono_of_nonzero CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.cancel_mono CategoryTheory.Iso.isIso_inv

---

← Back to Index