Commit 2026-02-06 11:03 fe7afa6e

View on Github →

feat(AlgebraicGeometry): replace PreservesLocalization with Coequifibered (#34701)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Normalization.lean

added theorem AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap

modified def AlgebraicGeometry.Scheme.Hom.normalization

added def AlgebraicGeometry.Scheme.Hom.normalizationGlueData

deleted theorem AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap

Modified Mathlib/AlgebraicGeometry/RelativeGluing.lean

added theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι

Modified Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean

deleted theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map

deleted def AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization

added theorem AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway

added theorem AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map

added def AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData

added def AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec

deleted theorem AlgebraicGeometry.Scheme.preservesLocalization_toOpensFunctor

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equifibered.lean

added theorem CategoryTheory.NatTrans.Coequifibered.rightOp

added theorem CategoryTheory.NatTrans.Equifibered.rightOp