EpiWithInjectiveKernel

📁 Source: Mathlib/CategoryTheory/Abelian/EpiWithInjectiveKernel.lean

Statistics

Metric	Count
Definitions epiWithInjectiveKernel	1
Theorems epiWithInjectiveKernel_iff, epiWithInjectiveKernel_of_iso, instIsMultiplicativeEpiWithInjectiveKernel	3
Total	4

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
epiWithInjectiveKernel 📖	CompOp	3 math math: instIsMultiplicativeEpiWithInjectiveKernel, epiWithInjectiveKernel_of_iso, epiWithInjectiveKernel_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epiWithInjectiveKernel_iff 📖	mathematical	—	epiWithInjectiveKernel CategoryTheory.ShortComplex.Splitting toPreadditive CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.ShortComplex.zero CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Injective.comp_factorThru CategoryTheory.ShortComplex.Splitting.s_g CategoryTheory.ShortComplex.Splitting.shortExact hasZeroObject CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsRegularEpi CategoryTheory.instIsRegularEpiOfIsSplitEpi CategoryTheory.Injective.of_iso
epiWithInjectiveKernel_of_iso 📖	mathematical	—	epiWithInjectiveKernel	—	epiWithInjectiveKernel_iff hasZeroObject CategoryTheory.Injective.zero_injective CategoryTheory.Limits.zero_comp CategoryTheory.Limits.isZero_zero
instIsMultiplicativeEpiWithInjectiveKernel 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative epiWithInjectiveKernel	—	epiWithInjectiveKernel_of_iso CategoryTheory.IsIso.id epiWithInjectiveKernel_iff CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct hasBinaryBiproducts CategoryTheory.Injective.instBiprod CategoryTheory.Limits.biprod.hom_ext' CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero zero_add CategoryTheory.Limits.BinaryBicone.inl_snd_assoc CategoryTheory.Category.id_comp CategoryTheory.ShortComplex.Splitting.s_g add_zero CategoryTheory.Limits.BinaryBicone.inr_fst_assoc CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Preadditive.comp_add CategoryTheory.ShortComplex.Splitting.s_r_assoc CategoryTheory.Limits.BinaryBicone.inl_fst_assoc CategoryTheory.Limits.BinaryBicone.inl_fst CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.Splitting.f_r CategoryTheory.Limits.BinaryBicone.inr_fst CategoryTheory.Limits.BinaryBicone.inl_snd CategoryTheory.Limits.BinaryBicone.inr_snd_assoc CategoryTheory.Limits.BinaryBicone.inr_snd CategoryTheory.whisker_eq CategoryTheory.eq_whisker CategoryTheory.ShortComplex.Splitting.id Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg

---

← Back to Index