Mathlib Changelog
v3
Changelog
About
Github
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