Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 07:10 6bd6b45e

View on Github →

feat(algebraic_geometry): Isomorphisms of presheafed space. (#10461)

Estimated changes

Modified src/algebraic_geometry/Spec.lean

Modified src/algebraic_geometry/presheafed_space.lean

modified theorem algebraic_geometry.PresheafedSpace.comp_c_app

added theorem algebraic_geometry.PresheafedSpace.is_iso_of_components

added def algebraic_geometry.PresheafedSpace.iso_of_components

added def algebraic_geometry.PresheafedSpace.sheaf_iso_of_iso

Modified src/algebraic_geometry/presheafed_space/has_colimits.lean

Modified src/category_theory/limits/has_limits.lean

modified theorem category_theory.limits.colimit.pre_desc

Modified src/topology/category/Top/opens.lean

added def topological_space.opens.map_map_iso

Modified src/topology/sheaves/presheaf.lean

added def Top.presheaf.presheaf_equiv_of_iso

added def Top.presheaf.pullback_hom_iso_pushforward_inv

added def Top.presheaf.pullback_inv_iso_pushforward_hom

added theorem Top.presheaf.pullback_obj_eq_pullback_obj

added def Top.presheaf.pushforward_to_of_iso

added theorem Top.presheaf.pushforward_to_of_iso_app

added def Top.presheaf.to_pushforward_of_iso

added theorem Top.presheaf.to_pushforward_of_iso_app