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

def Counterexample.x : CategoryTheory.Over (ModuleCat.of ℤ ℚ ⊞ ModuleCat.of ℤ ℚ)

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

Equations

• One or more equations did not get rendered due to their size.

def Counterexample.y : CategoryTheory.Over (ModuleCat.of ℤ ℚ ⊞ ModuleCat.of ℤ ℚ)

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

Equations

• Counterexample.y = CategoryTheory.Over.mk (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id (ModuleCat.of ℤ ℚ)) (CategoryTheory.CategoryStruct.id (ModuleCat.of ℤ ℚ)))

theorem Counterexample.fst_x_pseudo_eq_fst_y : CategoryTheory.Abelian.PseudoEqual (ModuleCat.of ℤ ℚ) (CategoryTheory.Abelian.app CategoryTheory.Limits.biprod.fst Counterexample.x) (CategoryTheory.Abelian.app CategoryTheory.Limits.biprod.fst Counterexample.y)

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

theorem Counterexample.snd_x_pseudo_eq_snd_y : CategoryTheory.Abelian.PseudoEqual (ModuleCat.of ℤ ℚ) (CategoryTheory.Abelian.app CategoryTheory.Limits.biprod.snd Counterexample.x) (CategoryTheory.Abelian.app CategoryTheory.Limits.biprod.snd Counterexample.y)

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

theorem Counterexample.x_not_pseudo_eq : ¬CategoryTheory.Abelian.PseudoEqual (ModuleCat.of ℤ ℚ ⊞ ModuleCat.of ℤ ℚ) Counterexample.x Counterexample.y

x is not pseudoequal to y.

theorem Counterexample.fst_mk'_x_eq_fst_mk'_y : CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.fst ⟦Counterexample.x⟧ = CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.fst ⟦Counterexample.y⟧

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

theorem Counterexample.snd_mk'_x_eq_snd_mk'_y : CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.snd ⟦Counterexample.x⟧ = CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.biprod.snd ⟦Counterexample.y⟧

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

theorem Counterexample.mk'_x_ne_mk'_y : ⟦Counterexample.x⟧ ≠ ⟦Counterexample.y⟧

⟦x⟧ ≠ ⟦y⟧.

theorem Counterexample.exist_ne_and_fst_eq_fst_and_snd_eq_snd : ∃ (x : CategoryTheory.Abelian.Pseudoelement (ModuleCat.of ℤ ℚ ⊞ ModuleCat.of ℤ ℚ)) (y : CategoryTheory.Abelian.Pseudoelement (ModuleCat.of ℤ ℚ ⊞ ModuleCat.of ℤ ℚ)), 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.