Commit 2022-09-26 09:37 ebf8ff42

View on Github →

feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set. (#15259) 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.

Estimated changes

Modified src/algebraic_geometry/projective_spectrum/scheme.lean

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.add_mem

added def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_homogeneous_ideal

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.homogeneous

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.ne_top

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal.prime

added def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.denom_not_mem

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.relevant

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.smul_mem

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.zero_mem

added def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier

added theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff

added def algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.to_fun

added theorem algebraic_geometry.degree_zero_part.coe_one

added theorem algebraic_geometry.degree_zero_part.coe_sum