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 ℬ)
:
The underlying function of Proj ℬ ⟶ Proj 𝒜 on the level of points.
Instances For
@[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 𝒜))
:
The underlying continuous function of Proj ℬ ⟶ Proj 𝒜 on the level of points.
Instances For
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)
:
The underlying function of Proj ℬ ⟶ Proj 𝒜 on the level of structure sheaves.
Instances For
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.
Instances For
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 𝒜))
:
The underlying map of Proj ℬ ⟶ Proj 𝒜 on the level of sheafed spaces.
Instances For
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 𝒜))
:
Functoriality of Proj.
Instances For
@[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)
:
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.
Instances For
@[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 𝒜)