Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-18 20:44
0ccda7e9
View on Github →
feat(AlgebraicGeometry): scheme-theoretic fibre (
#19427
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/AlgebraicGeometry/Fiber.lean
added
theorem
AlgebraicGeometry.IsFinite.finite_preimage_singleton
added
theorem
AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton
added
def
AlgebraicGeometry.Scheme.Hom.asFiber
added
def
AlgebraicGeometry.Scheme.Hom.fiber
added
def
AlgebraicGeometry.Scheme.Hom.fiberHomeo
added
theorem
AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply
added
def
AlgebraicGeometry.Scheme.Hom.fiberOverSpecResidueField
added
def
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
added
theorem
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply
added
def
AlgebraicGeometry.Scheme.Hom.fiberι
added
theorem
AlgebraicGeometry.Scheme.Hom.fiberι_asFiber
added
theorem
AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm
added
theorem
AlgebraicGeometry.Scheme.Hom.finite_preimage
added
theorem
AlgebraicGeometry.Scheme.Hom.range_fiberι
Modified
Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
deleted
theorem
AlgebraicGeometry.isAffineHom_isStableUnderBaseChange
Modified
Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean