Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 17:10 c447a31c

View on Github →

feat(algebraic_geometry): Stalk is localization of affine open. (#11640)

Estimated changes

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

added theorem category_theory.iso.CommRing_iso_to_ring_equiv_symm_to_ring_hom

added theorem category_theory.iso.CommRing_iso_to_ring_equiv_to_ring_hom

Modified src/algebraic_geometry/AffineScheme.lean

added theorem algebraic_geometry.is_affine_open.from_Spec_prime_ideal_of

added theorem algebraic_geometry.is_affine_open.is_localization_stalk

added theorem algebraic_geometry.is_affine_open.is_localization_stalk_aux

added def algebraic_geometry.is_affine_open.prime_ideal_of

Modified src/algebraic_geometry/Scheme.lean

added theorem algebraic_geometry.Scheme.app_eq

added theorem algebraic_geometry.Scheme.id_app

added theorem algebraic_geometry.Scheme.id_coe_base

added theorem algebraic_geometry.Scheme.id_val_base

added theorem algebraic_geometry.Scheme.inv_val_c_app

Modified src/algebraic_geometry/Spec.lean

Modified src/algebraic_geometry/properties.lean

added theorem algebraic_geometry.is_integral_of_is_affine_is_domain

added theorem algebraic_geometry.is_reduced_of_is_affine_is_reduced

added theorem algebraic_geometry.reduce_to_affine_nbhd

Modified src/ring_theory/localization.lean

added theorem is_fraction_ring.is_fraction_ring_of_is_domain_of_is_localization

added theorem is_fraction_ring.is_fraction_ring_of_is_localization

added theorem is_fraction_ring.nontrivial

added theorem is_localization.map_non_zero_divisors_le

added theorem is_localization.mk'_eq_zero_iff

added theorem is_localization.non_zero_divisors_le_comap

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

added theorem topological_space.opens.adjunction_counit_app_self

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.stalk_open_algebra_map