Commit 2024-11-20 19:44 9f24be2a

View on Github →

feat(AlgebraicGeometry): Proj is separated (#19290) This contribution was created as part of the Durham Computational Algebraic Geometry Workshop

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

added theorem AlgebraicGeometry.Proj.SpecMap_awayMap_awayι

added theorem AlgebraicGeometry.Proj.awayMap_awayToSection

added theorem AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap

added def AlgebraicGeometry.Proj.pullbackAwayιIso

added theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left

added theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right

added theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι

added theorem AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst

added theorem AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd

Created Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

added theorem AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

added theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

added theorem HomogeneousLocalization.algebraMap_eq

added def HomogeneousLocalization.awayMap

added theorem HomogeneousLocalization.awayMapAux_mk

added theorem HomogeneousLocalization.awayMap_fromZeroRingHom

added def HomogeneousLocalization.awayMapₐ

added theorem HomogeneousLocalization.awayMapₐ_apply

added theorem HomogeneousLocalization.range_awayMapAux_subset

added theorem HomogeneousLocalization.val_awayMap

added theorem HomogeneousLocalization.val_awayMap_eq_aux

added theorem HomogeneousLocalization.val_awayMap_mk

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

added theorem Localization.awayLift_mk