The two-chart model is Proj of a section ring

Let F / k be an algebraic function field and let z ∈ Fˣ. The degree-one sections 1 and z of the pole divisor (z)_∞ define two standard opens in Proj of its section ring ⨁ₙ L(n (z)_∞). This file identifies their homogeneous coordinate rings with the holomorphy rings used to construct the two-chart model:

• localization at X gives the finite chart, where z is regular;
• localization at z X gives the infinity chart, where z⁻¹ is regular.

Thus each standard open is canonically isomorphic to the corresponding affine chart of TauCeti.AlgebraicGeometry.twoChartModel. The ring identifications are TauCeti.Divisor.sectionRingAwayOneEquiv and TauCeti.Divisor.sectionRingAwayGeneratorEquiv; this file composes them with Mathlib's AlgebraicGeometry.Proj.basicOpenIsoSpec.

The two chart isomorphisms glue to an isomorphism of Proj of the section ring with the whole two-chart model. On the overlap Spec 𝒪_{z, z⁻¹} both charts give the point of Proj whose homogeneous coordinates send ∑ fₙ Xⁿ to ∑ fₙ, so they define a morphism out of the pushout of the two charts. Each chart maps isomorphically onto its standard open, the two standard opens cover Proj, and a point of the chart at infinity landing in D₊(X) lies where X / (z X) = z⁻¹ is invertible, that is, in the overlap; so the morphism is a bijective open immersion.

Main definitions

• TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso: the resulting isomorphism from the standard open D₊(X) to the finite chart.
• TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso: the resulting isomorphism from the standard open D₊(z X) to the infinity chart.
• TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso: the isomorphism of Proj of the section ring of (z)_∞ with the two-chart model built from z.

Main results

• TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso_hom and TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso_hom: the chart isomorphisms are the canonical maps D₊(f) ⟶ Spec A₍f₎ followed by the ring identifications.
• TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjChart_cover: the two standard opens cover Proj.
• TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_sectionRingProjIso_inv and TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_sectionRingProjIso_inv: on each chart, the isomorphism with Proj is the inverse of the chart isomorphism.
• TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso_hom_over: the isomorphism with Proj lies over Spec k.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section II.2.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.2 and Appendix B.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : ↑(AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z)) ≅ AlgebraicGeometry.Spec ↧↥(holomorphyRing {P : Place k F | ↑z ∈ P.integers})

The standard open D₊(X) of Proj of the section ring of (z)_∞ is the finite affine chart of the two-chart model.

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso_hom {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : (sectionRingProjFiniteChartIso hF z).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenIsoSpec (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z) ⋯ Nat.one_pos).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Divisor.sectionRingAwayOneEquiv hF z).symm.toRingEquiv.toRingHom))

The chart isomorphism TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso is Mathlib's isomorphism D₊(X) ≅ Spec A₍X₎ followed by the map induced by TauCeti.Divisor.sectionRingAwayOneEquiv.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : ↑(AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z)) ≅ AlgebraicGeometry.Spec ↧↥(holomorphyRing {P : Place k F | (↑z)⁻¹ ∈ P.integers})

The standard open D₊(z X) of Proj of the section ring of (z)_∞ is the affine chart at infinity of the two-chart model.

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso_hom {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : (sectionRingProjInfinityChartIso hF z).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenIsoSpec (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z) ⋯ Nat.one_pos).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Divisor.sectionRingAwayGeneratorEquiv hF z).symm.toRingEquiv.toRingHom))

The chart isomorphism TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso is Mathlib's isomorphism D₊(z X) ≅ Spec A₍z X₎ followed by the map induced by TauCeti.Divisor.sectionRingAwayGeneratorEquiv.

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjChart_cover {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z) ⊔ AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z) = ⊤

The standard opens D₊(X) and D₊(z X) cover Proj of the section ring of (z)_∞.

The global isomorphism

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso_inv_ι {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (sectionRingProjFiniteChartIso hF z).inv (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z)).ι = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Divisor.sectionRingAwayOneEquiv hF z).toRingEquiv.toRingHom)) (AlgebraicGeometry.Proj.awayι (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z) ⋯ Nat.one_pos)

The inverse of TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjFiniteChartIso, followed by the inclusion of D₊(X), is Mathlib's chart Spec A₍X₎ ⟶ Proj precomposed with the map induced by TauCeti.Divisor.sectionRingAwayOneEquiv.

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso_inv_ι {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (sectionRingProjInfinityChartIso hF z).inv (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z)).ι = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Divisor.sectionRingAwayGeneratorEquiv hF z).toRingEquiv.toRingHom)) (AlgebraicGeometry.Proj.awayι (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z) ⋯ Nat.one_pos)

The inverse of TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjInfinityChartIso, followed by the inclusion of D₊(z X), is Mathlib's chart Spec A₍z X₎ ⟶ Proj precomposed with the map induced by TauCeti.Divisor.sectionRingAwayGeneratorEquiv.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : AlgebraicGeometry.Proj (Divisor.poles hF z).sectionRingGrade ≅ twoChartModel hF ⋯

The two-chart model is Proj of the section ring of a pole divisor. For z ∈ Fˣ, the scheme glued from Spec 𝒪_z and Spec 𝒪_{z⁻¹} along Spec 𝒪_{z, z⁻¹} is isomorphic to Proj of the section ring ⨁ₙ L(n (z)_∞), compatibly with the chart isomorphisms D₊(X) ≅ Spec 𝒪_z and D₊(z X) ≅ Spec 𝒪_{z⁻¹} (TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_sectionRingProjIso_inv and TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_sectionRingProjIso_inv).

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_sectionRingProjIso_inv {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (ιFinite hF ⋯) (sectionRingProjIso hF z).inv = CategoryTheory.CategoryStruct.comp (sectionRingProjFiniteChartIso hF z).inv (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z)).ι

On the finite chart, the inverse of TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the inverse of the chart isomorphism D₊(X) ≅ Spec 𝒪_z.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_sectionRingProjIso_inv_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (Divisor.poles hF z).sectionRingGrade ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιFinite hF ⋯) (CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).inv h) = CategoryTheory.CategoryStruct.comp (sectionRingProjFiniteChartIso hF z).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z)).ι h)

On the finite chart, the inverse of TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the inverse of the chart isomorphism D₊(X) ≅ Spec 𝒪_z.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_sectionRingProjIso_inv {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (ιInfinity hF ⋯) (sectionRingProjIso hF z).inv = CategoryTheory.CategoryStruct.comp (sectionRingProjInfinityChartIso hF z).inv (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z)).ι

On the chart at infinity, the inverse of TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the inverse of the chart isomorphism D₊(z X) ≅ Spec 𝒪_{z⁻¹}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_sectionRingProjIso_inv_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj (Divisor.poles hF z).sectionRingGrade ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιInfinity hF ⋯) (CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).inv h) = CategoryTheory.CategoryStruct.comp (sectionRingProjInfinityChartIso hF z).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z)).ι h)

On the chart at infinity, the inverse of TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the inverse of the chart isomorphism D₊(z X) ≅ Spec 𝒪_{z⁻¹}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.basicOpen_polesSectionOne_ι_sectionRingProjIso_hom {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z)).ι (sectionRingProjIso hF z).hom = CategoryTheory.CategoryStruct.comp (sectionRingProjFiniteChartIso hF z).hom (ιFinite hF ⋯)

On D₊(X), TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the chart isomorphism D₊(X) ≅ Spec 𝒪_z followed by the finite chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.basicOpen_polesSectionOne_ι_sectionRingProjIso_hom_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {Z : AlgebraicGeometry.Scheme} (h : twoChartModel hF ⋯ ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionOne hF z)).ι (CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).hom h) = CategoryTheory.CategoryStruct.comp (sectionRingProjFiniteChartIso hF z).hom (CategoryTheory.CategoryStruct.comp (ιFinite hF ⋯) h)

On D₊(X), TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the chart isomorphism D₊(X) ≅ Spec 𝒪_z followed by the finite chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.basicOpen_polesSectionGenerator_ι_sectionRingProjIso_hom {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z)).ι (sectionRingProjIso hF z).hom = CategoryTheory.CategoryStruct.comp (sectionRingProjInfinityChartIso hF z).hom (ιInfinity hF ⋯)

On D₊(z X), TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the chart isomorphism D₊(z X) ≅ Spec 𝒪_{z⁻¹} followed by the chart at infinity.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.basicOpen_polesSectionGenerator_ι_sectionRingProjIso_hom_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {Z : AlgebraicGeometry.Scheme} (h : twoChartModel hF ⋯ ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (Divisor.poles hF z).sectionRingGrade (Divisor.polesSectionGenerator hF z)).ι (CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).hom h) = CategoryTheory.CategoryStruct.comp (sectionRingProjInfinityChartIso hF z).hom (CategoryTheory.CategoryStruct.comp (ιInfinity hF ⋯) h)

On D₊(z X), TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso is the chart isomorphism D₊(z X) ≅ Spec 𝒪_{z⁻¹} followed by the chart at infinity.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso_hom_over {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).hom (twoChartModel hF ⋯ ↘ AlgebraicGeometry.Spec ↧k) = AlgebraicGeometry.Proj.toSpecCoeff (Divisor.poles hF z).sectionRingGrade

The isomorphism with Proj lies over k: under TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso, the structure morphism of the two-chart model to Spec k is the coefficient morphism of Proj of the section ring.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso_hom_over_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (sectionRingProjIso hF z).hom (CategoryTheory.CategoryStruct.comp (twoChartModel hF ⋯ ↘ AlgebraicGeometry.Spec ↧k) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecCoeff (Divisor.poles hF z).sectionRingGrade) h

The isomorphism with Proj lies over k: under TauCeti.AlgebraicGeometry.twoChartModel.sectionRingProjIso, the structure morphism of the two-chart model to Spec k is the coefficient morphism of Proj of the section ring.