Structure sheaf of graded ring

[jjaassoonn]

Defined structure sheaf of graded ring by copying and pasting structure_sheaf.lean

---

• depends on: feat(ring_theory/graded_algebra/homogeneous_ideal): homogenous ideals of a graded algebras #9717

[github-actions]

This PR/issue depends on:

• feat(ring_theory/graded_algebra/homogeneous_ideal): homogenous ideals of a graded algebras #9717
  By Dependent Issues (🤖). Happy coding!

[jjaassoonn]

This now can be compiled by github action. But I have changed deterministic time limit from 100000 to 150000. Locally on my machine, I set the time limit as 800000, so it has been improved greatly, but I couldn't get the final 50000 to go away. The two proof isos.sheaf_component.backward_forward and isos.sheaf_component.forward_backward are both splitted into small lemmas and are about 100 lines long each, but they still takes more than 10s.

I changed compile time to 200000, after changing universe level to arbitrary, the original 15000 doesn't work anymore.