Commit 2022-07-11 14:26 b7626956

View on Github →

feat(algebraic_geometry/projective_spectrum): forward direction of homeomorphism between top_space of Proj and top_space of Spec (#13397) This pr is the start of showing that Proj is a scheme. In this pr, it will be shown that the locally on basic open set, there is a continuous function from the underlying topological space of Proj restricted to this open set to Spec of degree zero part of some localised ring. In the near future, it will be shown that this function is a homeomorphism.

Estimated changes

Modified src/algebraic_geometry/projective_spectrum/scheme.lean

added def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier_ne_top

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.disjoint

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier.clear_denominator

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.mem_carrier_iff

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.preimage_eq

added def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.to_fun

added def algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec

added theorem algebraic_geometry.degree_zero_part.coe_mul

modified def algebraic_geometry.degree_zero_part.deg

modified theorem algebraic_geometry.degree_zero_part.eq

deleted theorem algebraic_geometry.degree_zero_part.mul_val

modified def algebraic_geometry.degree_zero_part.num

modified theorem algebraic_geometry.degree_zero_part.num_mem

Modified src/algebraic_geometry/projective_spectrum/structure_sheaf.lean