Constants surject onto residue fields of all function-field places

Let L / K(X) be finite and separable, with K algebraically closed. At a finite place of L, the residue field is integral over the residue field of the place below it; the latter is canonically K. The same argument applies above infinity, using the explicit residue equivalence at the rational function infinity place. Thus constants surject onto every residue field.

This is the exact coefficient-lifting input used by Corvaja--Zannier case (i): equal negative leading terms can be cancelled by a genuine constant.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.residuePolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension residue surjectivity construction.

Equations

• BGS.CorvajaZannier.residuePolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.residuePolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.CorvajaZannier.residueFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.residueFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.residuePolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.CorvajaZannier.residueFiniteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.residueFiniteIntegralClosureConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the finite extension residue surjectivity construction.

Equations

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

theorem BGS.CorvajaZannier.residueFiniteIntegralClosureConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.residueInfinityConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the finite extension residue surjectivity construction.

Equations

• BGS.CorvajaZannier.residueInfinityConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

theorem BGS.CorvajaZannier.residueInfinityConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsScalarTower K (↥(RatFuncInfinityIntegers K)) (RatFunc K)

theorem BGS.CorvajaZannier.residueInfinityIntegralClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.residueInfinityIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.residueInfinityIntegralClosureConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the finite extension residue surjectivity construction.

Equations

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

theorem BGS.CorvajaZannier.residueInfinityIntegralClosureConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_constantResidue_surjective (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] (q : FiniteExtensionFinitePlace K L) : Function.Surjective ⇑(algebraMap K q.asIdeal.ResidueField)

Constants surject onto the residue field of every finite place of a finite separable extension of K(X), when K is algebraically closed.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_constantResidue_surjective (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] (P : ↑(FiniteExtensionInfinityPlace K L)) : Function.Surjective ⇑(algebraMap K (↑P).ResidueField)

Constants surject onto the residue field of every place above infinity in a finite separable extension of K(X), when K is algebraically closed.