Commit 2023-06-02 15:12 5b9ce13e

View on Github →

feat: port AlgebraicGeometry.LocallyRingedSpace (#4589)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean

added structure AlgebraicGeometry.LocallyRingedSpace.Hom

added theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero

added def AlgebraicGeometry.LocallyRingedSpace.comp

added theorem AlgebraicGeometry.LocallyRingedSpace.comp_val

added theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c

added theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c_app

added def AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

added def AlgebraicGeometry.LocallyRingedSpace.forgetToTop

added def AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso

added def AlgebraicGeometry.LocallyRingedSpace.id

added def AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso

added def AlgebraicGeometry.LocallyRingedSpace.ofRestrict

added theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen

added def AlgebraicGeometry.LocallyRingedSpace.restrict

added def AlgebraicGeometry.LocallyRingedSpace.restrictTopIso

added def AlgebraicGeometry.LocallyRingedSpace.toRingedSpace

added def AlgebraicGeometry.LocallyRingedSpace.toTopCat

added def AlgebraicGeometry.LocallyRingedSpace.Γ

added theorem AlgebraicGeometry.LocallyRingedSpace.Γ_def

added theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map

added theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map_op

added theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj

added theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op

added def AlgebraicGeometry.LocallyRingedSpace.𝒪

added structure AlgebraicGeometry.LocallyRingedSpace