Residue degree one above the rational-function place at infinity

For the infinity valuation ring of K(X), every integral rational function is congruent modulo the maximal ideal to a constant. Consequently its residue field is canonically a copy of K. When K is algebraically closed, the residue field at every prime above infinity in a finite separable extension of K(X) is therefore the same field, so the corresponding inertia degree is one.

noncomputable def BGS.CorvajaZannier.ratFuncInfinityConstantRingHom (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : K →+* ↥(RatFuncInfinityIntegers K)

Embed the constant field into the infinity valuation ring.

Equations

• BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K = RatFunc.C.codRestrict (BGS.CorvajaZannier.RatFuncInfinityIntegers K) ⋯

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.ratFuncInfinityConstantAlgebra (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 infinity inertia degree construction.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.ratFuncInfinityConstantAlgebra_coe (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (c : K) : ↑((algebraMap K ↥(RatFuncInfinityIntegers K)) c) = RatFunc.C c

The constant-field algebra map has underlying rational function RatFunc.C c.

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

theorem BGS.CorvajaZannier.ratFuncInfinityIntegers_exists_constant_mod_maximalIdeal (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (r : ↥(RatFuncInfinityIntegers K)) : ∃ (c : K), r - (algebraMap K ↥(RatFuncInfinityIntegers K)) c ∈ (ratFuncInfinityPlace K).asIdeal

Every rational function integral at infinity is congruent to a constant modulo the maximal ideal at infinity.

noncomputable def BGS.CorvajaZannier.ratFuncInfinityPlaceResidueEquiv (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : (ratFuncInfinityPlace K).asIdeal.ResidueField ≃ₐ[K] K

The residue field of the rational-function place at infinity is the constant field.

Equations

• BGS.CorvajaZannier.ratFuncInfinityPlaceResidueEquiv K = (AlgEquiv.ofBijective (Algebra.ofId K (BGS.CorvajaZannier.ratFuncInfinityPlace K).asIdeal.ResidueField) ⋯).symm

theorem BGS.CorvajaZannier.infinityInertiaIntegralClosureModuleFinite (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.infinityInertiaIntegralClosureIsIntegral (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)

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_inertiaDeg_eq_one (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] [IsAlgClosed K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : ↑((ratFuncInfinityPlace K).asIdeal.primesOver ↥(RatFuncInfinityIntegralClosure K L))) : (↑P).inertiaDeg ↥(RatFuncInfinityIntegers K) = 1

Over an algebraically closed constant field, every prime above the place at infinity has residue degree (inertia degree) one.