Commit 2025-09-27 10:51 ab29df34

View on Github →

feat(AlgebraicGeometry): inverse limits and schemes of finite type (#25941) We prove the following: Given a cofiltered diagram D of quasi-compact S-schemes with affine transition maps, and another scheme X of finite type over S. Then the canonical map colim Homₛ(Dᵢ, X) ⟶ Homₛ(lim Dᵢ, X) is injective.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

added def AlgebraicGeometry.ExistsHomHomCompEqCompAux.D'

added def AlgebraicGeometry.ExistsHomHomCompEqCompAux.c'

added theorem AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq

added theorem AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index

added def AlgebraicGeometry.ExistsHomHomCompEqCompAux.g

added def AlgebraicGeometry.ExistsHomHomCompEqCompAux.hc'

added def AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii'

added def AlgebraicGeometry.ExistsHomHomCompEqCompAux.i'

added theorem AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset

added structure AlgebraicGeometry.ExistsHomHomCompEqCompAux

added theorem AlgebraicGeometry.Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType

added theorem AlgebraicGeometry.Scheme.nonempty_of_isLimit

added theorem AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty'

added theorem AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty

deleted theorem Scheme.nonempty_of_isLimit

deleted theorem exists_mem_of_isClosed_of_nonempty'

deleted theorem exists_mem_of_isClosed_of_nonempty

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

added def CategoryTheory.Over.conePost

added def CategoryTheory.Over.conePostIso

added def CategoryTheory.Over.isLimitConePost

Modified Mathlib/CategoryTheory/Limits/Creates.lean

added theorem CategoryTheory.liftedLimitMapsToOriginal_hom_π