def CurveMorphism.IsRegularNonzeroAtOver {k : Type u} [Field k] {f₀ : Polynomial (Polynomial k)} {K : Type u} [Field K] [Algebra k K] (φ : ProjectiveCurve.FunctionField f₀) (P : ProjectiveCurve.AffinePointOver f₀ K) : Prop

Predicate asserting that a function field element φ on the affine curve defined by f₀ is regular and nonzero at an affine point P over an extension K: there is a representation φ = g / h with both h(P) and g(P) nonzero.

def CurveMorphism.IsRegularAtOver {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (ProjectiveCurve.CoordinateRing f₁)] (φ : ProjectiveCurve.RationalMap f₁ f₂) {K : Type u} [Field K] [Algebra k K] (P : ProjectiveCurve.AffinePointOver f₁ K) : Prop

Predicate asserting that the projective rational map φ from the curve f₁ to the curve f₂ is regular at an affine point P: there exists a nonzero common scaling μ so that all three coordinate components are regular at P and at least one is nonzero (so the resulting projective point is well-defined).

inductive CurveMorphism.ProjectiveCurvePointOver {k : Type u} [Field k] (f₀ : Polynomial (Polynomial k)) (K : Type u) [Field K] [Algebra k K] : Type u

The type of K-points of the projective curve cut out by f₀, encoded as either an affine point or a point at infinity given by projective coordinates (a : b : 0) with (a, b) not both zero.

• affine {k : Type u} [Field k] {f₀ : Polynomial (Polynomial k)} {K : Type u} [Field K] [Algebra k K] : ProjectiveCurve.AffinePointOver f₀ K → ProjectiveCurvePointOver f₀ K
• atInfinity {k : Type u} [Field k] {f₀ : Polynomial (Polynomial k)} {K : Type u} [Field K] [Algebra k K] (a b : K) : a ≠ 0 ∨ b ≠ 0 → ProjectiveCurvePointOver f₀ K

def CurveMorphism.IsRegularAtProjectivePoint {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (ProjectiveCurve.CoordinateRing f₁)] (φ : ProjectiveCurve.RationalMap f₁ f₂) {K : Type u} [Field K] [Algebra k K] (P : ProjectiveCurvePointOver f₁ K) : Prop

Predicate asserting that the rational map φ is regular at a projective point P, defined by cases: at an affine point we use IsRegularAtOver, and at a point at infinity we ask for a common denominator whose numerators are not all zero.

def CurveMorphism.IsMorphism {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (ProjectiveCurve.CoordinateRing f₁)] (φ : ProjectiveCurve.RationalMap f₁ f₂) : Prop

IsMorphism φ says the rational map φ is everywhere defined, i.e. regular at every projective point over every algebraically closed extension of k. This matches Definition 4.14: a rational map that is defined everywhere is called a morphism.

structure CurveMorphism.Morphism {k : Type u} [Field k] (f₁ f₂ : Polynomial (Polynomial k)) [IsDomain (ProjectiveCurve.CoordinateRing f₁)] : Type u

A morphism of projective curves from f₁ to f₂: a rational map together with a proof that it is regular everywhere. Corresponds to the notion of morphism of curves in Definition 4.14.

• toRationalMap : ProjectiveCurve.RationalMap f₁ f₂
• regular_everywhere : IsMorphism self.toRationalMap

theorem CurveMorphism.Morphism.isMorphism {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (ProjectiveCurve.CoordinateRing f₁)] (φ : Morphism f₁ f₂) : IsMorphism φ.toRationalMap

A Morphism is in particular a rational map satisfying the IsMorphism predicate.

def CurveMorphism.Morphism.ofIsMorphism {k : Type u} [Field k] {f₁ f₂ : Polynomial (Polynomial k)} [IsDomain (ProjectiveCurve.CoordinateRing f₁)] (φ : ProjectiveCurve.RationalMap f₁ f₂) (h : IsMorphism φ) : Morphism f₁ f₂

Build a Morphism from a rational map together with a proof that it is regular everywhere.