Commit 2023-06-29 04:06 b62dfca8

View on Github →

feat: port AlgebraicGeometry.Gluing (#5446)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Gluing.lean

added def AlgebraicGeometry.Scheme.GlueData.Rel

added theorem AlgebraicGeometry.Scheme.GlueData.glue_condition

added def AlgebraicGeometry.Scheme.GlueData.gluedScheme

added theorem AlgebraicGeometry.Scheme.GlueData.isOpen_iff

added def AlgebraicGeometry.Scheme.GlueData.isoCarrier

added def AlgebraicGeometry.Scheme.GlueData.openCover

added def AlgebraicGeometry.Scheme.GlueData.vPullbackCone

added def AlgebraicGeometry.Scheme.GlueData.vPullbackConeIsLimit

added theorem AlgebraicGeometry.Scheme.GlueData.ι_eq_iff

added theorem AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv

added theorem AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv

added theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective

added structure AlgebraicGeometry.Scheme.GlueData

added def AlgebraicGeometry.Scheme.OpenCover.fromGlued

added theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_injective

added theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_openEmbedding

added theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_open_map

added def AlgebraicGeometry.Scheme.OpenCover.glueMorphisms

added def AlgebraicGeometry.Scheme.OpenCover.gluedCover

added def AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'

added theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_fst

added theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_snd

added theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_fst

added theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd

added theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle

added theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle_fst

added theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle_snd

added theorem AlgebraicGeometry.Scheme.OpenCover.hom_ext

added theorem AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued

added theorem AlgebraicGeometry.Scheme.OpenCover.ι_glueMorphisms

Modified Mathlib/AlgebraicGeometry/SheafedSpace.lean