Theorems · Definition · category theory

CategoryTheory.Limits.Types.equalizerIso

{Y Z : Type u} →
  (g h : Y ⟶ Z) →
    CategoryTheory.Limits.equalizer g h ≅
      { x // (CategoryTheory.ConcreteCategory.hom g) x = (CategoryTheory.ConcreteCategory.hom h) x }

The categorical equalizer in Type u is {x : Y // g x = h x}.

Defined in: Mathlib.CategoryTheory.Limits.Types.Equalizers
Cited by: 7 results in Mathlib
Foundations: Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.ConcreteCategory.homstatement · cited by 4,022
CategoryTheory.Isostatement · cited by 3,963
TypeCat.Funstatement · cited by 1,307
CategoryTheory.Limits.WalkingParallelPairstatement · cited by 781
CategoryTheory.Limits.parallelPairstatement · cited by 766
CategoryTheory.Limits.equalizerstatement · cited by 60
CategoryTheory.Limits.limit.isoLimitConeproof · cited by 8
CategoryTheory.Limits.Types.equalizerLimitproof · cited by 1

Cited by8

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Types.equalizerIso_inv_comp_ιstatement · cited by 3
CategoryTheory.PreGaloisCategory.fiberEqualizerEquivproof · cited by 2
CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtypestatement and proof · cited by 1
CategoryTheory.regularTopology.mapToEqualizer_eq_compstatement and proof · cited by 1
CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype_applystatement and proof · cited by 0
CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_applystatement and proof · cited by 0
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_applyproof · cited by 0
CategoryTheory.regularTopology.equalizerCondition_iff_isIso_liftproof · cited by 0