Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 13:04 011a5998

View on Github →

feat(algebraic_geometry): Gluing morphisms from an open cover. (#11441)

Estimated changes

Modified src/algebraic_geometry/gluing.lean

added def algebraic_geometry.Scheme.glue_data.open_cover

added def algebraic_geometry.Scheme.open_cover.from_glued

added theorem algebraic_geometry.Scheme.open_cover.from_glued_injective

added theorem algebraic_geometry.Scheme.open_cover.from_glued_open_embedding

added theorem algebraic_geometry.Scheme.open_cover.from_glued_open_map

added def algebraic_geometry.Scheme.open_cover.glue_morphisms

added def algebraic_geometry.Scheme.open_cover.glued_cover

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_cocycle

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_cocycle_fst

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_cocycle_snd

added def algebraic_geometry.Scheme.open_cover.glued_cover_t'

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_fst_fst

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_fst_snd

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_snd_fst

added theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_snd_snd

added theorem algebraic_geometry.Scheme.open_cover.ι_from_glued

added theorem algebraic_geometry.Scheme.open_cover.ι_glue_morphisms