Commit 2025-05-18 17:44 5b53d143

View on Github →

feat(AlgebraicGeometry): Inverse limit of nonempty schemes is nonempty (#24758)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Ring/FilteredColimits.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Created Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

added theorem Scheme.nonempty_of_isLimit

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

added def CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty

added def CategoryTheory.Limits.isLimitEquivIsTerminalOfIsEmpty