The projective line over a commutative ring

The projective line over a commutative ring R is ℙ¹_R = Proj R[X₀, X₁], written here, following the convention of TauCeti.SymmetricAlgebra.projToSpec, as the projective spectrum of the symmetric algebra of R², whose two standard basis vectors are the homogeneous coordinates X₀ and X₁.

It is covered by the two standard affine charts D₊(Xᵢ). The chart D₊(Xᵢ) is the spectrum of the degree-zero part R[X₀, X₁]_(Xᵢ) of the localization away from Xᵢ, and dehomogenization, setting Xᵢ = 1 and the other coordinate to X, identifies it with the polynomial ring R[X]: the fraction p / Xᵢⁿ of a form p of degree n goes to p with Xᵢ = 1. Each chart Spec R[X] ⟶ ℙ¹_R is a schematically dense open immersion over any ring. The projective line ℙ¹_R is proper over R, as the Proj of the symmetric algebra of a finite module (TauCeti.SymmetricAlgebra.instIsProperOver), and smooth of relative dimension one over R, since each chart is the affine line Spec R[X]; it is integral when R is a domain, and its local rings are regular when R is a regular ring. Its formation commutes with every change of base ring R → S: ℙ¹_S is the fibre product ℙ¹_R ×_{Spec R} Spec S. Over a domain, its function field is the fraction field R(X) of the ring R[X] of functions on the chart D₊(X₀), the function X₁ / X₀ on that chart going to X.

Main definitions

• TauCeti.AlgebraicGeometry.projectiveLine R: the projective line over R, a scheme over Spec R.
• TauCeti.AlgebraicGeometry.projectiveLine.coord R i: the homogeneous coordinate Xᵢ.
• TauCeti.AlgebraicGeometry.projectiveLine.dehomogenize R i: setting Xᵢ = 1 and the other coordinate to X, an R-algebra map R[X₀, X₁] → R[X].
• TauCeti.AlgebraicGeometry.projectiveLine.awayEquivPolynomial R i: the ring of the chart D₊(Xᵢ) is R[X].
• TauCeti.AlgebraicGeometry.projectiveLine.awayι R i: the open immersion of that chart.
• TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι R i: that chart with source literally Spec R[X].
• TauCeti.AlgebraicGeometry.projectiveLine.infinitySection R: the section [0 : 1]; over a field K, TauCeti.AlgebraicGeometry.projectiveLine.infinity K is its single image point.
• TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv R i: the functions on the chart D₊(Xᵢ) are the polynomials R[X].
• TauCeti.AlgebraicGeometry.projectiveLine.baseChangeProjection R S: for an R-algebra S, the projection ℙ¹_S ⟶ ℙ¹_R.
• TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv R: over a domain R, the function field of ℙ¹_R is R(X), as an R-algebra.

Main results

• TauCeti.AlgebraicGeometry.projectiveLine.exists_eq_coord_pow_mul_add_coord_pow_mul: a form of degree k + l with k ≤ l + 1 is X₀ᵏ a + X₁ᵏ b for forms a and b of degree l.
• TauCeti.AlgebraicGeometry.projectiveLine.exists_eq_coord_pow_mul_add_coord_pow_mul_add: for k = l + m + 2, a form of degree k + l is X₀ᵏ a + X₁ᵏ b + (X₀X₁)ˡ⁺¹ c with c of degree m.
• TauCeti.AlgebraicGeometry.projectiveLine.coord_mem_nonZeroDivisors: homogeneous coordinates are nonzerodivisors over any ring, so every polynomialChartι is schematically dense.
• TauCeti.AlgebraicGeometry.projectiveLine.opensRange_polynomialChartι and TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι_preimage_basicOpen_rev: the chart ranges are the standard basic opens and their overlap is the locus where X is invertible.
• TauCeti.AlgebraicGeometry.projectiveLine.range_polynomialChartι_union_range_polynomialChartι: the two ranges cover.
• TauCeti.AlgebraicGeometry.projectiveLine.range_infinitySection: the infinity section is the complement of the zeroth chart over any ring; it is a closed immersion and misses that chart by TauCeti.AlgebraicGeometry.projectiveLine.infinitySection_notMem_range_polynomialChartι.
• TauCeti.AlgebraicGeometry.projectiveLine.compl_range_polynomialChartι: over a field the complement is the singleton infinity.
• TauCeti.AlgebraicGeometry.projectiveLine.awayEquivPolynomial_mk: the chart isomorphism sends p / Xᵢⁿ to the dehomogenization of p.
• TauCeti.AlgebraicGeometry.projectiveLine.iSup_basicOpen_coord_eq_top, TauCeti.AlgebraicGeometry.projectiveLine.exists_eq_awayι and TauCeti.AlgebraicGeometry.projectiveLine.basicOpen_coord_sup_eq_top: the two charts cover ℙ¹_R, and by TauCeti.AlgebraicGeometry.projectiveLine.isAffineOpen_basicOpen_coord each chart is affine.
• TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv_awayToSection: on the chart D₊(Xᵢ), chartSectionsEquiv agrees with the chart isomorphism on the fractions Proj.awayToSection a, and TauCeti.AlgebraicGeometry.projectiveLine.awayToSection_algebraMap: the constants restrict to the fractions c / 1, and TauCeti.AlgebraicGeometry.projectiveLine.val_map_baseRingToGlobalSections: on every open, the constant global function r takes the value r in every localization.
• TauCeti.AlgebraicGeometry.projectiveLine.isIntegral: ℙ¹_R is integral over a domain.
• TauCeti.AlgebraicGeometry.projectiveLine.isRegularLocalRing_stalk: its local rings are regular over a regular ring.
• TauCeti.AlgebraicGeometry.projectiveLine.smoothOfRelativeDimension: ℙ¹_R is smooth of relative dimension one over Spec R.
• TauCeti.AlgebraicGeometry.projectiveLine.isPullback_baseChangeProjection: ℙ¹_S is the base change of ℙ¹_R along Spec S ⟶ Spec R.
• TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv_germToFunctionField: on the chart D₊(X₀), the identification of the function field with R(X) is chartSectionsEquiv.
• TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv_symm_X: that identification sends the function X₁ / X₀ to X.
• TauCeti.AlgebraicGeometry.projectiveLine.natDegree_dehomogenize_le and TauCeti.AlgebraicGeometry.projectiveLine.dehomogenize_eq_zero_iff: dehomogenizing a form of degree j gives a polynomial of degree at most j, and is injective on such forms.
• TauCeti.AlgebraicGeometry.projectiveLine.eq_zero_of_coord_pow_mul_eq: a form c of degree m with X₀ᵏ X₁ᵏ' c = (X₀X₁)ᵐ⁺¹ (X₁ᵏ' a - X₀ᵏ b), for b of degree k' - m - 2, vanishes.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section II.2.
• The Stacks Project, Section 27.8 (the projective spectrum of a graded ring).

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.projectiveLine (R : Type u) [CommRing R] : AlgebraicGeometry.Scheme

The projective line ℙ¹_R = Proj R[X₀, X₁] over a commutative ring R: the projective spectrum of the symmetric algebra of R², whose standard basis vectors are the homogeneous coordinates. It is a scheme over Spec R through TauCeti.SymmetricAlgebra.projToSpec, proper by TauCeti.SymmetricAlgebra.instIsProperOver.

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.coord (R : Type u) [CommRing R] (i : Fin 2) : SymmetricAlgebra R (Fin 2 → R)

The homogeneous coordinate Xᵢ of the projective line: the i-th standard basis vector of R², in degree one of the symmetric algebra.

theorem TauCeti.AlgebraicGeometry.projectiveLine.coord_mem (R : Type u) [CommRing R] (i : Fin 2) : coord R i ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) 1

The homogeneous coordinates have degree one.

theorem TauCeti.AlgebraicGeometry.projectiveLine.coord_pow_mul_coord_pow_mem (R : Type u) [CommRing R] {a b d : ℕ} (h : a + b = d) : coord R 0 ^ a * coord R 1 ^ b ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) d

The monomial X₀ᵃ X₁ᵇ is a form of degree a + b.

theorem TauCeti.AlgebraicGeometry.projectiveLine.coord_mul_coord_pow_mem (R : Type u) [CommRing R] (k : ℕ) : (coord R 0 * coord R 1) ^ k ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) (k * 2)

The power (X₀X₁)ᵏ is a form of degree 2k.

theorem TauCeti.AlgebraicGeometry.projectiveLine.coord_mem_nonZeroDivisors (R : Type u) [CommRing R] (i : Fin 2) : coord R i ∈ nonZeroDivisors (SymmetricAlgebra R (Fin 2 → R))

Each homogeneous coordinate is a nonzerodivisor, even over a nonreduced base ring.

theorem TauCeti.AlgebraicGeometry.projectiveLine.ι_eq_smul_coord_add_smul_coord (R : Type u) [CommRing R] (i : Fin 2) (m : Fin 2 → R) : (SymmetricAlgebra.ι R (Fin 2 → R)) m = m i • coord R i + m i.rev • coord R i.rev

A linear form is the combination of the two homogeneous coordinates with its coefficients.

theorem TauCeti.AlgebraicGeometry.projectiveLine.range_ι_eq_span_coord_sup_span_coord (R : Type u) [CommRing R] : (SymmetricAlgebra.ι R (Fin 2 → R)).range = R ∙ coord R 0 ⊔ R ∙ coord R 1

The linear forms are the R-combinations of the two homogeneous coordinates.

theorem TauCeti.AlgebraicGeometry.projectiveLine.exists_eq_coord_pow_mul_add_coord_pow_mul (R : Type u) [CommRing R] {k l : ℕ} (hkl : k ≤ l + 1) {r : SymmetricAlgebra R (Fin 2 → R)} (hr : r ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) (k + l)) : ∃ a ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) l, ∃ b ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) l, r = coord R 0 ^ k * a + coord R 1 ^ k * b

Forms of degree at least 2k - 1 lie in the ideal (X₀ᵏ, X₁ᵏ). A form of degree k + l with k ≤ l + 1 is X₀ᵏ a + X₁ᵏ b for forms a and b of degree l: each of its monomials X₀ᵖ X₁^q, with p + q = k + l ≥ 2k - 1, has p ≥ k or q ≥ k.

theorem TauCeti.AlgebraicGeometry.projectiveLine.exists_eq_coord_pow_mul_add_coord_pow_mul_add (R : Type u) [CommRing R] {m k l : ℕ} (hk : k = l + m + 2) {r : SymmetricAlgebra R (Fin 2 → R)} (hr : r ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) (k + l)) : ∃ a ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) l, ∃ b ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) l, ∃ c ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) m, r = coord R 0 ^ k * a + coord R 1 ^ k * b + (coord R 0 * coord R 1) ^ (l + 1) * c

For k = l + m + 2, a form of degree k + l is X₀ᵏ a + X₁ᵏ b + (X₀X₁)ˡ⁺¹ c with a and b of degree l and c of degree m: a monomial X₀ᵅ X₁ᵝ of degree k + l with α, β < k has α, β ≥ l + 1.

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.dehomogenize (R : Type u) [CommRing R] (i : Fin 2) : SymmetricAlgebra R (Fin 2 → R) →ₐ[R] Polynomial R

Dehomogenization at Xᵢ: the R-algebra map R[X₀, X₁] → R[X] setting Xᵢ = 1 and the other homogeneous coordinate to X.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.dehomogenize_coord_self (R : Type u) [CommRing R] (i : Fin 2) : (dehomogenize R i) (coord R i) = 1

Dehomogenization at Xᵢ sends Xᵢ to 1.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.dehomogenize_coord_rev (R : Type u) [CommRing R] (i : Fin 2) : (dehomogenize R i) (coord R i.rev) = Polynomial.X

Dehomogenization at Xᵢ sends the other homogeneous coordinate to X.

theorem TauCeti.AlgebraicGeometry.projectiveLine.natDegree_dehomogenize_le (R : Type u) [CommRing R] (i : Fin 2) {j : ℕ} {p : SymmetricAlgebra R (Fin 2 → R)} (hp : p ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) j) : ((dehomogenize R i) p).natDegree ≤ j

Dehomogenizing a form of degree j gives a polynomial of degree at most j.

The standard affine charts

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.awayEquivPolynomial (R : Type u) [CommRing R] (i : Fin 2) : HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i) ≃ₐ[R] Polynomial R

The chart ring of D₊(Xᵢ) is a polynomial ring: dehomogenization identifies the degree-zero part R[X₀, X₁]_(Xᵢ) of the localization away from Xᵢ with R[X].

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.awayEquivPolynomial_mk (R : Type u) [CommRing R] (i : Fin 2) {n : ℕ} {a : SymmetricAlgebra R (Fin 2 → R)} (ha : a ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) (n • 1)) : (awayEquivPolynomial R i) (HomogeneousLocalization.Away.mk (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) ⋯ n a ha) = (dehomogenize R i) a

The chart isomorphism sends p / Xᵢⁿ to the dehomogenization of p.

theorem TauCeti.AlgebraicGeometry.projectiveLine.dehomogenize_eq_zero_iff (R : Type u) [CommRing R] (i : Fin 2) {j : ℕ} {p : SymmetricAlgebra R (Fin 2 → R)} (hp : p ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) j) : (dehomogenize R i) p = 0 ↔ p = 0

Dehomogenization is injective on forms of a fixed degree: a form of degree j vanishes once it does after setting Xᵢ = 1.

theorem TauCeti.AlgebraicGeometry.projectiveLine.eq_zero_of_coord_pow_mul_eq (R : Type u) [CommRing R] {m k k' j' : ℕ} (hk' : j' + m + 2 = k') {a b c : SymmetricAlgebra R (Fin 2 → R)} (hb : b ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) j') (hc : c ∈ SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R) m) (h : coord R 0 ^ k * coord R 1 ^ k' * c = (coord R 0 * coord R 1) ^ (m + 1) * (coord R 1 ^ k' * a - coord R 0 ^ k * b)) : c = 0

If X₀ᵏ X₁ᵏ' c = (X₀X₁)ᵐ⁺¹ (X₁ᵏ' a - X₀ᵏ b) for a form c of degree m and a form b of degree k' - m - 2, then c = 0: after setting X₀ = 1, the coefficients of X^{k' + i}, i ≤ m, of the right-hand side vanish.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.awayEquivPolynomial_symm_X (R : Type u) [CommRing R] (i : Fin 2) : (awayEquivPolynomial R i).symm Polynomial.X = HomogeneousLocalization.Away.mk (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) ⋯ 1 (coord R i.rev) ⋯

The inverse of the chart isomorphism sends X to the other coordinate over Xᵢ.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.projectiveLine.awayι (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.Spec ↧(HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)) ⟶ projectiveLine R

The open immersion of the standard affine chart D₊(Xᵢ) = Spec R[X₀, X₁]_(Xᵢ) into the projective line.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.awayι_over (R : Type u) [CommRing R] (i : Fin 2) : CategoryTheory.CategoryStruct.comp (awayι R i) (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))))

On the chart D₊(Xᵢ), the structure morphism of the projective line is Spec of the inclusion of the constants.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.awayι_over_assoc (R : Type u) [CommRing R] (i : Fin 2) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (awayι R i) (CategoryTheory.CategoryStruct.comp (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))))) h

On the chart D₊(Xᵢ), the structure morphism of the projective line is Spec of the inclusion of the constants.

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.Spec ↧(Polynomial R) ⟶ projectiveLine R

The standard affine chart of the projective line, with source literally Spec R[X].

theorem TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι_def (R : Type u) [CommRing R] (i : Fin 2) : polynomialChartι R i = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (awayEquivPolynomial R i).toRingEquiv.toCommRingCatIso.hom) (awayι R i)

The polynomial chart is the chart-ring equivalence followed by the standard open immersion.

instance TauCeti.AlgebraicGeometry.projectiveLine.instIsOpenImmersionPolynomialChartι (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.IsOpenImmersion (polynomialChartι R i)

instance TauCeti.AlgebraicGeometry.projectiveLine.instIsSchemeTheoreticallyDominantPolynomialChartι (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.IsSchemeTheoreticallyDominant (polynomialChartι R i)

Every standard polynomial chart of the projective line is schematically dense.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι_over (R : Type u) [CommRing R] (i : Fin 2) : CategoryTheory.CategoryStruct.comp (polynomialChartι R i) (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Polynomial R)))

Each polynomial chart is a morphism over Spec R.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι_over_assoc (R : Type u) [CommRing R] (i : Fin 2) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (polynomialChartι R i) (CategoryTheory.CategoryStruct.comp (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Polynomial R)))) h

Each polynomial chart is a morphism over Spec R.

theorem TauCeti.AlgebraicGeometry.projectiveLine.opensRange_polynomialChartι (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.Scheme.Hom.opensRange (polynomialChartι R i) = AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)

The image of the polynomial chart is the standard projective basic open.

theorem TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι_preimage_basicOpen_rev (R : Type u) [CommRing R] (i : Fin 2) : (TopologicalSpace.Opens.map (polynomialChartι R i).base).obj (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i.rev)) = PrimeSpectrum.basicOpen Polynomial.X

The two polynomial charts meet where their polynomial coordinate is invertible.

theorem TauCeti.AlgebraicGeometry.projectiveLine.polynomialChartι_mem_range_iff (R : Type u) [CommRing R] (i : Fin 2) (q : ↥(AlgebraicGeometry.Spec ↧(Polynomial R))) : (polynomialChartι R i) q ∈ Set.range ⇑(polynomialChartι R i.rev) ↔ Polynomial.X ∉ q.asIdeal

A point of one polynomial chart lies in the other chart exactly off its zero locus.

theorem TauCeti.AlgebraicGeometry.projectiveLine.iSup_basicOpen_coord_eq_top (R : Type u) [CommRing R] : ⨆ (i : Fin 2), AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i) = ⊤

The standard charts D₊(Xᵢ) cover the projective line.

theorem TauCeti.AlgebraicGeometry.projectiveLine.exists_eq_awayι (R : Type u) [CommRing R] (p : ↥(projectiveLine R)) : ∃ (i : Fin 2) (q : ↥(AlgebraicGeometry.Spec ↧(HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)))), (awayι R i) q = p

The two standard charts cover the projective line.

theorem TauCeti.AlgebraicGeometry.projectiveLine.basicOpen_coord_sup_eq_top (R : Type u) [CommRing R] : AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R 0) ⊔ AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R 1) = ⊤

The standard charts D₊(X₀) and D₊(X₁) cover the projective line.

theorem TauCeti.AlgebraicGeometry.projectiveLine.inf_le_basicOpen_coord_mul_coord_pow (R : Type u) [CommRing R] {k : ℕ} : AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R 0) ⊓ AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R 1) ≤ AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) ((coord R 0 * coord R 1) ^ k)

The overlap D₊(X₀) ⊓ D₊(X₁) of the standard charts lies in D₊((X₀X₁)ᵏ).

theorem TauCeti.AlgebraicGeometry.projectiveLine.range_polynomialChartι_union_range_polynomialChartι (R : Type u) [CommRing R] : Set.range ⇑(polynomialChartι R 0) ∪ Set.range ⇑(polynomialChartι R 1) = Set.univ

The two polynomial chart ranges cover the projective line.

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.infinitySection (R : Type u) [CommRing R] : AlgebraicGeometry.Spec ↧R ⟶ projectiveLine R

The infinity section of the projective line, given by the zero point of the chart D₊(X₁), with homogeneous coordinates [0 : 1].

theorem TauCeti.AlgebraicGeometry.projectiveLine.infinitySection_def (R : Type u) [CommRing R] : infinitySection R = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Polynomial.evalRingHom 0))) (polynomialChartι R 1)

The infinity section factors through the zero section of the opposite polynomial chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.infinitySection_over (R : Type u) [CommRing R] : CategoryTheory.CategoryStruct.comp (infinitySection R) (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)

The point at infinity is a section over the base ring.

instance TauCeti.AlgebraicGeometry.projectiveLine.instIsClosedImmersionInfinitySection (R : Type u) [CommRing R] : AlgebraicGeometry.IsClosedImmersion (infinitySection R)

theorem TauCeti.AlgebraicGeometry.projectiveLine.range_infinitySection (R : Type u) [CommRing R] : Set.range ⇑(infinitySection R) = (Set.range ⇑(polynomialChartι R 0))ᶜ

The boundary of the affine-line chart is precisely the infinity section, over any base ring.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.infinitySection_notMem_range_polynomialChartι (R : Type u) [CommRing R] (x : ↥(AlgebraicGeometry.Spec ↧R)) : (infinitySection R) x ∉ Set.range ⇑(polynomialChartι R 0)

Every point of the infinity section lies outside the affine-line chart.

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.infinity (K : Type u) [Field K] : ↥(projectiveLine K)

The point [0 : 1] at infinity on the projective line over a field.

theorem TauCeti.AlgebraicGeometry.projectiveLine.compl_range_polynomialChartι (K : Type u) [Field K] : (Set.range ⇑(polynomialChartι K 0))ᶜ = {infinity K}

Over a field the affine-line chart has exactly one boundary point.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.infinity_notMem_range_polynomialChartι (K : Type u) [Field K] : infinity K ∉ Set.range ⇑(polynomialChartι K 0)

The affine-line chart misses the point at infinity.

theorem TauCeti.AlgebraicGeometry.projectiveLine.isAffineOpen_basicOpen_coord (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))

The standard chart D₊(Xᵢ) is an affine open of the projective line.

instance TauCeti.AlgebraicGeometry.projectiveLine.isIntegral (R : Type u) [CommRing R] [IsDomain R] : AlgebraicGeometry.IsIntegral (projectiveLine R)

The projective line over a domain is integral: R[X₀, X₁] is a domain with a nonzero form of positive degree.

instance TauCeti.AlgebraicGeometry.projectiveLine.isRegularLocalRing_stalk (R : Type u) [CommRing R] [IsRegularRing R] (p : ↥(projectiveLine R)) : IsRegularLocalRing ↑((projectiveLine R).presheaf.stalk p)

The local rings of the projective line over a regular ring are regular: each is a local ring of a chart Spec R[X], and R[X] is a regular ring.

Functions on the charts

instance TauCeti.AlgebraicGeometry.projectiveLine.instNonemptyCarrierCarrierCommRingCatSpecOfAwayNatSymmetricAlgebraForallFinOfNatSubmoduleHomogeneousSubmoduleCoordOfNontrivial (R : Type u) [CommRing R] [Nontrivial R] (i : Fin 2) : Nonempty ↥(AlgebraicGeometry.Spec ↧(HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)))

instance TauCeti.AlgebraicGeometry.projectiveLine.instNonemptyCarrierCarrierCommRingCatToSchemeObjOpensSpecOfAwayNatSymmetricAlgebraForallFinOfNatSubmoduleHomogeneousSubmoduleCoordOpensFunctorAwayιTopOfNontrivial (R : Type u) [CommRing R] [Nontrivial R] (i : Fin 2) : Nonempty ↥↑((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R i)).obj ⊤)

theorem TauCeti.AlgebraicGeometry.projectiveLine.isAffineOpen_image_awayι_top (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R i)).obj ⊤)

The chart D₊(Xᵢ) is an affine open subscheme of the projective line.

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv (R : Type u) [CommRing R] (i : Fin 2) : ↑((projectiveLine R).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R i)).obj ⊤))) ≃+* Polynomial R

The functions on the chart D₊(Xᵢ) are the polynomials in X, the other coordinate over Xᵢ: restrict along the chart and dehomogenize.

theorem TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv_apply (R : Type u) [CommRing R] (i : Fin 2) (a : ↑((projectiveLine R).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R i)).obj ⊤)))) : (chartSectionsEquiv R i) a = (awayEquivPolynomial R i) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧(HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))).hom) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso (awayι R i) ⊤).hom) a))

chartSectionsEquiv restricts a function on the chart D₊(Xᵢ) along the chart and dehomogenizes it.

theorem TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv_symm_X (R : Type u) [CommRing R] (i : Fin 2) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧(HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))).hom) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso (awayι R i) ⊤).hom) ((chartSectionsEquiv R i).symm Polynomial.X)) = HomogeneousLocalization.Away.mk (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) ⋯ 1 (coord R i.rev) ⋯

The function X on the chart D₊(Xᵢ) restricts along the chart to the other coordinate over Xᵢ.

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv_appLE (R : Type u) [CommRing R] (i : Fin 2) (a : ↑((AlgebraicGeometry.Spec ↧R).presheaf.obj (Opposite.op ⊤))) : (chartSectionsEquiv R i) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) ⊤ ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R i)).obj ⊤) ⋯)) a) = Polynomial.C ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).hom) a)

On the chart D₊(Xᵢ), the functions on Spec R pulled back along the structure morphism are the constant polynomials.

theorem TauCeti.AlgebraicGeometry.projectiveLine.image_awayι_top (R : Type u) [CommRing R] (i : Fin 2) : (AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R i)).obj ⊤ = AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)

The chart D₊(Xᵢ), as the image of awayι, is the basic open set of Xᵢ.

theorem TauCeti.AlgebraicGeometry.projectiveLine.chartSectionsEquiv_awayToSection (R : Type u) [CommRing R] (i : Fin 2) (a : HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)) : (chartSectionsEquiv R i) ((CategoryTheory.ConcreteCategory.hom ((projectiveLine R).presheaf.map (CategoryTheory.eqToHom ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Proj.awayToSection (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))) a)) = (awayEquivPolynomial R i) a

chartSectionsEquiv sends the function Proj.awayToSection a on D₊(Xᵢ) to the dehomogenization of the fraction a.

theorem TauCeti.AlgebraicGeometry.projectiveLine.awayToSection_algebraMap (R : Type u) [CommRing R] (i : Fin 2) (c : R) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Proj.awayToSection (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))) ((algebraMap R ↑↧(HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))) c) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) ⊤ (AlgebraicGeometry.Proj.basicOpen (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i)) ⋯)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) c)

On the chart D₊(Xᵢ), the functions on Spec R pulled back along the structure morphism are the fractions c / 1 of the constants.

theorem TauCeti.AlgebraicGeometry.projectiveLine.val_map_baseRingToGlobalSections (R : Type u) [CommRing R] (r : R) (U : (projectiveLine R).Opens) (x : ↥U) : HomogeneousLocalization.val (↑((CategoryTheory.ConcreteCategory.hom ((projectiveLine R).presheaf.map (TopologicalSpace.Opens.leTop U).op)) ((AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections R (projectiveLine R)) r)) x) = (algebraMap R (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) r

On every open of the projective line, the restriction of the constant global function r takes the value r in every localization.

Smoothness

instance TauCeti.AlgebraicGeometry.projectiveLine.isStandardSmoothOfRelativeDimension_away (R : Type u) [CommRing R] (i : Fin 2) : Algebra.IsStandardSmoothOfRelativeDimension 1 R (HomogeneousLocalization.Away (SymmetricAlgebra.homogeneousSubmodule R (Fin 2 → R)) (coord R i))

The chart ring R[X₀, X₁]_(Xᵢ) is standard smooth of relative dimension one over R: it is the polynomial ring R[X] (awayEquivPolynomial).

theorem TauCeti.AlgebraicGeometry.projectiveLine.smoothOfRelativeDimension_awayι (R : Type u) [CommRing R] (i : Fin 2) : AlgebraicGeometry.SmoothOfRelativeDimension 1 (CategoryTheory.CategoryStruct.comp (awayι R i) (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R))

On the chart D₊(Xᵢ), the structure morphism of the projective line is smooth of relative dimension one.

instance TauCeti.AlgebraicGeometry.projectiveLine.smoothOfRelativeDimension (R : Type u) [CommRing R] : AlgebraicGeometry.SmoothOfRelativeDimension 1 (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R)

The projective line is smooth of relative dimension one over Spec R: it is covered by the two charts D₊(Xᵢ), each of which is the affine line Spec R[X] over Spec R.

Base change

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.baseChangeProjection (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] : projectiveLine S ⟶ projectiveLine R

The projection ℙ¹_S ⟶ ℙ¹_R for an R-algebra S: the coordinates S² of ℙ¹_S are identified with S ⊗[R] R², and Proj (Sym_S (S ⊗[R] R²)) maps to Proj (Sym_R R²) by extension of scalars.

theorem TauCeti.AlgebraicGeometry.projectiveLine.isPullback_baseChangeProjection (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] : CategoryTheory.IsPullback (baseChangeProjection R S) (projectiveLine S ↘ AlgebraicGeometry.Spec ↧S) (projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))

Base change of the projective line: for an R-algebra S, the square formed by the projection ℙ¹_S ⟶ ℙ¹_R, the structure morphisms, and Spec S ⟶ Spec R is a pullback, that is, ℙ¹_S = ℙ¹_R ×_{Spec R} Spec S.

The function field

noncomputable def TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv (R : Type u) [CommRing R] [IsDomain R] : ↑(projectiveLine R).functionField ≃ₐ[R] RatFunc R

The function field of the projective line over a domain R is R(X), as an R-algebra: it is the fraction field of the ring R[X] of functions on the chart D₊(X₀), the function X₁ / X₀ on that chart going to X (functionFieldEquiv_germToFunctionField).

@[simp]

theorem TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv_germToFunctionField (R : Type u) [CommRing R] [IsDomain R] (a : ↑((projectiveLine R).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R 0)).obj ⊤)))) : (functionFieldEquiv R) ((CategoryTheory.ConcreteCategory.hom ((projectiveLine R).germToFunctionField ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R 0)).obj ⊤))) a) = (algebraMap (Polynomial R) (RatFunc R)) ((chartSectionsEquiv R 0) a)

On the chart D₊(X₀), the identification of the function field of the projective line with R(X) is chartSectionsEquiv, that is, dehomogenization at X₀.

theorem TauCeti.AlgebraicGeometry.projectiveLine.functionFieldEquiv_symm_X (R : Type u) [CommRing R] [IsDomain R] : (functionFieldEquiv R).symm RatFunc.X = (CategoryTheory.ConcreteCategory.hom ((projectiveLine R).germToFunctionField ((AlgebraicGeometry.Scheme.Hom.opensFunctor (awayι R 0)).obj ⊤))) ((chartSectionsEquiv R 0).symm Polynomial.X)

The identification of the function field of the projective line with R(X) sends the function X₁ / X₀, the function on the chart D₊(X₀) restricting to X₁ / X₀ (chartSectionsEquiv_symm_X), to X.