Commit 2021-10-01 12:27 c33407ae

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.