# Documentation

Counterexamples.Pseudoelement

# 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 https://mathoverflow.net/a/419951/7845, 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 #

• Counterexample.exist_ne_and_fst_eq_fst_and_snd_eq_snd : there are two pseudoelements x y : ℚ ⊞ ℚ such that x ≠ y, biprod.fst x = biprod.fst y and biprod.snd x = biprod.snd y.

## References #

• [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]

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.

x is not pseudoequal to y.

biprod.fst ⟦x⟧ = biprod.fst ⟦y⟧.

biprod.snd ⟦x⟧ = biprod.snd ⟦y⟧.

⟦x⟧ ≠ ⟦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 x ≠ y, biprod.fst x = biprod.fst y and biprod.snd x = biprod.snd y.