Pseudoelements and pullbacks #

Borceux claims in Proposition 1.9.5 that the pseudoelement constructed in CategoryTheory.Abelian.Pseudoelement.pseudo_pullback is unique. We show here that this claim is false. This means in particular that we cannot have an extensionality principle for pullbacks in terms of pseudoelements.

Implementation details #

The construction, suggested in, is the following. We work in the category of ModuleCat and we consider the special case of ℚ ⊞ ℚ (that is the pullback over the terminal object). We consider the pseudoelements associated to x : ℚ ⟶ ℚ ⊞ ℚ given by t ↦ (t, 2 * t) and y : ℚ ⟶ ℚ ⊞ ℚ given by t ↦ (t, t).

Main results #

References #

x is given by t ↦ (t, 2 * t).

Instances For

    y is given by t ↦ (t, t).

    Instances For

      biprod.fst ≫ x is pseudoequal to biprod.fst y.

      biprod.snd ≫ x is pseudoequal to biprod.snd y.

      theorem Counterexample.exist_ne_and_fst_eq_fst_and_snd_eq_snd :
      x y, x y CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.fst x = CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.fst y CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.snd x = CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.snd y

      There are two pseudoelements x y : ℚ ⊞ ℚ such that xy, biprod.fst x = biprod.fst y and biprod.snd x = biprod.snd y.