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 #

References #

source
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.
Instances For
    source
    def Counterexample.y :
    CategoryTheory.Over (ModuleCat.of ℤ ℚ ⊞ ModuleCat.of ℤ ℚ)

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

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

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

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

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

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

      x is not pseudoequal to y.

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

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

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

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

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

      ⟦x⟧ ≠ ⟦y⟧.

      source
      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.