Commit 2024-10-16 18:15 ede77585

View on Github →

feat(AlgebraicGeometry): Classification of Spec R ⟶ X with R local. (#15240)

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem LocalRing.closed_point_mem_iff

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Spec_closedPoint

Modified Mathlib/AlgebraicGeometry/Stalk.lean

added theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk

added theorem AlgebraicGeometry.Scheme.Spec_fromSpecStalk'

added theorem AlgebraicGeometry.Scheme.Spec_fromSpecStalk

added theorem AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk

added theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk

added theorem AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk

added theorem AlgebraicGeometry.Scheme.fromSpecStalk_app

added theorem AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint

added theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo

added theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec

added theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk

added theorem AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem

added theorem AlgebraicGeometry.Scheme.range_fromSpecStalk

added def AlgebraicGeometry.Scheme.stalkClosedPointTo

added theorem AlgebraicGeometry.Scheme.stalkClosedPointTo_comp

added theorem AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk

added def AlgebraicGeometry.SpecToEquivOfLocalRing

added theorem AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff

added theorem AlgebraicGeometry.Spec_stalkClosedPointIso

added theorem AlgebraicGeometry.germ_stalkClosedPointIso_hom

added def AlgebraicGeometry.stalkClosedPointIso

added theorem AlgebraicGeometry.stalkClosedPointIso_inv

added theorem AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv