Commit 2023-06-23 04:14 ac0bfee7

View on Github →

feat: port AlgebraicGeometry.PresheafedSpace.Gluing (#5356)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean

Created Mathlib/AlgebraicGeometry/PresheafedSpace/Gluing.lean

added def AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit

added theorem AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv

added theorem AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective

added structure AlgebraicGeometry.LocallyRingedSpace.GlueData

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app

added def AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app'

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app'

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app

added def AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit

added def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π

added def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id

added theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π

added structure AlgebraicGeometry.PresheafedSpace.GlueData

added def AlgebraicGeometry.SheafedSpace.GlueData.vPullbackConeIsLimit

added theorem AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv

added theorem AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective

added structure AlgebraicGeometry.SheafedSpace.GlueData