Commit 2024-10-19 19:57 fee48cc3

View on Github →

feat(AlgebraicGeometry/ResidueField): classification of Spec K ⟶ X with K a field (#17768) This PR adds more API for residue fields and in particular the classification of morphisms Spec K ⟶ X with K a field. From the valuative criterion project.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

added theorem AlgebraicGeometry.IsPreimmersion.Spec_map_iff

added theorem AlgebraicGeometry.IsPreimmersion.mk_Spec_map

added theorem AlgebraicGeometry.IsPreimmersion.of_isLocalization

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

added theorem AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField

added theorem AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr

added def AlgebraicGeometry.Scheme.SpecToEquivOfField

added theorem AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff

added theorem AlgebraicGeometry.Scheme.Spec_map_residue_apply

added def AlgebraicGeometry.Scheme.descResidueField

added theorem AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField

added theorem AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField

added theorem AlgebraicGeometry.Scheme.fromSpecResidueField_apply

added theorem AlgebraicGeometry.Scheme.range_fromSpecResidueField

added theorem AlgebraicGeometry.Scheme.residue_descResidueField

Modified Mathlib/AlgebraicGeometry/Stalk.lean