Commit 2024-07-03 06:10 17a95d6c

View on Github →

feat(AlgebraicGeometry): residue field of a point and evaluation (#14302) Defines the residue field of a point of a locally ringed space and the corresponding evaluation map.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap

added theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap_apply

Created Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

added def AlgebraicGeometry.LocallyRingedSpace.evaluation

added theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_not_mem_basicOpen

added theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality

added theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen

added def AlgebraicGeometry.LocallyRingedSpace.residueField

added def AlgebraicGeometry.LocallyRingedSpace.residueFieldMap

added theorem AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp

added theorem AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_id

added theorem AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue

added def AlgebraicGeometry.LocallyRingedSpace.Γevaluation

added theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_not_mem_basicOpen

added theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality

added theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen

Modified Mathlib/RingTheory/Ideal/LocalRing.lean

added theorem LocalRing.ker_residue

added theorem LocalRing.residue_eq_zero_iff

added theorem LocalRing.residue_ne_zero_iff_isUnit