Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 01:42 34b2a989

View on Github →

feat(algebraic_geometry/*): Preliminary lemmas for #16059 (#16060)

Estimated changes

Modified src/algebra/category/Ring/basic.lean

added theorem CommRing.comp_eq_ring_hom_comp

added theorem CommRing.ring_hom_comp_eq_comp

Modified src/algebraic_geometry/AffineScheme.lean

added def algebraic_geometry.AffineScheme.of

added def algebraic_geometry.AffineScheme.of_hom

added theorem algebraic_geometry.is_affine_open.map_restrict_basic_open

added theorem algebraic_geometry.is_affine_open_iff_of_is_open_immersion

added theorem algebraic_geometry.is_localization_of_eq_basic_open

Created src/algebraic_geometry/morphisms/ring_hom_properties.lean

added theorem ring_hom.respects_iso.basic_open_iff

added theorem ring_hom.respects_iso.basic_open_iff_localization

added theorem ring_hom.respects_iso.of_restrict_morphism_restrict_iff

added theorem ring_hom.stable_under_base_change.Γ_pullback_fst

Modified src/algebraic_geometry/open_immersion.lean

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

added theorem topological_space.opens.functor_obj_map_obj