mathlib

mathlib copied to clipboard

--- [](https://gitpod.io/from-referrer/)

erdOne

--- [](https://gitpod.io/from-referrer/)

erdOne

--- [](https://gitpod.io/from-referrer/)

erdOne

feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set.

2

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....

jjaassoonn

feat(algebraic_geometry/morphisms): Construct morphism properties from ring homomorphism properties

1

--- - [ ] depends on: #16060 [](https://gitpod.io/from-referrer/)

erdOne

The purpose of this PR is to carry out the solution mentioned [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/map.20from.20mult.20gp.20to.20add.20gp/near/292623869) to the unpleasantness that one has to explicitly invoke `of_add` and `to_add` when working with homomorphisms from...

MichaelStollBayreuth

--- - [x] depends on:#15672 [](https://gitpod.io/from-referrer/)

jjaassoonn

The structure is taken literally from `linear_algebra/matrix/bilinear_form` with generalizations and easier proofs where possible. --- [](https://gitpod.io/from-referrer/)

mcdoll

Add a lemma about the sign of the product of two numbers (in the `linear_ordered_ring` case, deduced from the existing `sign_hom` in that case). --- [](https://gitpod.io/from-referrer/)

jsm28

feat(algebra/module/graded_module): define graded module

5

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...

jjaassoonn