Equalizers

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean

Statistics

Metric	Count
Definitions iso, iso, isColimitCoforkMapOfIsColimit, isColimitMapCoconeCoforkEquiv, isColimitOfHasCoequalizerOfPreservesColimit, isColimitOfIsColimitCoforkMap, isLimitForkMapOfIsLimit, isLimitMapConeForkEquiv, isLimitOfHasEqualizerOfPreservesLimit, isLimitOfIsLimitForkMap	10
Theorems iso_hom, iso_hom, iso_inv_ι, of_iso_comparison, instIsIsoCoequalizerComparison, instIsIsoEqualizerComparison, map_π_epi, map_π_preserves_coequalizer_inv, map_π_preserves_coequalizer_inv_assoc, map_π_preserves_coequalizer_inv_colimMap, map_π_preserves_coequalizer_inv_colimMap_assoc, map_π_preserves_coequalizer_inv_colimMap_desc, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, map_π_preserves_coequalizer_inv_desc, map_π_preserves_coequalizer_inv_desc_assoc, of_iso_comparison, preservesSplitCoequalizers, preservesSplitEqualizers	18
Total	28

CategoryTheory.Limits

Definitions

Name	Category	Theorems
isColimitCoforkMapOfIsColimit 📖	CompOp	—
isColimitMapCoconeCoforkEquiv 📖	CompOp	—
isColimitOfHasCoequalizerOfPreservesColimit 📖	CompOp	—
isColimitOfIsColimitCoforkMap 📖	CompOp	—
isLimitForkMapOfIsLimit 📖	CompOp	—
isLimitMapConeForkEquiv 📖	CompOp	—
isLimitOfHasEqualizerOfPreservesLimit 📖	CompOp	—
isLimitOfIsLimitForkMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoCoequalizerComparison 📖	mathematical	—	CategoryTheory.IsIso coequalizer CategoryTheory.Functor.obj CategoryTheory.Functor.map coequalizerComparison	—	PreservesCoequalizer.iso_hom CategoryTheory.Iso.isIso_hom
instIsIsoEqualizerComparison 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj equalizer CategoryTheory.Functor.map equalizerComparison	—	PreservesEqualizer.iso_hom CategoryTheory.Iso.isIso_hom
map_π_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj coequalizer CategoryTheory.Functor.map coequalizer.π	—	ι_comp_coequalizerComparison CategoryTheory.cancel_epi CategoryTheory.epi_comp coequalizer.π_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso instIsIsoCoequalizerComparison
map_π_preserves_coequalizer_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj coequalizer CategoryTheory.Functor.map coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso	—	ι_comp_coequalizerComparison_assoc PreservesCoequalizer.iso_hom CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
map_π_preserves_coequalizer_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj coequalizer CategoryTheory.Functor.map coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_π_preserves_coequalizer_inv
map_π_preserves_coequalizer_inv_colimMap 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	coequalizer colimit WalkingParallelPair walkingParallelPairHomCategory parallelPair coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso colimMap parallelPairHom	—	CategoryTheory.Category.assoc map_π_preserves_coequalizer_inv ι_colimMap parallelPairHom_app_one
map_π_preserves_coequalizer_inv_colimMap_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	coequalizer coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso colimit WalkingParallelPair walkingParallelPairHomCategory parallelPair colimMap parallelPairHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_π_preserves_coequalizer_inv_colimMap
map_π_preserves_coequalizer_inv_colimMap_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	coequalizer coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso colimit WalkingParallelPair walkingParallelPairHomCategory parallelPair colimMap parallelPairHom coequalizer.desc	—	CategoryTheory.Category.assoc map_π_preserves_coequalizer_inv_colimMap coequalizer.π_desc
map_π_preserves_coequalizer_inv_colimMap_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	coequalizer coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso colimit WalkingParallelPair walkingParallelPairHomCategory parallelPair colimMap parallelPairHom coequalizer.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_π_preserves_coequalizer_inv_colimMap_desc
map_π_preserves_coequalizer_inv_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	coequalizer coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso coequalizer.desc	—	CategoryTheory.Category.assoc map_π_preserves_coequalizer_inv coequalizer.π_desc
map_π_preserves_coequalizer_inv_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	coequalizer coequalizer.π CategoryTheory.Iso.inv PreservesCoequalizer.iso coequalizer.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_π_preserves_coequalizer_inv_desc
of_iso_comparison 📖	mathematical	—	PreservesColimit WalkingParallelPair walkingParallelPairHomCategory parallelPair	—	preservesColimit_of_preserves_colimit_cocone coequalizer.condition
preservesSplitCoequalizers 📖	mathematical	—	PreservesColimit WalkingParallelPair walkingParallelPairHomCategory parallelPair	—	preservesColimit_of_preserves_colimit_cocone CategoryTheory.IsSplitCoequalizer.condition
preservesSplitEqualizers 📖	mathematical	—	PreservesLimit WalkingParallelPair walkingParallelPairHomCategory parallelPair	—	preservesLimit_of_preserves_limit_cone CategoryTheory.IsSplitEqualizer.condition

CategoryTheory.Limits.PreservesCoequalizer

Definitions

Name	Category	Theorems
iso 📖	CompOp	13 math math: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, π_tensor_id_preserves_coequalizer_inv_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_assoc, id_tensor_π_preserves_coequalizer_inv_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_assoc, iso_hom, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc_assoc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc_assoc, π_tensor_id_preserves_coequalizer_inv_colimMap_desc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.coequalizer CategoryTheory.Functor.obj CategoryTheory.Functor.map iso CategoryTheory.Limits.coequalizerComparison	—	—

CategoryTheory.Limits.PreservesEqualizer

Definitions

Name	Category	Theorems
iso 📖	CompOp	2 math math: iso_hom, iso_inv_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Limits.equalizer CategoryTheory.Functor.map iso CategoryTheory.Limits.equalizerComparison	—	—
iso_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.equalizer CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Limits.equalizer.ι	—	CategoryTheory.Iso.cancel_iso_hom_left CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp CategoryTheory.Limits.equalizerComparison_comp_π
of_iso_comparison 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.equalizer.condition

---

← Back to Index