[Merged by Bors] - feat(AlgebraicGeometry): zero locus of sections and characterisation of nilpotent elements

[chrisflav]

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.

Co-authored-by: Andrew Yang @erdOne

---

The Scheme.eq_of_eq_cover lemma and the IsOpenImmersion.ΓIso related things are due to Andrew.

I'd be happy to move the first two sections of the Nilpotents file somewhere else, but I did not find the canonical place.

[github-actions]

PR summary f47d21b577

Import changes

No significant changes to the import graph

---

Declarations diff

+ LocallyRingedSpace.toΓSpec_preim_basicOpen_eq
+ OpenCover.ext_elem
+ Scheme.eq_zeroLocus_of_isClosed_of_isAffine
+ Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact
+ Scheme.toΓSpec_image_zeroLocus_eq_of_isAffine
+ Scheme.toΓSpec_preimage_zeroLocus_eq
+ Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact
+ Scheme.ιOpens_appLE_isIso
+ Scheme.ιOpens_image_top
+ appLE_eq_app
+ appLE_invApp
+ basicOpen_appLE
+ basicOpen_eq_bot_of_isNilpotent
+ eqToHom_comp_homOfLE
+ eqToHom_comp_homOfLE_op
+ homOfLE_comp_eqToHom
+ homOfLE_isIso_of_eq
+ homOfLE_op_comp_eqToHom
+ homeomorph
+ image_le_image_of_le
+ image_preimage_eq_opensRange_inter
+ image_top_eq_opensRange
+ instance {X : Scheme.{u}} : Subsingleton Γ(X, ⊥)
+ isNilpotent_of_isNilpotent_cover
+ map_homOfLE
+ map_ΓIso_inv
+ opensFunctor_map_homOfLE
+ preimage_image_eq
+ toΓSpec_preimage_basicOpen_eq
+ toΓSpec_preimage_zeroLocus_eq
+ zeroLocus_def
+ zeroLocus_eq_top_iff
+ zeroLocus_iUnion₂
+ zero_of_zero_cover
+ ΓIso
+ ΓIso_hom_map
+ ΓIso_inv
++ basicOpen_pow
++ mem_zeroLocus_iff
++ zeroLocus
++ zeroLocus_empty_eq_univ
++ zeroLocus_isClosed
++ zeroLocus_singleton
- fromSpec_image_top
- toΓSpec_preim_basicOpen_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[chrisflav]

I ended up moving everything somewhere else, so I removed the new file again.

[chrisflav]

Thanks again for all the suggestions @erdOne! Adapted them in the latest commit.

[erdOne]

Thanks!
maintainer merge
May I ask what this is for?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[chrisflav]

Thanks! maintainer merge May I ask what this is for?

This is towards characterizing closed immersions with affine target as quotient maps.