Commit 2025-10-07 21:16 2634a31a

View on Github →

chore(AlgebraicGeometry): replace IsLocalAtTarget by IsZariskiLocalAtTarget (#30310) IsZariskiLocalAtTarget is an abbrev for MorphismProperty.IsLocalAtTarget Scheme.zariskiPrecoverage. The same is done for Source.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/AlgebraicGeometry/Cover/Sigma.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

deleted theorem AlgebraicGeometry.HasAffineProperty.isLocalAtSource

added theorem AlgebraicGeometry.HasAffineProperty.isZariskiLocalAtSource

deleted theorem AlgebraicGeometry.HasAffineProperty.of_isLocalAtTarget

added theorem AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget

deleted theorem AlgebraicGeometry.IsLocalAtSource.comp

deleted theorem AlgebraicGeometry.IsLocalAtSource.iff_exists_resLE

deleted theorem AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top

deleted theorem AlgebraicGeometry.IsLocalAtSource.iff_of_openCover

deleted theorem AlgebraicGeometry.IsLocalAtSource.isLocalAtTarget

deleted theorem AlgebraicGeometry.IsLocalAtSource.of_iSup_eq_top

deleted theorem AlgebraicGeometry.IsLocalAtSource.of_isOpenImmersion

deleted theorem AlgebraicGeometry.IsLocalAtSource.of_openCover

deleted theorem AlgebraicGeometry.IsLocalAtSource.resLE

deleted theorem AlgebraicGeometry.IsLocalAtSource.sigmaDesc

deleted theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top

deleted theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover

deleted theorem AlgebraicGeometry.IsLocalAtTarget.of_iSup_eq_top

deleted theorem AlgebraicGeometry.IsLocalAtTarget.of_isPullback

deleted theorem AlgebraicGeometry.IsLocalAtTarget.of_openCover

deleted theorem AlgebraicGeometry.IsLocalAtTarget.of_range_subset_iSup

deleted theorem AlgebraicGeometry.IsLocalAtTarget.restrict

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.comp

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.isZariskiLocalAtTarget

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.of_openCover

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.resLE

added theorem AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.of_range_subset_iSup

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.restrict

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

deleted theorem AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isLocalAtTarget

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget

deleted theorem AlgebraicGeometry.stalkwiseIsLocalAtTarget_of_respectsIso

added theorem AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso

deleted theorem AlgebraicGeometry.stalkwise_isLocalAtSource_of_respectsIso

added theorem AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso

deleted theorem AlgebraicGeometry.topologically_isLocalAtSource'

deleted theorem AlgebraicGeometry.topologically_isLocalAtSource

deleted theorem AlgebraicGeometry.topologically_isLocalAtTarget'

deleted theorem AlgebraicGeometry.topologically_isLocalAtTarget

added theorem AlgebraicGeometry.topologically_isZariskiLocalAtSource'

added theorem AlgebraicGeometry.topologically_isZariskiLocalAtSource

added theorem AlgebraicGeometry.topologically_isZariskiLocalAtTarget'

added theorem AlgebraicGeometry.topologically_isZariskiLocalAtTarget

deleted theorem AlgebraicGeometry.universally_isLocalAtSource

deleted theorem AlgebraicGeometry.universally_isLocalAtTarget

added theorem AlgebraicGeometry.universally_isZariskiLocalAtSource

added theorem AlgebraicGeometry.universally_isZariskiLocalAtTarget

Modified Mathlib/AlgebraicGeometry/Morphisms/Descent.lean

deleted theorem AlgebraicGeometry.IsLocalAtTarget.descendsAlong

deleted theorem AlgebraicGeometry.IsLocalAtTarget.descendsAlong_inf_quasiCompact

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact

deleted theorem AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isLocalAtSource

added theorem AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/LocalClosure.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/LocalIso.lean

deleted theorem AlgebraicGeometry.IsLocalIso.le_of_isLocalAtSource

added theorem AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

deleted theorem AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget

added theorem AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget

deleted theorem AlgebraicGeometry.HasRingHomProperty.of_isLocalAtSource_of_isLocalAtTarget

added theorem AlgebraicGeometry.HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Modified Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Local.lean

added theorem CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean