Commit 2025-12-28 17:51 f7ff0742

View on Github →

feat(AlgebraicGeometry): relative normalization of schemes (#32813)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_iSup_eq_top

Created Mathlib/AlgebraicGeometry/Normalization.lean

added def AlgebraicGeometry.Scheme.Hom.fromNormalization

added theorem AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage

added theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage

added theorem AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage

added theorem AlgebraicGeometry.Scheme.Hom.ker_toNormalization

added def AlgebraicGeometry.Scheme.Hom.normalization

added def AlgebraicGeometry.Scheme.Hom.normalizationDiagram

added def AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap

added def AlgebraicGeometry.Scheme.Hom.normalizationOpenCover

added theorem AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap

added def AlgebraicGeometry.Scheme.Hom.toNormalization

added theorem AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage

added theorem AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization

added theorem AlgebraicGeometry.Scheme.Hom.ι_fromNormalization

added theorem AlgebraicGeometry.Scheme.Hom.ι_toNormalization

Modified Mathlib/AlgebraicGeometry/Properties.lean

added theorem AlgebraicGeometry.IsReduced.of_openCover