Commit 2026-01-07 00:18 3ad51856

View on Github →

feat(AlgebraicGeometry): universal property of relative normalization (#33476)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE

added theorem AlgebraicGeometry.eq_of_SpecMap_comp_eq_of_isAffineOpen

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

added theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage

Modified Mathlib/AlgebraicGeometry/Normalization.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage

deleted theorem AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage

added theorem AlgebraicGeometry.Scheme.Hom.normalization.hom_ext

added def AlgebraicGeometry.Scheme.Hom.normalizationDesc

added theorem AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp

added theorem AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc