Commit 2024-11-17 17:51 b10de21d

View on Github →

feat(AlgebraicGeometry): basic API for Proj (#19152)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.opensRange_comp

added theorem AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso

added theorem AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso

Created Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

added def AlgebraicGeometry.Proj.affineOpenCover

added def AlgebraicGeometry.Proj.awayToSection

added def AlgebraicGeometry.Proj.awayι

added theorem AlgebraicGeometry.Proj.awayι_toSpecZero

added def AlgebraicGeometry.Proj.basicOpen

added def AlgebraicGeometry.Proj.basicOpenIsoAway

added def AlgebraicGeometry.Proj.basicOpenIsoSpec

added def AlgebraicGeometry.Proj.basicOpenToSpec

added theorem AlgebraicGeometry.Proj.basicOpenToSpec_app_top

added theorem AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj

added theorem AlgebraicGeometry.Proj.basicOpen_mono

added theorem AlgebraicGeometry.Proj.basicOpen_mul

added theorem AlgebraicGeometry.Proj.basicOpen_one

added theorem AlgebraicGeometry.Proj.basicOpen_pow

added theorem AlgebraicGeometry.Proj.basicOpen_zero

added theorem AlgebraicGeometry.Proj.iSup_basicOpen_eq_top

added theorem AlgebraicGeometry.Proj.isAffineOpen_basicOpen

added theorem AlgebraicGeometry.Proj.isBasis_basicOpen

added theorem AlgebraicGeometry.Proj.mem_basicOpen

added def AlgebraicGeometry.Proj.openCoverOfISupEqTop

added theorem AlgebraicGeometry.Proj.opensRange_awayι

added def AlgebraicGeometry.Proj.stalkIso

added def AlgebraicGeometry.Proj.toSpecZero

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

added def HomogeneousLocalization.fromZeroRingHom