Commit 2026-05-29 00:22 3b9b4dca

View on Github →

refactor(CategoryTheory): redefine MorphismProperty.IsLocalAtTarget in terms of presieves (#39978) This changes the definition slightly: The condition is now required for covers indexed in Type max u v, while before this PR it was only required for index types in Type v. Requested in review of #32046.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

modified def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover

modified theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange

modified theorem AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/LocalClosure.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

modified def AlgebraicGeometry.Scheme.OpenCover.restrict

Modified Mathlib/CategoryTheory/MorphismProperty/Local.lean

added theorem CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff_of_zeroHypercover

added theorem CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_small

added theorem CategoryTheory.MorphismProperty.IsLocalAtSource.of_zeroHypercover

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_forall_pullbackSnd

modified theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff_of_zeroHypercover

modified theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small

modified theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_le

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover

deleted theorem CategoryTheory.MorphismProperty.of_zeroHypercover_source

deleted theorem CategoryTheory.MorphismProperty.of_zeroHypercover_target