Smoothness and integrality of the projective line

This file identifies both standard affine charts of the projective line with a one-variable polynomial ring. The explicit presentations prove that the structure morphism is smooth of relative dimension one. The same charts, together with the homogeneous zero ideal, show that the projective line is integral; properness and finite type then imply it is Noetherian.

These instances are the target-side geometric input for the finite morphism used in the product-formula proof.

noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.standardAffinePolynomialEquiv (K : Type u) [Field K] : Polynomial ↥(homogeneousPieces K 0) ≃+* ↑((scheme K).presheaf.obj (Opposite.op (standardAffineOpen K)))

The standard affine chart of the projective line is a polynomial line over the degree-zero homogeneous coordinate ring.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.standardAffinePolynomialEquiv_X (K : Type u) [Field K] : (standardAffinePolynomialEquiv K) Polynomial.X = affineCoordinate K

Under the polynomial presentation of the standard chart, the polynomial variable is the affine coordinate X₀ / X₁.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.affineCoordinate_ne_zero (K : Type u) [Field K] : affineCoordinate K ≠ 0

The standard affine coordinate on ℙ¹ is nonzero.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.isAffineOpen_standardAffineOpen (K : Type u) [Field K] : AlgebraicGeometry.IsAffineOpen (standardAffineOpen K)

The standard chart D₊(X₁) is affine.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.standardAffineOpen_sup_infinityAffineOpen_eq_top (K : Type u) [Field K] : standardAffineOpen K ⊔ infinityAffineOpen K = ⊤

The two standard affine charts cover the projective line.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.span_affineCoordinate_isPrime (K : Type u) [Field K] : (Ideal.span {affineCoordinate K}).IsPrime

The zero locus of the affine coordinate is a prime point of the standard chart.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.span_affineCoordinate_isMaximal (K : Type u) [Field K] : (Ideal.span {affineCoordinate K}).IsMaximal

The zero locus of the affine coordinate is a maximal point of the standard chart.

noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPrime (K : Type u) [Field K] : PrimeSpectrum ↑((scheme K).presheaf.obj (Opposite.op (standardAffineOpen K)))

The prime of the standard affine chart cut out by its coordinate.

Equations

• TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPrime K = { asIdeal := Ideal.span {TauCeti.AlgebraicGeometry.ProjectiveLine.affineCoordinate K}, isPrime := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPrime_asIdeal (K : Type u) [Field K] : (zeroPrime K).asIdeal = Ideal.span {affineCoordinate K}

noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPoint (K : Type u) [Field K] : ↥(scheme K)

The zero point [0 : 1] of the projective line, defined through the standard affine chart.

Equations

• TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPoint K = ⋯.fromSpec (TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPrime K)

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.zeroPoint_mem_standardAffineOpen (K : Type u) [Field K] : zeroPoint K ∈ standardAffineOpen K

The zero point belongs to the standard affine chart.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.primeIdealOf_zeroPoint (K : Type u) [Field K] : ⋯.primeIdealOf ⟨zeroPoint K, ⋯⟩ = zeroPrime K

In the standard affine chart, the prime ideal of the zero point is generated by the affine coordinate.

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.primeIdealOf_zeroPoint_asIdeal (K : Type u) [Field K] : (⋯.primeIdealOf ⟨zeroPoint K, ⋯⟩).asIdeal = Ideal.span {affineCoordinate K}

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.primeIdealOf_zeroPoint_asIdeal_of_mem (K : Type u) [Field K] (hz : zeroPoint K ∈ standardAffineOpen K) : (⋯.primeIdealOf ⟨zeroPoint K, hz⟩).asIdeal = Ideal.span {affineCoordinate K}

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.affineCoordinate_mem_primeIdealOf_iff_eq_zeroPoint (K : Type u) [Field K] (y : ↥(scheme K)) (hy : y ∈ standardAffineOpen K) : affineCoordinate K ∈ (⋯.primeIdealOf ⟨y, hy⟩).asIdeal ↔ y = zeroPoint K

A point of the standard chart contains the affine coordinate in its prime ideal exactly when it is the zero point.

noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.infinityAffinePolynomialEquiv (K : Type u) [Field K] : Polynomial ↥(homogeneousPieces K 0) ≃+* ↑((scheme K).presheaf.obj (Opposite.op (infinityAffineOpen K)))

The affine chart containing infinity is a polynomial line over the degree-zero homogeneous coordinate ring.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.infinityAffinePolynomialEquiv_X (K : Type u) [Field K] : (infinityAffinePolynomialEquiv K) Polynomial.X = inverseAffineCoordinate K

Under the polynomial presentation of the chart at infinity, the polynomial variable is the inverse affine coordinate X₁ / X₀.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.inverseAffineCoordinate_ne_zero (K : Type u) [Field K] : inverseAffineCoordinate K ≠ 0

The inverse affine coordinate on ℙ¹ is nonzero.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.isAffineOpen_infinityAffineOpen (K : Type u) [Field K] : AlgebraicGeometry.IsAffineOpen (infinityAffineOpen K)

The chart D₊(X₀) containing infinity is affine.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.span_inverseAffineCoordinate_isPrime (K : Type u) [Field K] : (Ideal.span {inverseAffineCoordinate K}).IsPrime

The zero locus of the inverse affine coordinate is a prime point of the chart at infinity.

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.span_inverseAffineCoordinate_isMaximal (K : Type u) [Field K] : (Ideal.span {inverseAffineCoordinate K}).IsMaximal

The zero locus of the inverse affine coordinate is a maximal point of the chart at infinity.

noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPrime (K : Type u) [Field K] : PrimeSpectrum ↑((scheme K).presheaf.obj (Opposite.op (infinityAffineOpen K)))

The prime of the affine chart at infinity cut out by the inverse coordinate.

Equations

• TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPrime K = { asIdeal := Ideal.span {TauCeti.AlgebraicGeometry.ProjectiveLine.inverseAffineCoordinate K}, isPrime := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPrime_asIdeal (K : Type u) [Field K] : (infinityPrime K).asIdeal = Ideal.span {inverseAffineCoordinate K}

noncomputable def TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPoint (K : Type u) [Field K] : ↥(scheme K)

The point [1 : 0] of the projective line, defined through the affine chart at infinity.

Equations

• TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPoint K = ⋯.fromSpec (TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPrime K)

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.infinityPoint_mem_infinityAffineOpen (K : Type u) [Field K] : infinityPoint K ∈ infinityAffineOpen K

The point at infinity belongs to the chart D₊(X₀).

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.primeIdealOf_infinityPoint (K : Type u) [Field K] : ⋯.primeIdealOf ⟨infinityPoint K, ⋯⟩ = infinityPrime K

In the chart at infinity, the prime ideal of [1 : 0] is generated by the inverse affine coordinate.

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.primeIdealOf_infinityPoint_asIdeal (K : Type u) [Field K] : (⋯.primeIdealOf ⟨infinityPoint K, ⋯⟩).asIdeal = Ideal.span {inverseAffineCoordinate K}

@[simp]

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.primeIdealOf_infinityPoint_asIdeal_of_mem (K : Type u) [Field K] (hinf : infinityPoint K ∈ infinityAffineOpen K) : (⋯.primeIdealOf ⟨infinityPoint K, hinf⟩).asIdeal = Ideal.span {inverseAffineCoordinate K}

theorem TauCeti.AlgebraicGeometry.ProjectiveLine.inverseAffineCoordinate_mem_primeIdealOf_iff_eq_infinityPoint (K : Type u) [Field K] (y : ↥(scheme K)) (hy : y ∈ infinityAffineOpen K) : inverseAffineCoordinate K ∈ (⋯.primeIdealOf ⟨y, hy⟩).asIdeal ↔ y = infinityPoint K

A point of the chart at infinity contains the inverse affine coordinate in its prime ideal exactly when it is the point at infinity.

instance TauCeti.AlgebraicGeometry.ProjectiveLine.instSmoothOfRelativeDimensionOfNatNatStructureMap (K : Type u) [Field K] : AlgebraicGeometry.SmoothOfRelativeDimension 1 (structureMap K)

instance TauCeti.AlgebraicGeometry.ProjectiveLine.instIsIntegralScheme (K : Type u) [Field K] : AlgebraicGeometry.IsIntegral (scheme K)

instance TauCeti.AlgebraicGeometry.ProjectiveLine.instIsNoetherianScheme (K : Type u) [Field K] : AlgebraicGeometry.IsNoetherian (scheme K)