pseudoelements

Stream: maths

[Johan Commelin]

It seems to me that pseudoelements of an object X in an abelian category form a group. Is this true? Is it in mathlib? Can we endow homsets with an add_monoid_hom_class instance?

Is the following provable?

import category_theory.abelian.pseudoelements

open category_theory category_theory.limits
open_locale pseudoelement

 lemma pseudoelement.biprod_ext {X Y : A} (p q : ↥(X ⊞ Y))
   (h1 : (biprod.fst : X ⊞ Y ⟶ X) p = (biprod.fst : X ⊞ Y ⟶ X) q)
   (h2 : (biprod.snd : X ⊞ Y ⟶ Y) p = (biprod.snd : X ⊞ Y ⟶ Y) q) :
   p = q :=
sorry

[Johan Commelin]

@Markus Himmel I guess you have thought about such issues. I read a comment that doing pullbacks is hairy...

[Adam Topaz]

The proper way to do what I'm guessing you want is to prove the Freyd embedding theorem.

[Adam Topaz]

But maybe there is a more direct way with pseudoelements.... I don't know.

[Riccardo Brasca]

You can often use docs#category_theory.abelian.pseudoelement.sub_of_eq_image to "mimic" the difference of two pseudoelements.

[Riccardo Brasca]

It was enough to prove the snake lemma, where on paper one would take the difference (at least in R-mod).

[Markus Himmel]

The equivalence relation on the homs with codomain P is not compatible with addition-after-taking-pullbacks, so you cannot make the pseudoelements into an abelian group.

One way to fix this is by not quotienting out the equivalence relation, but then you have to do all the bookkeeping manually. This technique is described in https://math.berkeley.edu/~gbergman/papers/unpub/elem-chase.pdf

[Johan Commelin]

Hmm, I will try to work out what goes wrong, because I don't see it yet.

[Adam Topaz]

The relation involves some epi assumptions. Does that throw a wrench in things?

[Johan Commelin]

I guess the problem is with negation? Becuase $f \oplus (-f) \colon X \oplus X \to Y$ is not equivalent to the zero map?

[Johan Commelin]

I haven't written lean code yet, but getting a monoid seems to be ok

[Adam Topaz]

What about associativity of addition?

[Johan Commelin]

I think that should be fine, since $(X \oplus Y) \oplus Z \cong X \oplus (Y \oplus Z)$. The problem is axioms that reduce arity. Afaict.

[Adam Topaz]

Yeah that's right.

[Adam Topaz]

You would take that isomorphism as your epi

[Markus Himmel]

$f \oplus (-f)$ cannot be equivalent to the zero map unless $f = 0$ since the only things that are equivalent to zero maps are zero maps. See docs#category_theory.abelian.pseudoelement.pseudo_zero_aux

[Kevin Buzzard]

Aah so maybe it's a monoid :-)

[Johan Commelin]

So here's a lemma that I've been trying to prove using pseudoelements, but I failed so far:
https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/derived/les.lean#L128

I would be interested in seeing a proof that works. Because I think that a proof without pseudoelements will quickly be ugly.