Commit 2025-10-27 22:34 0a7fab8b

View on Github →

feat(AlgebraicGeometry): global sections of inverse limits of schemes (#30226)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

added theorem AlgebraicGeometry.Scheme.compactSpace_of_isLimit

added theorem AlgebraicGeometry.exists_appTop_map_eq_zero_of_isAffine_of_isLimit

added theorem AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit

added theorem AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit

added theorem AlgebraicGeometry.exists_appTop_π_eq_of_isLimit

added theorem AlgebraicGeometry.exists_app_map_eq_map_of_isLimit

added theorem AlgebraicGeometry.exists_app_map_eq_zero_of_isLimit

added theorem AlgebraicGeometry.exists_map_eq_top

added theorem AlgebraicGeometry.isAffineHom_π_app

added def AlgebraicGeometry.isLimitOpensCone

added theorem AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone

added def AlgebraicGeometry.opensCone

added def AlgebraicGeometry.opensDiagram

added def AlgebraicGeometry.opensDiagramι

Modified Mathlib/AlgebraicGeometry/Limits.lean

added theorem AlgebraicGeometry.Scheme.isAffine_of_isLimit

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.isPullback

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Connected.lean

added def CategoryTheory.Limits.isColimitOfIsPushoutOfIsConnected

added def CategoryTheory.Limits.isLimitOfIsPullbackOfIsConnected