Commit 2025-10-03 22:56 0607ff2a

View on Github →

feat(CategoryTheory/MorphismProperty): locality conditions (#30164) These are "upstreamed" from the corresponding definitions for morphism properties of schemes. The old definitions for schemes will be deprecated in a follow-up PR.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

Created Mathlib/CategoryTheory/MorphismProperty/Local.lean

added theorem CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover

added theorem CategoryTheory.MorphismProperty.IsLocalAtSource.of_le

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback

added theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_le

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

added def CategoryTheory.Precoverage.ZeroHypercover.weaken