As of May 31, 2023, we have updated our Code of Conduct.

New answers tagged

0 votes

Exact sequences with two FL-modules

Yes, this is true. Let $K_0(R)$ be the Grothendieck group of $R$ and $\widetilde K_0(R)=K_0(R)/\langle [R]\rangle$. Then $[P]=0$ in $\widetilde K_0(R)$ if and only if $P$ is stably free. For any $...
Andrei Jaikin's user avatar
7 votes

How to make Ext and Tor constructive?

Jarl Flaten and I have developed the theory of Ext groups constructively in homotopy type theory, and have formalized most of the results in Coq. We use Yoneda's resolution-free approach to Ext, so ...
Dan Christensen's user avatar

Top 50 recent answers are included