Nyll.SchemeTheory.PlaneCurves.ConstantExtension

Module documentation

Monic normalization after a finite constant extension

For a finite ground field, a generic linear projection need not be defined over the ground field itself. Fried--Jarden therefore first passes to a suitable finite constant extension. This file develops that missing constant-extension form of linear monic normalization.

theorem

exists_algebraicClosure_linearChangeY_leadingCoeff_isUnit

L37 ↗

FieldArithmetic.Chapter06.FiniteExtensionMonicNormalization.exists_algebraicClosure_linearChangeY_leadingCoeff_isUnit

Documentation

After extending coefficients to an algebraic closure, a nonzero plane equation admits a linear change with unit leading coefficient.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FiniteExtensionMonicNormalization
open AffinePlaneCurve MonicPlaneCurveProjection
open PlaneCurveMonicNormalization
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_algebraicClosure_linearChangeY_leadingCoeff_isUnit
    {Ω : Type*} [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
    {f : BivariatePolynomial K} (hf : f ≠ 0) :
    ∃ c : Fin 1 → Ω,
      IsUnit
        (yPolynomial
          (linearChangeY c
            (MvPolynomial.map
              (algebraMap K Ω) f))).leadingCoeff

Module documentation

Monic normalization after a finite constant extension

Declarations

exists_algebraicClosure_linearChangeY_leadingCoeff_isUnit