Commit 2024-10-17 09:39 c199a0e2

View on Github →

feat(AlgebraicGeometry): closed immersions with affine target (#15038) Shows that closed immersions are affine morphisms inducing affine locally surjective maps on sections.

Estimated changes

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

added theorem CategoryTheory.Iso.commRingIsoToRingEquiv_apply

added theorem CategoryTheory.Iso.commRingIsoToRingEquiv_symm_apply

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

added theorem pow_mul_eq_zero_of_le

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.stalkMap_injective

added theorem AlgebraicGeometry.stalkMap_injective_of_isAffine

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine

added theorem AlgebraicGeometry.IsClosedImmersion.isIso_of_injective_of_isAffine

added theorem AlgebraicGeometry.IsClosedImmersion.stableUnderBaseChange

added theorem AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective

added theorem AlgebraicGeometry.surjective_of_isClosed_range_of_injective

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

added theorem AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot

added theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.exists_of_res_eq_of_qcqs

added theorem AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top

added theorem AlgebraicGeometry.exists_of_res_zero_of_qcqs

added theorem AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

added theorem AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero

added theorem AlgebraicGeometry.Scheme.Γevaluation_naturality

added theorem AlgebraicGeometry.Scheme.Γevaluation_naturality_apply

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero

Modified Mathlib/Geometry/RingedSpace/Basic.lean

added theorem AlgebraicGeometry.RingedSpace.exists_res_eq_zero_of_germ_eq_zero

added theorem AlgebraicGeometry.RingedSpace.res_zero

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero

Modified Mathlib/RingTheory/Localization/Defs.lean

added theorem IsLocalization.injective_iff_map_algebraMap_eq

added theorem IsLocalization.injective_of_map_algebraMap_zero

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

added theorem TopCat.isIso_of_bijective_of_isClosedMap

added theorem TopCat.isIso_of_bijective_of_isOpenMap

Modified Mathlib/Topology/Homeomorph.lean

added def Homeomorph.homeomorphOfContinuousClosed