Documentation

Mathlib.CategoryTheory.Limits.Types.Equalizers

Equalizers in Type #

The equalizer of a pair of maps (g, h) from X to Y is the subtype {x : Y // g x = h x}.

source
noncomputable def CategoryTheory.Limits.Types.typeEqualizerOfUnique {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryStruct.comp f g = CategoryStruct.comp f h) (t : ∀ (y : Y), (ConcreteCategory.hom g) y = (ConcreteCategory.hom h) y → ∃! x : X, (ConcreteCategory.hom f) x = y) :
IsLimit (Fork.ofι f w)

Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Limits.Types.unique_of_type_equalizer {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryStruct.comp f g = CategoryStruct.comp f h) (t : IsLimit (Fork.ofι f w)) (y : Y) (hy : (ConcreteCategory.hom g) y = (ConcreteCategory.hom h) y) :
    ∃! x : X, (ConcreteCategory.hom f) x = y

    The converse of type_equalizer_of_unique.

    source
    theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryStruct.comp f g = CategoryStruct.comp f h) :
    Nonempty (IsLimit (Fork.ofι f w)) ↔ ∀ (y : Y), (ConcreteCategory.hom g) y = (ConcreteCategory.hom h) y → ∃! x : X, (ConcreteCategory.hom f) x = y
    source
    def CategoryTheory.Limits.Types.equalizerLimit {Y Z : Type u} {g h : Y ⟶ Z} :
    LimitCone (parallelPair g h)

    Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CategoryTheory.Limits.Types.equalizerIso {Y Z : Type u} (g h : Y ⟶ Z) :
      equalizer g h ≅ { x : Y // (ConcreteCategory.hom g) x = (ConcreteCategory.hom h) x }

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

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype {Y Z : Type u} (g h : Y ⟶ Z) :
        CategoryStruct.comp (equalizerIso g h).hom (TypeCat.ofHom Subtype.val) = equalizer.ι g h
        source
        @[simp]
        theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype_apply {Y Z : Type u} (g h : Y ⟶ Z) (x : equalizer g h) :
        ↑((ConcreteCategory.hom (equalizerIso g h).hom) x) = (ConcreteCategory.hom (equalizer.ι g h)) x
        source
        @[simp]
        theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι {Y Z : Type u} (g h : Y ⟶ Z) :
        CategoryStruct.comp (equalizerIso g h).inv (equalizer.ι g h) = TypeCat.ofHom Subtype.val
        source
        @[simp]
        theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply {Y Z : Type u} (g h : Y ⟶ Z) (x : { x : Y // (ConcreteCategory.hom g) x = (ConcreteCategory.hom h) x }) :
        (ConcreteCategory.hom (equalizer.ι g h)) ((ConcreteCategory.hom (equalizerIso g h).inv) x) = ↑x