Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-13 08:21 5d35e626

View on Github →

feat(algebraic_geometry/*): Gamma the global sections functor (#4126)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.Γ

added theorem algebraic_geometry.Scheme.Γ_def

added theorem algebraic_geometry.Scheme.Γ_map

added theorem algebraic_geometry.Scheme.Γ_map_op

added theorem algebraic_geometry.Scheme.Γ_obj

added theorem algebraic_geometry.Scheme.Γ_obj_op

Modified src/algebraic_geometry/locally_ringed_space.lean

added def algebraic_geometry.LocallyRingedSpace.Γ

added theorem algebraic_geometry.LocallyRingedSpace.Γ_def

added theorem algebraic_geometry.LocallyRingedSpace.Γ_map

added theorem algebraic_geometry.LocallyRingedSpace.Γ_map_op

added theorem algebraic_geometry.LocallyRingedSpace.Γ_obj

added theorem algebraic_geometry.LocallyRingedSpace.Γ_obj_op

Modified src/algebraic_geometry/presheafed_space.lean

added def algebraic_geometry.PresheafedSpace.Γ

added theorem algebraic_geometry.PresheafedSpace.Γ_map_op

added theorem algebraic_geometry.PresheafedSpace.Γ_obj_op

Modified src/algebraic_geometry/sheafed_space.lean

added def algebraic_geometry.SheafedSpace.Γ

added theorem algebraic_geometry.SheafedSpace.Γ_def

added theorem algebraic_geometry.SheafedSpace.Γ_map

added theorem algebraic_geometry.SheafedSpace.Γ_map_op

added theorem algebraic_geometry.SheafedSpace.Γ_obj

added theorem algebraic_geometry.SheafedSpace.Γ_obj_op

Modified src/topology/category/Top/opens.lean

added def topological_space.opens.bot_le

added def topological_space.opens.le_map_top

added def topological_space.opens.le_top