mathlib3 documentation

mathlib-counterexamples / pseudoelement

Pseudoelements and pullbacks #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Borceux claims in Proposition 1.9.5 that the pseudoelement constructed in category_theory.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 Module 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 #

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