Mathlib Changelog
v3
Changelog
About
Github
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