Commit 2024-07-03 05:48 a708114c

View on Github →

feat(AlgebraicGeometry): zero locus of sections and characterisation of nilpotent elements (#14337) Introduces the zero locus of a set of sections on a ringed space and characterizes nilpotent sections over compact opens of a scheme in terms of basic opens and the zero locus.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

deleted theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top

added theorem AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine

added theorem AlgebraicGeometry.Scheme.toΓSpec_image_zeroLocus_eq_of_isAffine

added theorem AlgebraicGeometry.Scheme.toΓSpec_preimage_zeroLocus_eq

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

added theorem AlgebraicGeometry.Scheme.OpenCover.ext_elem

added theorem AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover

added theorem AlgebraicGeometry.Scheme.zero_of_zero_cover

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

deleted theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preim_basicOpen_eq

added theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq

added theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

added theorem AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact

added theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv

added def AlgebraicGeometry.IsOpenImmersion.ΓIso

added theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map

added theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_inv

added theorem AlgebraicGeometry.Scheme.Hom.appLE_invApp

added theorem AlgebraicGeometry.Scheme.Hom.image_le_image_of_le

added theorem AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter

added theorem AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange

added theorem AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE

added theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.zeroLocus_eq_top_iff

added theorem PrimeSpectrum.zeroLocus_iUnion₂

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.ιOpens_image_top

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.Hom.appLE_eq_app

added theorem AlgebraicGeometry.Scheme.basicOpen_appLE

added theorem AlgebraicGeometry.Scheme.basicOpen_pow

added theorem AlgebraicGeometry.Scheme.mem_zeroLocus_iff

modified theorem AlgebraicGeometry.Scheme.preimage_basicOpen

added def AlgebraicGeometry.Scheme.zeroLocus

added theorem AlgebraicGeometry.Scheme.zeroLocus_def

added theorem AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ

added theorem AlgebraicGeometry.Scheme.zeroLocus_isClosed

added theorem AlgebraicGeometry.Scheme.zeroLocus_singleton

Modified Mathlib/CategoryTheory/Category/Preorder.lean

added theorem CategoryTheory.eqToHom_comp_homOfLE

added theorem CategoryTheory.eqToHom_comp_homOfLE_op

added theorem CategoryTheory.homOfLE_comp_eqToHom

added theorem CategoryTheory.homOfLE_isIso_of_eq

added theorem CategoryTheory.homOfLE_op_comp_eqToHom

Modified Mathlib/Geometry/RingedSpace/Basic.lean

added theorem AlgebraicGeometry.RingedSpace.basicOpen_pow

added theorem AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff

added def AlgebraicGeometry.RingedSpace.zeroLocus

added theorem AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ

added theorem AlgebraicGeometry.RingedSpace.zeroLocus_isClosed

added theorem AlgebraicGeometry.RingedSpace.zeroLocus_singleton

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent

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

added theorem TopologicalSpace.Opens.map_homOfLE