Commit 2025-07-24 07:37 909b3beb

View on Github →

feat(AlgebraicGeometry): codescent implies descent (#23547) Let P and P' be morphism properties of schemes. We show some results to deduce that P descends along P' from a codescent property of ring homomorphisms.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

added theorem AlgebraicGeometry.HasAffineProperty.SpecMap_iff_of_affineAnd

Created Mathlib/AlgebraicGeometry/Morphisms/Descent.lean

added theorem AlgebraicGeometry.IsLocalAtTarget.descendsAlong

added theorem AlgebraicGeometry.IsLocalAtTarget.descendsAlong_inf_quasiCompact

added theorem AlgebraicGeometry.IsStableUnderBaseChange.of_pullback_fst_of_isAffine

added theorem AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isLocalAtSource

added theorem AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong

Modified Mathlib/RingTheory/RingHomProperties.lean

added theorem RingHom.CodescendsAlong.algebraMap_tensorProduct

added theorem RingHom.CodescendsAlong.includeRight

added theorem RingHom.CodescendsAlong.mk

added def RingHom.CodescendsAlong