Commit 2024-07-14 17:46 62bfebd4

View on Github →

feat(AlgebraicGeometry): add locally Noetherian and Noetherian schemes (#13972)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.iSup_affineOpens_eq_top

Created Mathlib/AlgebraicGeometry/Noetherian.lean

added theorem AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian

added theorem AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover

added theorem AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top

added theorem AlgebraicGeometry.isLocallyNoetherian_iff_openCover

added theorem AlgebraicGeometry.isLocallyNoetherian_of_affine_cover

added theorem AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion

added theorem AlgebraicGeometry.isNoetherianRing_of_away

added theorem AlgebraicGeometry.isNoetherian_Spec

added theorem AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover

added theorem AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top

added theorem AlgebraicGeometry.noetherianSpace_of_isAffine

added theorem AlgebraicGeometry.noetherianSpace_of_isAffineOpen

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added def AlgebraicGeometry.IsOpenImmersion.ΓIsoTop

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.ideal_eq_iInf_comap_map_away