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