Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 09:35 7f06271e

View on Github →

feat(algebraic_geometry/limits): Empty scheme is initial. (#16086)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

deleted def algebraic_geometry.Scheme.empty

added def algebraic_geometry.Scheme.{u}

Created src/algebraic_geometry/limits.lean

added theorem algebraic_geometry.Scheme.empty_ext

added def algebraic_geometry.Scheme.empty_to

added theorem algebraic_geometry.Scheme.eq_empty_to

added def algebraic_geometry.Spec_Z_is_terminal

added def algebraic_geometry.Spec_punit_is_initial

added theorem algebraic_geometry.bot_is_affine_open

added def algebraic_geometry.empty_is_initial

added theorem algebraic_geometry.empty_is_initial_to

added def algebraic_geometry.is_initial_of_is_empty

Modified src/algebraic_geometry/open_immersion.lean

added theorem algebraic_geometry.is_iso_iff_is_open_immersion

added theorem algebraic_geometry.is_iso_iff_stalk_iso

added theorem algebraic_geometry.is_open_immersion.iff_stalk_iso

added theorem algebraic_geometry.is_open_immersion.of_stalk_iso

added theorem algebraic_geometry.is_open_immersion.to_iso

Modified src/category_theory/sites/sheaf.lean

added theorem category_theory.presheaf.is_sheaf_of_is_terminal