Commit 2025-01-30 15:54 344e1cfc

View on Github →

feat(AlgebraicGeometry): Π Rᵢ-points of schemes (#20494)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.Spec.preimage_comp

added theorem AlgebraicGeometry.Spec.preimage_id

Modified Mathlib/AlgebraicGeometry/Limits.lean

added theorem AlgebraicGeometry.isOpenImmersion_sigmaDesc

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.IsClosedImmersion.Spec_iff

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift

Created Mathlib/AlgebraicGeometry/PointsPi.lean

added theorem AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom

added theorem AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec

added theorem AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact

added theorem AlgebraicGeometry.isIso_of_comp_eq_sigmaSpec

added def AlgebraicGeometry.pointsPi

added theorem AlgebraicGeometry.pointsPi_injective

added theorem AlgebraicGeometry.pointsPi_surjective

added theorem AlgebraicGeometry.pointsPi_surjective_of_isAffine