Commit 2024-10-03 17:24 1a4c6bcc

View on Github →

feat(AlgebraicGeometry): Residue fields of schemes. (#15333)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/ResidueField.lean

added def AlgebraicGeometry.Scheme.Hom.residueFieldMap

added def AlgebraicGeometry.Scheme.evaluation

added theorem AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_not_mem_basicOpen

added theorem AlgebraicGeometry.Scheme.evaluation_naturality

added theorem AlgebraicGeometry.Scheme.evaluation_naturality_apply

added theorem AlgebraicGeometry.Scheme.evaluation_ne_zero_iff_mem_basicOpen

added def AlgebraicGeometry.Scheme.fromSpecResidueField

added theorem AlgebraicGeometry.Scheme.germ_residue

added def AlgebraicGeometry.Scheme.residue

added def AlgebraicGeometry.Scheme.residueField

added def AlgebraicGeometry.Scheme.residueFieldCongr

added theorem AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField

added theorem AlgebraicGeometry.Scheme.residueFieldCongr_inv

added theorem AlgebraicGeometry.Scheme.residueFieldCongr_refl

added theorem AlgebraicGeometry.Scheme.residueFieldCongr_symm

added theorem AlgebraicGeometry.Scheme.residueFieldCongr_trans

added theorem AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom

added theorem AlgebraicGeometry.Scheme.residueFieldMap_comp

added theorem AlgebraicGeometry.Scheme.residueFieldMap_id

added theorem AlgebraicGeometry.Scheme.residue_residueFieldCongr

added theorem AlgebraicGeometry.Scheme.residue_residueFieldMap

added theorem AlgebraicGeometry.Scheme.residue_surjective