feat(algebraic_geometry/*): Proved Spec ⋙ Γ ≅ 𝟭 (#9416)
- Specialied `algebraic_geometry.structure_sheaf.basic_open_iso` into global sections, proving that the map `structure_sheaf.to_open R ⊤` is an isomorphism in `algebraic_geometry.is_iso_to_global`.
- Proved that the map `R ⟶ Γ(Spec R)` is natural, and presents the fact above as an natural isomorphism `Spec.right_op ⋙ Γ ≅ 𝟭 _` in `algebraic_geometry.Spec_Γ_identity`.
Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
