The field generated by projected coordinates is the fraction field of the image coordinate ring. Its inclusion in the source function field is constructed and identified on every coordinate-ring element.

def CCDN.projectionImageField {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) : IntermediateField K F

The subfield of F generated over K by the images of the forms a in the quotient by I; for F the function field of I, it is the function field of the image of the projection by a.

Equations

• CCDN.projectionImageField I a = IntermediateField.adjoin K (Set.range fun (i : σ) => (algebraMap (MvPolynomial τ K ⧸ I) F) ((Ideal.Quotient.mk I) (a i)))

structure CCDN.IsNoetherNormalization {K : Type u_1} {σ : Type u_3} {τ : Type u_4} [Field K] (I : Ideal (MvPolynomial τ K)) (a : σ → MvPolynomial τ K) : Prop

The forms a give a Noether normalization of the quotient by I: the coordinate map K[y] → K[x]/I is integral and injective, that is, the forms are algebraically independent modulo I and the quotient is finite over the polynomial ring they generate.

• integral : (projectionCoordinateMap I a).IsIntegral

  The quotient by I is integral over the subring generated by the forms.

• injective : Function.Injective ⇑(projectionCoordinateMap I a)

  The forms are algebraically independent modulo I.

structure CCDN.IsBirationalImage {K : Type u_1} {σ : Type u_3} {τ : Type u_4} [Field K] (I : Ideal (MvPolynomial τ K)) (a : σ → MvPolynomial τ K) [I.IsPrime] (f : MvPolynomial σ K) : Prop

The forms a map the variety of the prime I birationally onto the hypersurface f = 0: the images of the forms generate the function field of I, and the kernel of the coordinate map K[y] → K[x]/I is generated by the irreducible polynomial f.

• birational : projectionImageField I a = ⊤

  The images of the forms generate the function field of I.

• irreducible : Irreducible f

  The image equation f is irreducible.

• ker_eq : RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}

  The kernel of the coordinate map is the principal ideal generated by f.

structure CCDN.IsBirationalProjection {K : Type u_1} {σ : Type u_3} {τ : Type u_4} [Field K] (I : Ideal (MvPolynomial τ K)) (a : σ → MvPolynomial τ K) [I.IsPrime] (f : MvPolynomial σ K) extends CCDN.IsBirationalImage I a f : Prop

The forms a define a finite birational projection of the variety of the prime I onto the hypersurface f = 0: a birational image whose coordinate map K[y] → K[x]/I is moreover integral.

• birational : projectionImageField I a = ⊤
• irreducible : Irreducible f
• ker_eq : RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}
• integral : (projectionCoordinateMap I a).IsIntegral

  The quotient by I is integral over the subring generated by the forms.

theorem CCDN.IsBirationalImage.aeval_mem_iff {K : Type u_1} {σ : Type u_3} {τ : Type u_4} [Field K] {I : Ideal (MvPolynomial τ K)} [I.IsPrime] {a : σ → MvPolynomial τ K} {f : MvPolynomial σ K} (h : IsBirationalImage I a f) (g : MvPolynomial σ K) : (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g

For a birational image onto f = 0, a polynomial in the forms lies in the ideal exactly when it is a multiple of f.

theorem CCDN.IsBirationalImage.aeval_mem {K : Type u_1} {σ : Type u_3} {τ : Type u_4} [Field K] {I : Ideal (MvPolynomial τ K)} [I.IsPrime] {a : σ → MvPolynomial τ K} {f : MvPolynomial σ K} (h : IsBirationalImage I a f) : (MvPolynomial.aeval a) f ∈ I

The image equation of a birational image vanishes on the variety: substituting the forms into it gives an element of the ideal.

noncomputable def CCDN.projectionImageCoordinate {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) (i : σ) : ↥(projectionImageField I a)

The image of the form a i in F, as an element of the field generated by the projected coordinates.

Equations

• CCDN.projectionImageCoordinate I a i = ⟨(algebraMap (MvPolynomial τ K ⧸ I) F) ((Ideal.Quotient.mk I) (a i)), ⋯⟩

theorem CCDN.projectionImageCoordinate_eval_comp {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] [IsScalarTower K (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) : (projectionImageField I a).val.comp (MvPolynomial.aeval (projectionImageCoordinate I a)) = (IsScalarTower.toAlgHom K (MvPolynomial τ K ⧸ I) F).comp (projectionCoordinateMap I a)

Evaluating a polynomial at the projected coordinates and including the result in F agrees with applying the projection map to the quotient by I and then mapping to F.

noncomputable def CCDN.projectionImageFieldMap {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] [IsScalarTower K (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) : MvPolynomial σ K ⧸ RingHom.ker (projectionCoordinateMap I a) →ₐ[K] ↥(projectionImageField I a)

The image coordinate ring embeds into the generated image field.

Equations

• CCDN.projectionImageFieldMap I a = Ideal.Quotient.liftₐ (RingHom.ker (CCDN.projectionCoordinateMap I a)) (MvPolynomial.aeval (CCDN.projectionImageCoordinate I a)) ⋯

theorem CCDN.projectionImageFieldMap_comp_val {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] [IsScalarTower K (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) : (projectionImageField I a).val.comp (projectionImageFieldMap I a) = (IsScalarTower.toAlgHom K (MvPolynomial τ K ⧸ I) F).comp (Ideal.kerLiftAlg (projectionCoordinateMap I a))

The embedding of the image coordinate ring into the image field, followed by the inclusion into F, is the induced map from the image coordinate ring to the quotient by I, followed by the map to F.

theorem CCDN.projectionImageFieldMap_injective {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] [IsScalarTower K (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) [IsFractionRing (MvPolynomial τ K ⧸ I) F] : Function.Injective ⇑(projectionImageFieldMap I a)

When F is the fraction field of the quotient by the prime I, the embedding of the image coordinate ring into the image field is injective.

theorem CCDN.projectionImageFieldMap_isFractionRing {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra K F] (I : Ideal (MvPolynomial τ K)) [Algebra (MvPolynomial τ K ⧸ I) F] [IsScalarTower K (MvPolynomial τ K ⧸ I) F] (a : σ → MvPolynomial τ K) [IsFractionRing (MvPolynomial τ K ⧸ I) F] : have this := (projectionImageFieldMap I a).toAlgebra; IsFractionRing (MvPolynomial σ K ⧸ RingHom.ker (projectionCoordinateMap I a)) ↥(projectionImageField I a)

When F is the fraction field of the quotient by the prime I, the field generated by the projected coordinates is a fraction field of the image coordinate ring.