Mathlib Changelog
v4
Changelog
About
Github
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