Functoriality of Proj

def AlgebraicGeometry.ProjectiveSpectrum.comapFun {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (p : ProjectiveSpectrum ℬ) : ProjectiveSpectrum 𝒜

The underlying function of Proj ℬ ⟶ Proj 𝒜 on the level of points.

Equations

• AlgebraicGeometry.ProjectiveSpectrum.comapFun f hf p = { asHomogeneousIdeal := HomogeneousIdeal.comap f p.asHomogeneousIdeal, isPrime := ⋯, not_irrelevant_le := ⋯ }

@[simp]

theorem AlgebraicGeometry.ProjectiveSpectrum.comapFun_asHomogeneousIdeal {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (p : ProjectiveSpectrum ℬ) : (comapFun f hf p).asHomogeneousIdeal = HomogeneousIdeal.comap f p.asHomogeneousIdeal

def AlgebraicGeometry.ProjectiveSpectrum.comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)

The underlying continuous function of Proj ℬ ⟶ Proj 𝒜 on the level of points.

Equations

• AlgebraicGeometry.ProjectiveSpectrum.comap f hf = { toFun := AlgebraicGeometry.ProjectiveSpectrum.comapFun f hf, continuous_toFun := ⋯ }

noncomputable def AlgebraicGeometry.Proj.comapStructureSheafFun {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ)) (hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier) (s : (x : ↥U) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule) (y : ↥V) : HomogeneousLocalization.AtPrime ℬ (↑y).asHomogeneousIdeal.toSubmodule

The underlying function of Proj ℬ ⟶ Proj 𝒜 on the level of structure sheaves.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.isLocallyFraction_comapStructureSheafFun {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ)) (hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier) (s : (x : ↥U) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule) (hs : (ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred s) : (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ).pred (comapStructureSheafFun f hf U V hUV s)

noncomputable def AlgebraicGeometry.Proj.comapStructureSheaf {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ)) (hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier) : ↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U)) →+* ↑((ProjectiveSpectrum.Proj.structureSheaf ℬ).obj.obj (Opposite.op V))

The underlying ring hom of Proj ℬ ⟶ Proj 𝒜 on the level of structure sheaves.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.sheafedSpaceMap {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) : toSheafedSpace ℬ ⟶ toSheafedSpace 𝒜

The underlying map of Proj ℬ ⟶ Proj 𝒜 on the level of sheafed spaces.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (p : ProjectiveSpectrum ℬ) : ↑((TopCat.Hom.hom (sheafedSpaceMap f hf).hom.base) p).asHomogeneousIdeal = ⇑f ⁻¹' ↑p.asHomogeneousIdeal

theorem AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (U : (TopologicalSpace.Opens ↑↑(toSheafedSpace 𝒜).toPresheafedSpace)ᵒᵖ) (s : ↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op (Opposite.unop U)))) (y : ↥(Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (TopCat.ofHom (ProjectiveSpectrum.comap f hf))).obj (Opposite.unop U))))) : ↑((CommRingCat.Hom.hom ((sheafedSpaceMap f hf).hom.c.app U)) s) y = comapStructureSheafFun f hf (Opposite.unop U) ((TopologicalSpace.Opens.map (TopCat.ofHom (ProjectiveSpectrum.comap f hf))).obj (Opposite.unop U)) ⋯ (↑s) y

theorem AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {p : ProjectiveSpectrum ℬ} (c : HomogeneousLocalization.NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl) : (CategoryTheory.ConcreteCategory.hom ((toSheafedSpace ℬ).presheaf.germ ((TopologicalSpace.Opens.map (sheafedSpaceMap f hf).hom.base).obj (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)))) p ⋯)) ((CategoryTheory.ConcreteCategory.hom ((sheafedSpaceMap f hf).hom.c.app (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)))) (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c)) = (CategoryTheory.ConcreteCategory.hom ((toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯)) (sectionInBasicOpen ℬ p (HomogeneousLocalization.NumDenSameDeg.map f ⋯ c))

@[simp]

theorem AlgebraicGeometry.Proj.val_sectionInBasicOpen_apply {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (p : ↑(ProjectiveSpectrum.top 𝒜)) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 p.asHomogeneousIdeal.toIdeal.primeCompl) (q : ↥(ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)) : HomogeneousLocalization.val (↑(sectionInBasicOpen 𝒜 p c) q) = Localization.mk ↑c.num ⟨↑c.den, ⋯⟩

theorem AlgebraicGeometry.Proj.localRingHom_comp_stalkIso {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (p : ProjectiveSpectrum ℬ) : CategoryTheory.CategoryStruct.comp (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯)) (stalkIso ℬ p).inv) = PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p

theorem AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (p : ProjectiveSpectrum ℬ) (x : ↑((Proj 𝒜).presheaf.stalk ((ProjectiveSpectrum.comap f hf) p))) : (CategoryTheory.ConcreteCategory.hom (stalkIso ℬ p).inv) ((HomogeneousLocalization.localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯) ((CategoryTheory.ConcreteCategory.hom (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom) x)) = (CategoryTheory.ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p)) x

noncomputable def AlgebraicGeometry.Proj.map {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) : Proj ℬ ⟶ Proj 𝒜

Functoriality of Proj.

Equations

• AlgebraicGeometry.Proj.map f hf = { toHom := (AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom, prop := ⋯ }

@[simp]

theorem AlgebraicGeometry.Proj.map_preimage_basicOpen {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (s : A) : (TopologicalSpace.Opens.map (map f hf).base).obj (basicOpen 𝒜 s) = basicOpen ℬ (f s)

theorem AlgebraicGeometry.Proj.ι_comp_map {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (s : A) : CategoryTheory.CategoryStruct.comp (basicOpen ℬ (f s)).ι (map f hf) = CategoryTheory.CategoryStruct.comp (Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) ((TopologicalSpace.Opens.map (map f hf).base).obj (basicOpen 𝒜 s)) ⋯) (basicOpen 𝒜 s).ι

theorem AlgebraicGeometry.Proj.awayToSection_comp_appLE {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} {s : A} (hs : s ∈ 𝒜 i) : CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 s) (Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ (f s)) ⋯) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s)) (awayToSection ℬ (f s))

theorem AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} {s : A} (hs : s ∈ 𝒜 i) {Z : CommRingCat} (h : (Proj ℬ).presheaf.obj (Opposite.op (basicOpen ℬ (f s))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 s) (CategoryTheory.CategoryStruct.comp (Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ (f s)) ⋯) h) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s)) (CategoryTheory.CategoryStruct.comp (awayToSection ℬ (f s)) h)

theorem AlgebraicGeometry.Proj.awayι_comp_map {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} (hi : 0 < i) (s : A) (hs : s ∈ 𝒜 i) : CategoryTheory.CategoryStruct.comp (awayι ℬ (f s) ⋯ hi) (map f hf) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s))) (awayι 𝒜 s hs hi)

The following square commutes:

Proj ℬ         ⟶ Proj 𝒜₁
    ^                   ^
    |                   |
Spec A₂[f(s)⁻¹]₀ ⟶ Spec A₁[s⁻¹]₀

theorem AlgebraicGeometry.Proj.awayι_comp_map_assoc {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} (hi : 0 < i) (s : A) (hs : s ∈ 𝒜 i) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (awayι ℬ (f s) ⋯ hi) (CategoryTheory.CategoryStruct.comp (map f hf) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s))) (CategoryTheory.CategoryStruct.comp (awayι 𝒜 s hs hi) h)

The following square commutes:

Proj ℬ         ⟶ Proj 𝒜₁
    ^                   ^
    |                   |
Spec A₂[f(s)⁻¹]₀ ⟶ Spec A₁[s⁻¹]₀

noncomputable def AlgebraicGeometry.Proj.mapAffineOpenCover {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) : (Proj ℬ).AffineOpenCover

Given a graded ring hom f : 𝒜 →+*ᵍ ℬ satisfying the hypothesis ℬ₊ ≤ 𝒜₊.map f, we obtain an affine open cover of Proj ℬ consisting of D(f(s)) for s ∈ A positive degree.

Equations

• AlgebraicGeometry.Proj.mapAffineOpenCover f hf = AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan ℬ (fun (s : (AlgebraicGeometry.Proj.affineOpenCover 𝒜).I₀) => f ↑s.snd) ⋯ ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Proj.mapAffineOpenCover_f {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (i : (affineOpenCover 𝒜).I₀) : (mapAffineOpenCover f hf).f i = awayι ℬ (f ↑i.snd) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Proj.mapAffineOpenCover_I₀ {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) : (mapAffineOpenCover f hf).I₀ = (affineOpenCover 𝒜).I₀

theorem AlgebraicGeometry.Proj.map_comp {A B C σ τ ψ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] [CommRing C] [SetLike ψ C] [AddSubgroupClass ψ C] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} {𝒞 : ℕ → ψ} [GradedRing 𝒜] [GradedRing ℬ] [GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (hg : HomogeneousIdeal.irrelevant 𝒞 ≤ HomogeneousIdeal.map g (HomogeneousIdeal.irrelevant ℬ)) : map (g.comp f) ⋯ = CategoryTheory.CategoryStruct.comp (map g hg) (map f hf)

theorem AlgebraicGeometry.Proj.map_id {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] : map (GradedRingHom.id 𝒜) ⋯ = CategoryTheory.CategoryStruct.id (Proj 𝒜)