Jujian Zhang
Jujian Zhang
We want to have a homeomorphism between $\mathrm{Proj}|_{D(f)}$ to $\mathrm{Spec}{A^0_f}$, we have the forward direction already. This PR is the underlying function of backward direction. Continuity will be proved separately....
--- - [x] depends on:#15672 [](https://gitpod.io/from-referrer/)
By imitating the current `graded_algebra`, this pr builds `graded_module` over some `graded algebra` Co-authored-by: Eric Wieser @eric-wieser - [x] depends on: #14626 - [x] depends on: #15654 --- [![Open in...
Given a ring homomorphism $f : R \to S$ between commutative rings, the extension of scalars functor from $R$-module to $S$-module. In #15564 it will proven that extension of scalars...
This PR defines divisible group and proves that the set of rationals is divisible and product of divisible group is divisible. Future PR will be opened to prove that divisibility...
This is definition "computes better", so it is needed when showing `from_Spec` and `to_Spec` are inverses - [x] depends on: #16693 --- [](https://gitpod.io/from-referrer/)
If $A, B$ are abelian categories and $L\dashv R$ is a pair of adjoint functors, where $L$ is faithful and exact, then enough invectiveness of $B$ implies that of $A$...
--- [](https://gitpod.io/from-referrer/)
Since injective groups are divisible and vice versa, we show `AddCommGroup` has enough "divisibles": for any group $A$, we embed $A$ into $\prod_{f : A \to \mathbb{Q}/\mathbb{Z}} \mathbb{Q}/\mathbb{Z}$, since $\mathbb{Q}/\mathbb{Z}$...
I defined the category of modules following [this link](https://ncatlab.org/nlab/show/Mod). This may or may not be useful to define sheaf of modules. --- [](https://gitpod.io/from-referrer/)