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

source
noncomputable def counterexample.x  :
category_theory.over (Module.of ℤ ℚ ⊞ Module.of ℤ ℚ)

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

Equations
source
noncomputable def counterexample.y  :
category_theory.over (Module.of ℤ ℚ ⊞ Module.of ℤ ℚ)

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

Equations
source
theorem counterexample.fst_x_pseudo_eq_fst_y  :
category_theory.abelian.pseudo_equal (Module.of ℤ ℚ) (category_theory.abelian.app category_theory.limits.biprod.fst counterexample.x) (category_theory.abelian.app category_theory.limits.biprod.fst counterexample.y)

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

source
theorem counterexample.snd_x_pseudo_eq_snd_y  :
category_theory.abelian.pseudo_equal (Module.of ℤ ℚ) (category_theory.abelian.app category_theory.limits.biprod.snd counterexample.x) (category_theory.abelian.app category_theory.limits.biprod.snd counterexample.y)

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

source
theorem counterexample.x_not_pseudo_eq  :
¬category_theory.abelian.pseudo_equal (Module.of ℤ ℚ ⊞ Module.of ℤ ℚ) counterexample.x counterexample.y

x is not pseudoequal to y.

source
theorem counterexample.fst_mk_x_eq_fst_mk_y  :
⇑category_theory.limits.biprod.fst ⟦counterexample.x⟧ = ⇑category_theory.limits.biprod.fst ⟦counterexample.y⟧

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

source
theorem counterexample.snd_mk_x_eq_snd_mk_y  :
⇑category_theory.limits.biprod.snd ⟦counterexample.x⟧ = ⇑category_theory.limits.biprod.snd ⟦counterexample.y⟧

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

source
theorem counterexample.mk_x_ne_mk_y  :
⟦counterexample.x⟧ ≠ ⟦counterexample.y⟧

⟦x⟧ ≠ ⟦y⟧.

source
theorem counterexample.exist_ne_and_fst_eq_fst_and_snd_eq_snd  :
∃ (x y : ↥(Module.of ℤ ℚ ⊞ Module.of ℤ ℚ)), x ≠ y ∧ ⇑category_theory.limits.biprod.fst x = ⇑category_theory.limits.biprod.fst y ∧ ⇑category_theory.limits.biprod.snd x = ⇑category_theory.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.