Commit 2026-02-06 16:14 e83debb9

View on Github →

feat(AlgebraicGeometry): quasi-finite morphisms have finite fibers (#34898)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Fiber.lean

deleted theorem AlgebraicGeometry.IsFinite.finite_preimage_singleton

deleted theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton

added def AlgebraicGeometry.Scheme.Hom.asFiberHom

added theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_apply

added theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField

added theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι

deleted theorem AlgebraicGeometry.Scheme.Hom.finite_preimage

added theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton

added theorem AlgebraicGeometry.Scheme.Hom.range_asFiberHom

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

added theorem AlgebraicGeometry.Scheme.Hom.finite_preimage

added theorem AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton

added theorem AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage

added theorem AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton

added theorem AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite

added theorem AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton

added theorem AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

added theorem AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv

added def AlgebraicGeometry.Scheme.Spec.residueFieldIso

added theorem AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom

Modified Mathlib/AlgebraicGeometry/Stalk.lean

deleted theorem AlgebraicGeometry.Scheme.Spec_fromSpecStalk'

deleted theorem AlgebraicGeometry.Scheme.Spec_fromSpecStalk

added theorem AlgebraicGeometry.Spec.algebraMap_stalkIso_inv

added theorem AlgebraicGeometry.Spec.fromSpecStalk_eq'

added theorem AlgebraicGeometry.Spec.fromSpecStalk_eq

added theorem AlgebraicGeometry.Spec.germ_stalkMapIso_hom

added def AlgebraicGeometry.Spec.stalkIso