Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 16:11 df931664

View on Github →

feat(algebraic_geometry): Explicit description of the colimit of presheafed spaces. (#10466)

Estimated changes

Modified src/algebraic_geometry/presheafed_space/has_colimits.lean

added def algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit

added theorem algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit_hom_π

added theorem algebraic_geometry.PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit_inv_ι_app

added def algebraic_geometry.PresheafedSpace.componentwise_diagram