Mathlib Changelog
Changelog
About
Github
Commit
2021-06-16 04:52
b8658928
View on Github →
feat(algebraic_geometry/Spec): Make Spec a functor. (
#7790
)
Estimated changes
Modified
src/algebraic_geometry/Scheme.lean
modified
def
algebraic_geometry.Scheme.Spec
added
def
algebraic_geometry.Scheme.Spec_map
added
theorem
algebraic_geometry.Scheme.Spec_map_comp
added
theorem
algebraic_geometry.Scheme.Spec_map_id
added
def
algebraic_geometry.Scheme.Spec_obj
added
theorem
algebraic_geometry.Scheme.Spec_obj_to_LocallyRingedSpace
Modified
src/algebraic_geometry/Spec.lean
deleted
def
algebraic_geometry.Spec.LocallyRingedSpace
added
def
algebraic_geometry.Spec.LocallyRingedSpace_map
added
theorem
algebraic_geometry.Spec.LocallyRingedSpace_map_comp
added
theorem
algebraic_geometry.Spec.LocallyRingedSpace_map_id
added
def
algebraic_geometry.Spec.LocallyRingedSpace_obj
deleted
def
algebraic_geometry.Spec.PresheafedSpace
deleted
def
algebraic_geometry.Spec.SheafedSpace
added
def
algebraic_geometry.Spec.SheafedSpace_map
added
theorem
algebraic_geometry.Spec.SheafedSpace_map_comp
added
theorem
algebraic_geometry.Spec.SheafedSpace_map_id
added
def
algebraic_geometry.Spec.SheafedSpace_obj
added
def
algebraic_geometry.Spec.Top_map
added
theorem
algebraic_geometry.Spec.Top_map_comp
added
theorem
algebraic_geometry.Spec.Top_map_id
added
def
algebraic_geometry.Spec.Top_obj
added
def
algebraic_geometry.Spec.to_LocallyRingedSpace
added
def
algebraic_geometry.Spec.to_PresheafedSpace
added
theorem
algebraic_geometry.Spec.to_PresheafedSpace_map
added
theorem
algebraic_geometry.Spec.to_PresheafedSpace_map_op
added
theorem
algebraic_geometry.Spec.to_PresheafedSpace_obj
added
theorem
algebraic_geometry.Spec.to_PresheafedSpace_obj_op
added
def
algebraic_geometry.Spec.to_SheafedSpace
added
def
algebraic_geometry.Spec.to_Top
added
theorem
algebraic_geometry.local_ring_hom_comp_stalk_iso
added
theorem
algebraic_geometry.stalk_map_to_stalk