Commit 2023-05-26 23:07 cff244bf

View on Github →

feat: port AlgebraicGeometry.SheafedSpace (#4405)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/SheafedSpace.lean

added theorem AlgebraicGeometry.SheafedSpace.comp_base

added theorem AlgebraicGeometry.SheafedSpace.comp_c_app'

added theorem AlgebraicGeometry.SheafedSpace.comp_c_app

added theorem AlgebraicGeometry.SheafedSpace.congr_app

added def AlgebraicGeometry.SheafedSpace.forget

added def AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

added theorem AlgebraicGeometry.SheafedSpace.id_base

added theorem AlgebraicGeometry.SheafedSpace.id_c

added theorem AlgebraicGeometry.SheafedSpace.id_c_app

added theorem AlgebraicGeometry.SheafedSpace.mk_coe

added def AlgebraicGeometry.SheafedSpace.restrict

added def AlgebraicGeometry.SheafedSpace.restrictTopIso

added def AlgebraicGeometry.SheafedSpace.sheaf

added def AlgebraicGeometry.SheafedSpace.unit

added def AlgebraicGeometry.SheafedSpace.Γ

added theorem AlgebraicGeometry.SheafedSpace.Γ_def

added theorem AlgebraicGeometry.SheafedSpace.Γ_map

added theorem AlgebraicGeometry.SheafedSpace.Γ_map_op

added theorem AlgebraicGeometry.SheafedSpace.Γ_obj

added theorem AlgebraicGeometry.SheafedSpace.Γ_obj_op

added structure AlgebraicGeometry.SheafedSpace