Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 06:28 d2484474

View on Github →

feat(algebraic_geometry): Gluing schemes (#11431)

Estimated changes

Created src/algebraic_geometry/gluing.lean

added def algebraic_geometry.Scheme.glue_data.V_pullback_cone

added def algebraic_geometry.Scheme.glue_data.V_pullback_cone_is_limit

added theorem algebraic_geometry.Scheme.glue_data.glue_condition

added def algebraic_geometry.Scheme.glue_data.glued

added def algebraic_geometry.Scheme.glue_data.glued_Scheme

added theorem algebraic_geometry.Scheme.glue_data.is_open_iff

added def algebraic_geometry.Scheme.glue_data.iso_LocallyRingedSpace

added def algebraic_geometry.Scheme.glue_data.iso_carrier

added def algebraic_geometry.Scheme.glue_data.rel

added def algebraic_geometry.Scheme.glue_data.to_LocallyRingedSpace_glue_data

added def algebraic_geometry.Scheme.glue_data.ι

added theorem algebraic_geometry.Scheme.glue_data.ι_eq_iff

added theorem algebraic_geometry.Scheme.glue_data.ι_iso_LocallyRingedSpace_inv

added theorem algebraic_geometry.Scheme.glue_data.ι_iso_carrier_inv

added theorem algebraic_geometry.Scheme.glue_data.ι_jointly_surjective

added structure algebraic_geometry.Scheme.glue_data

Modified src/algebraic_geometry/presheafed_space.lean

added theorem algebraic_geometry.PresheafedSpace.coe_to_fun_eq

Modified src/algebraic_geometry/presheafed_space/gluing.lean

added def algebraic_geometry.LocallyRingedSpace.glue_data.V_pullback_cone_is_limit

added def algebraic_geometry.LocallyRingedSpace.glue_data.iso_SheafedSpace

added def algebraic_geometry.LocallyRingedSpace.glue_data.to_SheafedSpace_glue_data

added theorem algebraic_geometry.LocallyRingedSpace.glue_data.ι_iso_SheafedSpace_inv

added theorem algebraic_geometry.LocallyRingedSpace.glue_data.ι_jointly_surjective

added structure algebraic_geometry.LocallyRingedSpace.glue_data

deleted theorem algebraic_geometry.PresheafedSpace.coe_to_fun_eq

added def algebraic_geometry.PresheafedSpace.glue_data.V_pullback_cone_is_limit

added theorem algebraic_geometry.PresheafedSpace.glue_data.ι_jointly_surjective

added def algebraic_geometry.SheafedSpace.glue_data.V_pullback_cone_is_limit

added def algebraic_geometry.SheafedSpace.glue_data.iso_PresheafedSpace

added def algebraic_geometry.SheafedSpace.glue_data.to_PresheafedSpace_glue_data

added theorem algebraic_geometry.SheafedSpace.glue_data.ι_iso_PresheafedSpace_inv

added theorem algebraic_geometry.SheafedSpace.glue_data.ι_jointly_surjective

added structure algebraic_geometry.SheafedSpace.glue_data