On free abelian categories for theorem proving

Abstract: Computing explicitly within a free mathematical object can be interpreted as theorem proving. In this talk, we discuss the constructiveness of free abelian categories. A very concrete description of free abelian categories was given by Murray Adelman, and we demonstrate how his description can be employed to validate homological lemmata like the Snake lemma computationally.

rings and algebrasrepresentation theory

Audience: researchers in the topic

ONCAS Online Noncommutative Algebra Seminar

Series comments: This is an online seminar organized to keep the community of noncommutative algebraists connected during the pandemic which has made it difficult for everyone to travel. If you would like to attend these talks, please email to any of the organizers and you will be added to the mailing list.