EpiMono

📁 Source: Mathlib/Algebra/Homology/SpectralObject/EpiMono.lean

Statistics

Metric	Count
Definitions isoMapFourδ₁Toδ₀', isoMapFourδ₄Toδ₃', mapFourδ₁Toδ₀', mapFourδ₂Toδ₁', mapFourδ₄Toδ₃'	5
Theorems d_map_fourδ₄Toδ₃, d_map_fourδ₄Toδ₃_assoc, epi_map, instEpiMapFourδ₄Toδ₃, instMonoMapFourδ₁Toδ₀, isIso_mapFourδ₁Toδ₀', isIso_mapFourδ₂Toδ₁', isIso_mapFourδ₄Toδ₃', isIso_map_fourδ₁Toδ₀, isIso_map_fourδ₁Toδ₀_of_isZero, isIso_map_fourδ₄Toδ₃, isIso_map_fourδ₄Toδ₃_of_isZero, isoMapFourδ₁Toδ₀'_hom, isoMapFourδ₁Toδ₀'_hom_inv_id, isoMapFourδ₁Toδ₀'_hom_inv_id_assoc, isoMapFourδ₁Toδ₀'_inv_hom_id, isoMapFourδ₁Toδ₀'_inv_hom_id_assoc, isoMapFourδ₄Toδ₃'_hom, isoMapFourδ₄Toδ₄'_hom_inv_id, isoMapFourδ₄Toδ₄'_hom_inv_id_assoc, isoMapFourδ₄Toδ₄'_inv_hom_id, isoMapFourδ₄Toδ₄'_inv_hom_id_assoc, mapFourδ₁Toδ₀'_comp, mapFourδ₁Toδ₀'_comp_assoc, mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃', mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc, mapFourδ₄Toδ₃'_comp, mapFourδ₄Toδ₃'_comp_assoc, map_fourδ₁Toδ₀_d, map_fourδ₁Toδ₀_d_assoc, mono_map	31
Total	36

CategoryTheory.Abelian.SpectralObject

Definitions

Name	Category	Theorems
isoMapFourδ₁Toδ₀' 📖	CompOp	5 math math: isoMapFourδ₁Toδ₀'_hom_inv_id, isoMapFourδ₁Toδ₀'_inv_hom_id, isoMapFourδ₁Toδ₀'_hom_inv_id_assoc, isoMapFourδ₁Toδ₀'_inv_hom_id_assoc, isoMapFourδ₁Toδ₀'_hom
isoMapFourδ₄Toδ₃' 📖	CompOp	5 math math: isoMapFourδ₄Toδ₄'_inv_hom_id, isoMapFourδ₄Toδ₄'_inv_hom_id_assoc, isoMapFourδ₄Toδ₄'_hom_inv_id, isoMapFourδ₄Toδ₄'_hom_inv_id_assoc, isoMapFourδ₄Toδ₃'_hom
mapFourδ₁Toδ₀' 📖	CompOp	13 math math: SpectralSequence.HomologyData.kf_w, SpectralSequence.HomologyData.kfSc_f, isoMapFourδ₁Toδ₀'_hom_inv_id, isoMapFourδ₁Toδ₀'_inv_hom_id, mapFourδ₁Toδ₀'_comp_assoc, SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀', isoMapFourδ₁Toδ₀'_hom_inv_id_assoc, isoMapFourδ₁Toδ₀'_inv_hom_id_assoc, mapFourδ₁Toδ₀'_comp, isIso_mapFourδ₁Toδ₀', mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃', isoMapFourδ₁Toδ₀'_hom, mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc
mapFourδ₂Toδ₁' 📖	CompOp	1 math math: isIso_mapFourδ₂Toδ₁'
mapFourδ₄Toδ₃' 📖	CompOp	10 math math: isoMapFourδ₄Toδ₄'_inv_hom_id, isoMapFourδ₄Toδ₄'_inv_hom_id_assoc, mapFourδ₄Toδ₃'_comp_assoc, mapFourδ₄Toδ₃'_comp, isoMapFourδ₄Toδ₄'_hom_inv_id, mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃', isIso_mapFourδ₄Toδ₃', isoMapFourδ₄Toδ₄'_hom_inv_id_assoc, mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc, isoMapFourδ₄Toδ₃'_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_map_fourδ₄Toδ₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E d map CategoryTheory.ComposableArrows.fourδ₄Toδ₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_epi CategoryTheory.Limits.comp_zero instEpiToCycles toCycles_πE_d_assoc πE_map CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.hom_ext₂ cyclesMap_id CategoryTheory.Category.id_comp δ_toCycles_assoc δToCycles_πE
d_map_fourδ₄Toδ₃_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E d map CategoryTheory.ComposableArrows.fourδ₄Toδ₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_map_fourδ₄Toδ₃
epi_map 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.NatTrans.app CategoryTheory.CategoryStruct.id	CategoryTheory.Epi E map	—	cyclesMap_id CategoryTheory.instEpiId CategoryTheory.epi_of_epi_fac CategoryTheory.epi_comp πE_map CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.homMk₂.congr_simp CategoryTheory.ComposableArrows.hom_ext₂
instEpiMapFourδ₄Toδ₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi E map CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	epi_map
instMonoMapFourδ₁Toδ₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀	—	mono_map
isIso_mapFourδ₁Toδ₀' 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.IsIso E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀'	—	isIso_map_fourδ₁Toδ₀_of_isZero LE.le.trans
isIso_mapFourδ₂Toδ₁' 📖	mathematical	Preorder.toLE	CategoryTheory.IsIso E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₂Toδ₁'	—	LE.le.trans isIso_map
isIso_mapFourδ₄Toδ₃' 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.IsIso E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₄Toδ₃'	—	isIso_map_fourδ₄Toδ₃_of_isZero LE.le.trans
isIso_map_fourδ₁Toδ₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.IsIso E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀	—	CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono' CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id CategoryTheory.ShortComplex.Exact.mono_g exact₂
isIso_map_fourδ₁Toδ₀_of_isZero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.IsIso E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀	—	isIso_map_fourδ₁Toδ₀ CategoryTheory.Limits.IsZero.eq_of_src
isIso_map_fourδ₄Toδ₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.IsIso E map CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono' CategoryTheory.ShortComplex.Exact.epi_f exact₂ CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.instIsSplitMonoMap CategoryTheory.IsSplitMono.of_iso
isIso_map_fourδ₄Toδ₃_of_isZero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.IsIso E map CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	isIso_map_fourδ₄Toδ₃ CategoryTheory.Limits.IsZero.eq_of_tgt
isoMapFourδ₁Toδ₀'_hom 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.Iso.hom E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans isoMapFourδ₁Toδ₀' mapFourδ₁Toδ₀'	—	LE.le.trans
isoMapFourδ₁Toδ₀'_hom_inv_id 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀' CategoryTheory.Iso.inv isoMapFourδ₁Toδ₀' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id LE.le.trans
isoMapFourδ₁Toδ₀'_hom_inv_id_assoc 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀' CategoryTheory.Iso.inv isoMapFourδ₁Toδ₀'	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoMapFourδ₁Toδ₀'_hom_inv_id
isoMapFourδ₁Toδ₀'_inv_hom_id 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans CategoryTheory.Iso.inv isoMapFourδ₁Toδ₀' mapFourδ₁Toδ₀' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id LE.le.trans
isoMapFourδ₁Toδ₀'_inv_hom_id_assoc 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans CategoryTheory.Iso.inv isoMapFourδ₁Toδ₀' mapFourδ₁Toδ₀'	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoMapFourδ₁Toδ₀'_inv_hom_id
isoMapFourδ₄Toδ₃'_hom 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.Iso.hom E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans isoMapFourδ₄Toδ₃' mapFourδ₄Toδ₃'	—	LE.le.trans
isoMapFourδ₄Toδ₄'_hom_inv_id 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₄Toδ₃' CategoryTheory.Iso.inv isoMapFourδ₄Toδ₃' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id LE.le.trans
isoMapFourδ₄Toδ₄'_hom_inv_id_assoc 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₄Toδ₃' CategoryTheory.Iso.inv isoMapFourδ₄Toδ₃'	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoMapFourδ₄Toδ₄'_hom_inv_id
isoMapFourδ₄Toδ₄'_inv_hom_id 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans CategoryTheory.Iso.inv isoMapFourδ₄Toδ₃' mapFourδ₄Toδ₃' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id LE.le.trans
isoMapFourδ₄Toδ₄'_inv_hom_id_assoc 📖	mathematical	Preorder.toLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans CategoryTheory.Iso.inv isoMapFourδ₄Toδ₃' mapFourδ₄Toδ₃'	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoMapFourδ₄Toδ₄'_inv_hom_id
mapFourδ₁Toδ₀'_comp 📖	mathematical	Preorder.toLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀'	—	LE.le.trans map_comp
mapFourδ₁Toδ₀'_comp_assoc 📖	mathematical	Preorder.toLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀'	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapFourδ₁Toδ₀'_comp
mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃' 📖	mathematical	Preorder.toLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀' mapFourδ₄Toδ₃'	—	LE.le.trans map_comp
mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc 📖	mathematical	Preorder.toLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₁Toδ₀' mapFourδ₄Toδ₃'	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'
mapFourδ₄Toδ₃'_comp 📖	mathematical	Preorder.toLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₄Toδ₃'	—	LE.le.trans map_comp
mapFourδ₄Toδ₃'_comp_assoc 📖	mathematical	Preorder.toLE	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E Preorder.smallCategory CategoryTheory.homOfLE LE.le.trans mapFourδ₄Toδ₃'	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapFourδ₄Toδ₃'_comp
map_fourδ₁Toδ₀_d 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀ d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp instMonoFromOpcycles d_ιE_fromOpcycles fromOpcyles_δ map_ιE_assoc CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.hom_ext₂ opcyclesMap_id CategoryTheory.Category.id_comp ιE_δFromOpcycles
map_fourδ₁Toδ₀_d_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀ d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_fourδ₁Toδ₀_d
mono_map 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.NatTrans.app CategoryTheory.CategoryStruct.id	CategoryTheory.Mono E map	—	map_ιE CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.homMk₂.congr_simp CategoryTheory.ComposableArrows.hom_ext₂ CategoryTheory.mono_of_mono_fac CategoryTheory.Category.comp_id opcyclesMap_id

---

← Back to Index