Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 07:23 6050f9df

View on Github →

feat(algebraic_geometry, category_theory): SheafedSpace has colimits (#10401)

Estimated changes

Modified src/algebraic_geometry/sheafed_space.lean

Modified src/category_theory/limits/creates.lean

added def category_theory.creates_colimit_of_fully_faithful_of_iso

added def category_theory.creates_colimit_of_fully_faithful_of_lift

Modified src/topology/sheaves/limits.lean

added theorem Top.is_sheaf_of_is_limit

added theorem Top.limit_is_sheaf

Modified src/topology/sheaves/sheaf_condition/sites.lean

added def Top.presheaf.Sheaf_spaces_equiv_sheaf_sites

added def Top.presheaf.Sheaf_spaces_equiv_sheaf_sites_functor_forget

added def Top.presheaf.Sheaf_spaces_equiv_sheaf_sites_inverse_forget

deleted def Top.presheaf.Sheaf_spaces_equivelence_sheaf_sites