Commit 2026-06-24 14:59 9ca31d8b

View on Github →

feat(AlgebraicGeometry): Scheme.Hom.opensFunctor preserves 1-hypercovers (#40990) We deduce this from the fact that it preserves pullbacks, which we deduce from general facts about thin categories.

Estimated changes

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.appIso_hom_naturality

added theorem AlgebraicGeometry.Scheme.Hom.coverPreserving_opensFunctor

added def AlgebraicGeometry.Scheme.Hom.opensFunctorAdjunction

Modified Mathlib/CategoryTheory/Discrete/Basic.lean

added theorem CategoryTheory.Discrete.as_bijective

added theorem CategoryTheory.Discrete.range_functor

Modified Mathlib/CategoryTheory/Limits/Preorder.lean

added def Preorder.isColimitISup

added def Preorder.isLimitIInf

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

added def CategoryTheory.Limits.isColimitEquivCofanOfIsThin

added def CategoryTheory.Limits.isLimitEquivFanOfIsThin

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

added theorem CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin

added theorem CategoryTheory.isPushout_iff_isColimit_binaryCofan_of_isThin

Modified Mathlib/Topology/Category/TopCat/Opens.lean

added theorem Topology.IsOpenEmbedding.functor_obj_iInf

Modified Mathlib/Topology/Sets/Opens.lean

added theorem TopologicalSpace.Opens.coe_iInf