Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-11 21:18 61a04c51

View on Github →

feat(algebraic_geometry/structure_sheaf): Define comap on structure sheaf (#7788) Defines the comap of a ring homomorphism on the structure sheaves of the prime spectra.

Estimated changes

Modified src/algebraic_geometry/structure_sheaf.lean

modified def algebraic_geometry.stalk_iso

added def algebraic_geometry.structure_sheaf.comap

added theorem algebraic_geometry.structure_sheaf.comap_apply

added theorem algebraic_geometry.structure_sheaf.comap_comp

added theorem algebraic_geometry.structure_sheaf.comap_const

added def algebraic_geometry.structure_sheaf.comap_fun

added theorem algebraic_geometry.structure_sheaf.comap_fun_is_locally_fraction

added theorem algebraic_geometry.structure_sheaf.comap_id'

added theorem algebraic_geometry.structure_sheaf.comap_id

added theorem algebraic_geometry.structure_sheaf.comap_id_eq_map

added theorem algebraic_geometry.structure_sheaf.is_fraction.eq_mk'

modified def algebraic_geometry.to_open

deleted theorem algebraic_geometry.to_open_apply

added theorem algebraic_geometry.to_open_comp_comap