The chart lemmas, restated on Proj 𝒜

ChartExtension.lean and AwayChart.lean state extension and agreement in the chart's own coordinates: sections of modulesSpecToSheaf.obj (awayRestrict …) over opens of Spec A_{(g)}, scaled by the away ring's element isLocalizationElem. #585's glue consumes them on Proj 𝒜: sections of F over opens of Proj 𝒜, scaled by a structure-sheaf section. This file is that restatement, and it is the last step before the cover.

The transport is a substitution, not a transport

Scheme.Modules.restrictAppIso is Iso.refl, so Γ(awayRestrict 𝒜 F hg hd, U) is Γ(F, awayι 𝒜 g hg hd ''ᵁ U) — nothing has to move. What is left is that the glue wants the opens spelled D₊(g) and D₊(g) ⊓ D₊(f) rather than as chart images, and those are equal only propositionally (awayι_image_top, awayι_image_basicOpen).

Rather than transporting sections along eqToHom, each statement here takes the opens as variables together with an equation pinning them to the chart's images. subst then turns the statement into the chart's own, and the caller instantiates the variables at whatever spelling it wants. The restriction maps and the ≤ proofs come along for free: morphisms of Opens are proof-carrying data in a poset, so proof irrelevance identifies homOfLE hVW with the chart's own homOfLE (image_mono le_top).

That is why the hypotheses are oriented chart image = W and not W = chart image: subst eliminates the variable, and the variable has to be the one that disappears.

Scope

Extension and agreement, on Proj 𝒜, for a finite family. The cover itself, the twist that puts the family into one sheaf, and the gluing are not here.

theorem AlgebraicGeometry.Proj.exists_pow_smul_eq_res_image {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) {W V : (Proj 𝒜).Opens} (hW : (Scheme.Hom.opensFunctor (awayι 𝒜 g hg hd)).obj ⊤ = W) (hV : (Scheme.Hom.opensFunctor (awayι 𝒜 g hg hd)).obj (PrimeSpectrum.basicOpen (HomogeneousLocalization.Away.isLocalizationElem hg hf)) = V) (hVW : V ≤ W) (hVg : V ≤ ProjectiveSpectrum.basicOpen 𝒜 g) (s : ↑(F.presheaf.obj (Opposite.op V))) : ∃ (n : ℕ) (t : ↑(F.presheaf.obj (Opposite.op W))), (AddCommGrpCat.Hom.hom (F.presheaf.map (CategoryTheory.homOfLE hVW).op)) t = (have this := isLocalizationFrac 𝒜 hf hg n hVg; this) • s

Extension across the chart of a positive-degree element, on Proj 𝒜.

A section over D₊(g) ⊓ D₊(f) extends to D₊(g) after multiplying by (f / g)ⁿ.

theorem AlgebraicGeometry.Proj.exists_pow_smul_eq_res_image_uniform {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 : A} (hf : f ∈ 𝒜 e) {ι : Type u_1} [Finite ι] {g : ι → A} (hg : ∀ (i : ι), g i ∈ 𝒜 d) (hd : 0 < d) {W V : ι → (Proj 𝒜).Opens} (hW : (fun (i : ι) => (Scheme.Hom.opensFunctor (awayι 𝒜 (g i) ⋯ hd)).obj ⊤) = W) (hV : (fun (i : ι) => (Scheme.Hom.opensFunctor (awayι 𝒜 (g i) ⋯ hd)).obj (PrimeSpectrum.basicOpen (HomogeneousLocalization.Away.isLocalizationElem ⋯ hf))) = V) (hVW : ∀ (i : ι), V i ≤ W i) (hVg : ∀ (i : ι), V i ≤ ProjectiveSpectrum.basicOpen 𝒜 (g i)) (s : (i : ι) → ↑(F.presheaf.obj (Opposite.op (V i)))) : ∃ (n : ℕ), ∀ (i : ι), ∃ (t : ↑(F.presheaf.obj (Opposite.op (W i)))), (AddCommGrpCat.Hom.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)) t = (have this := isLocalizationFrac 𝒜 hf ⋯ n ⋯; this) • s i

One exponent for a finite family of charts, on Proj 𝒜.

theorem AlgebraicGeometry.Proj.exists_pow_smul_eq_of_res_eq_image_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 b : ι → A} (hf : ∀ (p : ι), f p ∈ 𝒜 e) (hb : ∀ (p : ι), b p ∈ 𝒜 d) (hd : 0 < d) {W V : ι → (Proj 𝒜).Opens} (hW : (fun (p : ι) => (Scheme.Hom.opensFunctor (awayι 𝒜 (b p) ⋯ hd)).obj ⊤) = W) (hV : (fun (p : ι) => (Scheme.Hom.opensFunctor (awayι 𝒜 (b p) ⋯ hd)).obj (PrimeSpectrum.basicOpen (HomogeneousLocalization.Away.isLocalizationElem ⋯ ⋯))) = V) (hVW : ∀ (p : ι), V p ≤ W p) (hWb : ∀ (p : ι), W p ≤ ProjectiveSpectrum.basicOpen 𝒜 (b p)) (t t' : (p : ι) → ↑(F.presheaf.obj (Opposite.op (W p)))) (h : ∀ (p : ι), (AddCommGrpCat.Hom.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (t p) = (AddCommGrpCat.Hom.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (t' p)) : ∃ (n : ℕ), ∀ (p : ι), (have this := isLocalizationFrac 𝒜 ⋯ ⋯ n ⋯; this) • t p = (have this := isLocalizationFrac 𝒜 ⋯ ⋯ n ⋯; this) • t' p

One exponent forcing a finite family of agreements, on Proj 𝒜.

The charts here are of arbitrary positive degree because #585 calls this on the pairwise overlaps of a degree-one cover, and those are the charts of products gᵢ gⱼ.