Commit 2024-07-25 23:15 de49f39e

View on Github →

feat(AlgebraicGeometry): Define affine morphisms (#13996)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.iSup_basicOpen_of_span_eq_top

Created Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

added def AlgebraicGeometry.affinePreimage

added theorem AlgebraicGeometry.isAffineHom_stableUnderBaseChange

added theorem AlgebraicGeometry.isAffineOpen.preimage

added theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen

added theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen_aux

added theorem AlgebraicGeometry.isAffine_of_isAffineHom

added theorem AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.iSup_basicOpen_eq_top_iff'

added theorem PrimeSpectrum.iSup_basicOpen_eq_top_iff

Modified Mathlib/RingTheory/Localization/Basic.lean