Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 08:32 68fa0fd2

View on Github →

feat(src/algebraic_geometry/morphisms/open_immersion): New file (#17591)

Estimated changes

Created src/algebraic_geometry/morphisms/open_immersion.lean

added theorem algebraic_geometry.is_open_immersion.open_cover_iff

added theorem algebraic_geometry.is_open_immersion.open_cover_tfae

added theorem algebraic_geometry.is_open_immersion_iff_stalk

added theorem algebraic_geometry.is_open_immersion_is_local_at_target

added theorem algebraic_geometry.is_open_immersion_respects_iso

added theorem algebraic_geometry.is_open_immersion_stable_under_base_change

added theorem algebraic_geometry.is_open_immersion_stable_under_composition

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.morphism_restrict_stalk_map

added theorem algebraic_geometry.morphism_restrict_val_base

Modified src/topology/inseparable.lean

added theorem inseparable.of_eq

added theorem specializes_of_eq

Modified src/topology/sheaves/stalks.lean

added def Top.presheaf.stalk_congr

added theorem Top.presheaf.stalk_specializes_comp

added theorem Top.presheaf.stalk_specializes_refl