New answers tagged modules
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 $...
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 ...
Top 50 recent answers are included