Equalizer

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean

Statistics

Metric	Count
Definitions equalizerPullbackMapIso	1
Theorems equalizerPullbackMapIso_hom_fst, equalizerPullbackMapIso_hom_fst_assoc, equalizerPullbackMapIso_hom_snd, equalizerPullbackMapIso_hom_snd_assoc, equalizerPullbackMapIso_inv_ι_fst, equalizerPullbackMapIso_inv_ι_fst_assoc, equalizerPullbackMapIso_inv_ι_snd, equalizerPullbackMapIso_inv_ι_snd_assoc, isPullback_equalizer_prod, isPushout_coequalizer_coprod	10
Total	11

CategoryTheory.Limits

Definitions

Name	Category	Theorems
equalizerPullbackMapIso 📖	CompOp	8 math math: equalizerPullbackMapIso_inv_ι_snd, equalizerPullbackMapIso_inv_ι_fst, equalizerPullbackMapIso_hom_fst_assoc, equalizerPullbackMapIso_hom_snd_assoc, equalizerPullbackMapIso_hom_snd, equalizerPullbackMapIso_hom_fst, equalizerPullbackMapIso_inv_ι_snd_assoc, equalizerPullbackMapIso_inv_ι_fst_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizerPullbackMapIso_hom_fst 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	equalizer pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.map CategoryTheory.CategoryStruct.id WalkingParallelPair walkingParallelPairHomCategory parallelPair equalizer.ι pullback.fst CategoryTheory.Iso.hom equalizerPullbackMapIso	—	hasLimitOfHasLimitsOfShape limit.lift_π_assoc limit.lift_π
equalizerPullbackMapIso_hom_fst_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	equalizer pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.map CategoryTheory.CategoryStruct.id WalkingParallelPair walkingParallelPairHomCategory parallelPair equalizer.ι pullback.fst CategoryTheory.Iso.hom equalizerPullbackMapIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerPullbackMapIso_hom_fst
equalizerPullbackMapIso_hom_snd 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	equalizer pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.map CategoryTheory.CategoryStruct.id WalkingParallelPair walkingParallelPairHomCategory parallelPair equalizer.ι pullback.fst CategoryTheory.Iso.hom equalizerPullbackMapIso pullback.snd	—	pullback.hom_ext hasLimitOfHasLimitsOfShape limit.lift_π
equalizerPullbackMapIso_hom_snd_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	equalizer pullback hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan pullback.map CategoryTheory.CategoryStruct.id WalkingParallelPair walkingParallelPairHomCategory parallelPair equalizer.ι pullback.fst CategoryTheory.Iso.hom equalizerPullbackMapIso pullback.snd	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerPullbackMapIso_hom_snd
equalizerPullbackMapIso_inv_ι_fst 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pullback equalizer hasLimitOfHasLimitsOfShape WalkingParallelPair walkingParallelPairHomCategory parallelPair WalkingCospan WidePullbackShape.category WalkingPair cospan equalizer.ι pullback.fst pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv equalizerPullbackMapIso	—	hasLimitOfHasLimitsOfShape limit.lift_π_assoc limit.lift_π
equalizerPullbackMapIso_inv_ι_fst_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pullback equalizer hasLimitOfHasLimitsOfShape WalkingParallelPair walkingParallelPairHomCategory parallelPair WalkingCospan WidePullbackShape.category WalkingPair cospan equalizer.ι pullback.fst pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv equalizerPullbackMapIso	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerPullbackMapIso_inv_ι_fst
equalizerPullbackMapIso_inv_ι_snd 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pullback equalizer hasLimitOfHasLimitsOfShape WalkingParallelPair walkingParallelPairHomCategory parallelPair WalkingCospan WidePullbackShape.category WalkingPair cospan equalizer.ι pullback.fst pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv equalizerPullbackMapIso pullback.snd	—	hasLimitOfHasLimitsOfShape limit.lift_π_assoc limit.lift_π
equalizerPullbackMapIso_inv_ι_snd_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pullback equalizer hasLimitOfHasLimitsOfShape WalkingParallelPair walkingParallelPairHomCategory parallelPair WalkingCospan WidePullbackShape.category WalkingPair cospan equalizer.ι pullback.fst pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv equalizerPullbackMapIso pullback.snd	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerPullbackMapIso_inv_ι_snd
isPullback_equalizer_prod 📖	mathematical	—	CategoryTheory.IsPullback equalizer prod equalizer.ι CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod.lift CategoryTheory.CategoryStruct.id	—	prod.hom_ext prod.comp_lift equalizer.condition limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.CommSq.w PullbackCone.condition limit.lift_π_assoc equalizer.hom_ext
isPushout_coequalizer_coprod 📖	mathematical	—	CategoryTheory.IsPushout coprod coequalizer coprod.desc CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct coequalizer.π CategoryTheory.CategoryStruct.comp	—	coprod.hom_ext coprod.desc_comp coequalizer.condition colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.CommSq.w PushoutCocone.condition CategoryTheory.Category.assoc coequalizer.hom_ext

---

← Back to Index