Commit 2025-12-09 18:53 1ac5f9c6

View on Github →

feat(AlgebraicGeometry): "quasi-coherent 𝒪ₓ-algebras" (#32595)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Cover/Directed.lean

Modified Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean

added theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage

added theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isLocallyDirected

added theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion

added theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map

added def AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization

modified def AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen

added theorem AlgebraicGeometry.Scheme.preservesLocalization_toOpensFunctor