Commit 2025-10-25 17:18 b07925bb

View on Github →

feat(AlgebraicGeometry): quasi-affine if covered by affine basic opens of global sections (#30286)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

added theorem AlgebraicGeometry.Scheme.ker_toSpecΓ

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

deleted theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen_aux

added theorem AlgebraicGeometry.isRetrocompact_basicOpen

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_source_exists_preimage

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

modified theorem AlgebraicGeometry.IsImmersion.of_comp

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/QuasiAffine.lean

added theorem AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen

added theorem AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpen

added theorem AlgebraicGeometry.Scheme.IsQuasiAffine.of_isAffineHom

Modified Mathlib/Topology/Constructible.lean

added theorem QuasiSeparatedSpace.of_isOpenCover