Agreement on the chart of a homogeneous element of any positive degree

ChartExtension.lean supplies the chart, its restriction awayRestrict, and the extension half of Modules/Affine/Extension.lean read on it. This file supplies the separatedness half.

Why it is a separate file rather than a separate degree

It used to be both. ChartExtension.lean was degree-one only and this file repeated the same three statements one degree up, because #585's cover is made of degree-one charts while its pairwise overlaps are not: D₊(gᵢ) ⊓ D₊(gⱼ) = D₊(gᵢ gⱼ) has degree two. The stated reason for the split -- "#585 extends only across degree-one charts" -- was true of #585 and false as a design principle, and the two trios were the same theorem with one lemma swapped. #822 collapsed that: ChartExtension.lean is now general in the degree, and what remains here is only the half it does not state.

Scope

One chart, one basic open of it. No cover, no gluing.

theorem AlgebraicGeometry.Proj.exists_pow_smul_eq_of_res_eq_away {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (F : (Proj 𝒜).Modules) [(have this := F; this).IsQuasicoherent] {d e : ℕ} {f g : A} (hf : f ∈ 𝒜 e) (hg : g ∈ 𝒜 d) (hd : 0 < d) (t t' : ↑((modulesSpecToSheaf.obj (awayRestrict 𝒜 F hg hd)).presheaf.obj (Opposite.op ⊤))) (h : (CategoryTheory.ConcreteCategory.hom ((modulesSpecToSheaf.obj (awayRestrict 𝒜 F hg hd)).presheaf.map (CategoryTheory.homOfLE ⋯).op)) t = (CategoryTheory.ConcreteCategory.hom ((modulesSpecToSheaf.obj (awayRestrict 𝒜 F hg hd)).presheaf.map (CategoryTheory.homOfLE ⋯).op)) t') : ∃ (n : ℕ), HomogeneousLocalization.Away.isLocalizationElem hg hf ^ n • t = HomogeneousLocalization.Away.isLocalizationElem hg hf ^ n • t'

Two sections of a chart agreeing on a basic open agree after clearing a power.

exists_pow_smul_eq_of_res_eq_chart one degree up, and the reason it is needed: #585's pairwise overlap D₊(gᵢ) ⊓ D₊(gⱼ) is the chart of gᵢ gⱼ, which has degree two.

theorem AlgebraicGeometry.Proj.exists_pow_smul_eq_of_res_eq_away_of_le {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (F : (Proj 𝒜).Modules) {d e : ℕ} {f g : A} (hf : f ∈ 𝒜 e) (hg : g ∈ 𝒜 d) (hd : 0 < d) (t t' : ↑((modulesSpecToSheaf.obj (awayRestrict 𝒜 F hg hd)).presheaf.obj (Opposite.op ⊤))) {n m : ℕ} (hnm : n ≤ m) (h : HomogeneousLocalization.Away.isLocalizationElem hg hf ^ n • t = HomogeneousLocalization.Away.isLocalizationElem hg hf ^ n • t') : HomogeneousLocalization.Away.isLocalizationElem hg hf ^ m • t = HomogeneousLocalization.Away.isLocalizationElem hg hf ^ m • t'

That exponent can be raised, exactly as in the degree-one case and for the same reason: a single exponent across all pairs of a finite cover needs every pair raised to the maximum.

theorem AlgebraicGeometry.Proj.exists_pow_smul_eq_of_res_eq_away_uniform {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (F : (Proj 𝒜).Modules) [(have this := F; this).IsQuasicoherent] {ι : Type u_1} [Finite ι] {d e : ℕ} {f g : ι → A} (hf : ∀ (i : ι), f i ∈ 𝒜 e) (hg : ∀ (i : ι), g i ∈ 𝒜 d) (hd : 0 < d) (t t' : (i : ι) → ↑((modulesSpecToSheaf.obj (awayRestrict 𝒜 F ⋯ hd)).presheaf.obj (Opposite.op ⊤))) (h : ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom ((modulesSpecToSheaf.obj (awayRestrict 𝒜 F ⋯ hd)).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (t i) = (CategoryTheory.ConcreteCategory.hom ((modulesSpecToSheaf.obj (awayRestrict 𝒜 F ⋯ hd)).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (t' i)) : ∃ (n : ℕ), ∀ (i : ι), HomogeneousLocalization.Away.isLocalizationElem ⋯ ⋯ ^ n • t i = HomogeneousLocalization.Away.isLocalizationElem ⋯ ⋯ ^ n • t' i

One exponent for a finite family of agreements, the shape #585's glue calls: agreement has to be forced on every pairwise overlap at once, so the family is indexed by pairs.