EpiMono

📁 Source: Mathlib/CategoryTheory/EpiMono.lean

Statistics

Metric	Count
Definitions ofTruncSplitMono, IsSplitEpi, IsSplitMono, SplitEpi, comp, map, op, section_, splitMono, SplitEpiCategory, SplitMono, comp, map, op, retraction, splitEpi, SplitMonoCategory, retraction, section_	19
Theorems of_epi_section, of_epi_section', of_mono_retraction, of_mono_retraction', epi, exists_splitEpi, id, id_assoc, mk', of_iso, exists_splitMono, id, id_assoc, mk', mono, of_iso, comp_section_, epi, ext, ext_iff, id, id_assoc, map_section_, isSplitEpi_of_epi, comp_retraction, ext, ext_iff, id, id_assoc, map_retraction, mono, isSplitMono_of_mono, epi_comp_iff_of_epi, epi_comp_iff_of_isIso, instIsSplitEpiComp, instIsSplitEpiMap, instIsSplitEpiOppositeOpOfIsSplitMono, instIsSplitMonoComp, instIsSplitMonoMap, instIsSplitMonoOppositeOpOfIsSplitEpi, isIso_of_epi_of_isSplitMono, isIso_of_mono_of_isSplitEpi, isSplitEpi_of_epi, isSplitMono_of_mono, mono_comp_iff_of_isIso, mono_comp_iff_of_mono, op_epi_iff, op_epi_of_mono, op_mono_iff, op_mono_of_epi, retraction_isSplitEpi, section_isSplitMono, unop_epi_iff, unop_epi_of_mono, unop_mono_iff, unop_mono_of_epi	56
Total	75

CategoryTheory

Definitions

Name	Category	Theorems
IsSplitEpi 📖	CompData	35 math math: Functor.instIsSplitEpiBiproductComparison, Limits.pullback.instIsSplitEpiFst, SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ, Comonad.isSplitEpi_iff_isIso_counit, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, Limits.isSplitEpi_prod_fst, Limits.pullback.instIsSplitEpiSnd, instIsSplitEpiOppositeOpOfIsSplitMono, instIsSplitEpiMap, SimplexCategoryGenRel.instIsSplitEpiσ, Limits.initial.isSplitEpi_to, Functor.instIsSplitEpiBiprodComparison, IsSplitEpi.of_iso, Adjunction.unit_isSplitEpi_of_L_full, Limits.isSplitEpi_pi_π, isSplitEpi_iff_surjective, Retract.instIsSplitEpiR, RetractArrow.instIsSplitEpiRightRArrow, Limits.biprod.fst_epi, Limits.biprod.snd_epi, Functor.instIsSplitEpiApp, Limits.BinaryBicone.instIsSplitEpiFst, ShortComplex.Splitting.isSplitEpi_g, Limits.BinaryBicone.instIsSplitEpiSnd, SimplexCategoryGenRel.isSplitEpi_P_σ, Limits.isSplitEpi_prod_snd, isSplitEpi_of_epi, Limits.IsInitial.isSplitEpi_to, RetractArrow.instIsSplitEpiLeftRArrow, Limits.biproduct.π_epi, instIsSplitEpiComp, SplitEpiCategory.isSplitEpi_of_epi, retraction_isSplitEpi, IsSplitEpi.mk', Functor.isSplitEpi_iff
IsSplitMono 📖	CompData	35 math math: Functor.instIsSplitMonoBiprodComparison', instIsSplitMonoMap, Limits.isSplitMono_coprod_inr, Monad.isSplitMono_iff_isIso_unit, Limits.BinaryBicone.instIsSplitMonoInl, instIsSplitMonoOppositeOpOfIsSplitEpi, SimplexCategoryGenRel.instIsSplitMonoδ, Limits.terminal.isSplitMono_from, instIsSplitMonoComp, Functor.instIsSplitMonoApp, Functor.isSplitMono_iff, Limits.biproduct.ι_mono, Limits.instIsSplitMonoDiag, IsSplitMono.of_iso, SplitMonoCategory.isSplitMono_of_mono, isSplitMono_of_mono, Limits.isSplitMono_coprod_inl, CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective, HasClassifier.truthIsSplitMono, Retract.instIsSplitMonoI, section_isSplitMono, SimplexCategoryGenRel.isSplitMono_P_δ, IsSplitMono.mk', ShortComplex.Splitting.isSplitMono_f, RetractArrow.instIsSplitMonoRightIArrow, Limits.isSplitMono_sigma_ι, Limits.IsTerminal.isSplitMono_from, Limits.biprod.inr_mono, Limits.biprod.inl_mono, RetractArrow.instIsSplitMonoLeftIArrow, Adjunction.counit_isSplitMono_of_R_full, SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ, Limits.BinaryBicone.instIsSplitMonoInr, Limits.pullback.instIsSplitMonoDiagonal, Functor.instIsSplitMonoBiproductComparison'
SplitEpi 📖	CompData	1 math math: IsSplitEpi.exists_splitEpi
SplitEpiCategory 📖	CompData	5 math math: NonemptyFinLinOrd.instSplitEpiCategory, SimplexCategory.instSplitEpiCategory, Functor.splitEpiCategoryImpOfIsEquivalence, Pretriangulated.instSplitEpiCategory, instSplitEpiCategoryType
SplitMono 📖	CompData	1 math math: IsSplitMono.exists_splitMono
SplitMonoCategory 📖	CompData	1 math math: Pretriangulated.instSplitMonoCategory
retraction 📖	CompOp	7 math math: Limits.coneOfIsSplitMono_ι, Limits.coneOfIsSplitMono_π_app, IsSplitMono.id_assoc, IsSplitMono.id, Limits.coneOfIsSplitMono_pt, retraction_isSplitEpi, Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst
section_ 📖	CompOp	7 math math: IsSplitEpi.id, Limits.coconeOfIsSplitEpi_pt, Limits.coconeOfIsSplitEpi_π, section_isSplitMono, IsSplitEpi.id_assoc, Limits.coconeOfIsSplitEpi_ι_app, Limits.binaryBiconeOfIsSplitEpiOfKernel_inr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_comp_iff_of_epi 📖	mathematical	—	Epi CategoryStruct.comp Category.toCategoryStruct	—	epi_of_epi epi_comp
epi_comp_iff_of_isIso 📖	mathematical	—	Epi CategoryStruct.comp Category.toCategoryStruct	—	Category.assoc IsIso.hom_inv_id Category.comp_id epi_comp IsSplitEpi.epi IsSplitEpi.of_iso IsIso.inv_isIso
instIsSplitEpiComp 📖	mathematical	—	IsSplitEpi CategoryStruct.comp Category.toCategoryStruct	—	IsSplitEpi.mk' IsSplitEpi.exists_splitEpi
instIsSplitEpiMap 📖	mathematical	—	IsSplitEpi Functor.obj Functor.map	—	IsSplitEpi.mk' IsSplitEpi.exists_splitEpi
instIsSplitEpiOppositeOpOfIsSplitMono 📖	mathematical	—	IsSplitEpi Opposite Category.opposite Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct	—	IsSplitEpi.mk' IsSplitMono.exists_splitMono
instIsSplitMonoComp 📖	mathematical	—	IsSplitMono CategoryStruct.comp Category.toCategoryStruct	—	IsSplitMono.mk' IsSplitMono.exists_splitMono
instIsSplitMonoMap 📖	mathematical	—	IsSplitMono Functor.obj Functor.map	—	IsSplitMono.mk' IsSplitMono.exists_splitMono
instIsSplitMonoOppositeOpOfIsSplitEpi 📖	mathematical	—	IsSplitMono Opposite Category.opposite Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct	—	IsSplitMono.mk' IsSplitEpi.exists_splitEpi
isIso_of_epi_of_isSplitMono 📖	mathematical	—	IsIso	—	IsSplitMono.id cancel_epi IsSplitMono.id_assoc Category.comp_id
isIso_of_mono_of_isSplitEpi 📖	mathematical	—	IsIso	—	cancel_mono Category.assoc IsSplitEpi.id Category.comp_id Category.id_comp
isSplitEpi_of_epi 📖	mathematical	—	IsSplitEpi	—	SplitEpiCategory.isSplitEpi_of_epi
isSplitMono_of_mono 📖	mathematical	—	IsSplitMono	—	SplitMonoCategory.isSplitMono_of_mono
mono_comp_iff_of_isIso 📖	mathematical	—	Mono CategoryStruct.comp Category.toCategoryStruct	—	IsIso.inv_hom_id_assoc mono_comp IsSplitMono.mono IsSplitMono.of_iso IsIso.inv_isIso
mono_comp_iff_of_mono 📖	mathematical	—	Mono CategoryStruct.comp Category.toCategoryStruct	—	mono_of_mono mono_comp
op_epi_iff 📖	mathematical	—	Epi Opposite Category.opposite Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Mono	—	unop_mono_of_epi op_epi_of_mono
op_epi_of_mono 📖	mathematical	—	Epi Opposite Category.opposite Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct	—	cancel_mono
op_mono_iff 📖	mathematical	—	Mono Opposite Category.opposite Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Epi	—	unop_epi_of_mono op_mono_of_epi
op_mono_of_epi 📖	mathematical	—	Mono Opposite Category.opposite Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct	—	cancel_epi
retraction_isSplitEpi 📖	mathematical	—	IsSplitEpi retraction	—	IsSplitEpi.mk' IsSplitMono.exists_splitMono
section_isSplitMono 📖	mathematical	—	IsSplitMono section_	—	IsSplitMono.mk' IsSplitEpi.exists_splitEpi
unop_epi_iff 📖	mathematical	—	Epi Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Mono Opposite Category.opposite	—	op_mono_of_epi unop_epi_of_mono
unop_epi_of_mono 📖	mathematical	—	Epi Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct	—	cancel_mono
unop_mono_iff 📖	mathematical	—	Mono Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Epi Opposite Category.opposite	—	op_epi_of_mono unop_mono_of_epi
unop_mono_of_epi 📖	mathematical	—	Mono Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct	—	cancel_epi

CategoryTheory.Groupoid

Definitions

Name	Category	Theorems
ofTruncSplitMono 📖	CompOp	—

CategoryTheory.IsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_epi_section 📖	mathematical	—	CategoryTheory.IsIso	—	of_epi_section' CategoryTheory.IsSplitEpi.exists_splitEpi
of_epi_section' 📖	mathematical	—	CategoryTheory.IsIso	—	CategoryTheory.cancel_epi_id CategoryTheory.SplitEpi.id_assoc CategoryTheory.SplitEpi.id
of_mono_retraction 📖	mathematical	—	CategoryTheory.IsIso	—	of_mono_retraction' CategoryTheory.IsSplitMono.exists_splitMono
of_mono_retraction' 📖	mathematical	—	CategoryTheory.IsIso	—	CategoryTheory.SplitMono.id CategoryTheory.cancel_mono_id CategoryTheory.Category.assoc CategoryTheory.Category.comp_id

CategoryTheory.IsSplitEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi 📖	mathematical	—	CategoryTheory.Epi	—	CategoryTheory.SplitEpi.epi exists_splitEpi
exists_splitEpi 📖	mathematical	—	CategoryTheory.SplitEpi	—	—
id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.section_ CategoryTheory.CategoryStruct.id	—	CategoryTheory.SplitEpi.id exists_splitEpi
id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.section_	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' id
mk' 📖	mathematical	—	CategoryTheory.IsSplitEpi	—	—
of_iso 📖	mathematical	—	CategoryTheory.IsSplitEpi	—	mk' CategoryTheory.IsIso.inv_hom_id

CategoryTheory.IsSplitMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_splitMono 📖	mathematical	—	CategoryTheory.SplitMono	—	—
id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.retraction CategoryTheory.CategoryStruct.id	—	CategoryTheory.SplitMono.id exists_splitMono
id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.retraction	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' id
mk' 📖	mathematical	—	CategoryTheory.IsSplitMono	—	—
mono 📖	mathematical	—	CategoryTheory.Mono	—	CategoryTheory.SplitMono.mono exists_splitMono
of_iso 📖	mathematical	—	CategoryTheory.IsSplitMono	—	mk' CategoryTheory.IsIso.hom_inv_id

CategoryTheory.SplitEpi

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: comp_section_
map 📖	CompOp	1 math math: map_section_
op 📖	CompOp	—
section_ 📖	CompOp	11 math math: CategoryTheory.Retract.splitEpi_section_, id, comp_section_, CategoryTheory.Functor.splitEpiBiproductComparison_section_, id_assoc, CategoryTheory.ShortComplex.Splitting.splitEpi_g_section_, ext_iff, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, map_section_, CategoryTheory.Functor.splitEpiBiprodComparison_section_
splitMono 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_section_ 📖	mathematical	—	section_ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp	—	—
epi 📖	mathematical	—	CategoryTheory.Epi	—	CategoryTheory.whisker_eq id_assoc
ext 📖	—	section_	—	—	—
ext_iff 📖	mathematical	—	section_	—	ext
id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct section_ CategoryTheory.CategoryStruct.id	—	—
id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct section_	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' id
map_section_ 📖	mathematical	—	section_ CategoryTheory.Functor.obj CategoryTheory.Functor.map map	—	—

CategoryTheory.SplitEpiCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSplitEpi_of_epi 📖	mathematical	—	CategoryTheory.IsSplitEpi	—	—

CategoryTheory.SplitMono

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: comp_retraction
map 📖	CompOp	1 math math: map_retraction
op 📖	CompOp	—
retraction 📖	CompOp	10 math math: CategoryTheory.Retract.splitMono_retraction, map_retraction, CategoryTheory.ShortComplex.Splitting.splitMono_f_retraction, id_assoc, CategoryTheory.Functor.splitMonoBiproductComparison'_retraction, comp_retraction, id, CategoryTheory.Functor.splitMonoBiprodComparison'_retraction, CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction, ext_iff
splitEpi 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_retraction 📖	mathematical	—	retraction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp	—	—
ext 📖	—	retraction	—	—	—
ext_iff 📖	mathematical	—	retraction	—	ext
id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct retraction CategoryTheory.CategoryStruct.id	—	—
id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct retraction	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' id
map_retraction 📖	mathematical	—	retraction CategoryTheory.Functor.obj CategoryTheory.Functor.map map	—	—
mono 📖	mathematical	—	CategoryTheory.Mono	—	CategoryTheory.eq_whisker CategoryTheory.Category.assoc id CategoryTheory.Category.comp_id

CategoryTheory.SplitMonoCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSplitMono_of_mono 📖	mathematical	—	CategoryTheory.IsSplitMono	—	—

---

← Back to Index