Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ConstantFieldInfinityBase

The rational-function place at infinity under coefficient extension #

Coefficient extension K(X) → E(X) preserves the integer degree of every rational function, hence preserves the valuation at infinity exactly. It therefore restricts to an injective local homomorphism between the two infinity valuation rings. The maximal ideal of the enlarged valuation ring contracts to the original maximal ideal.

This is the base-place comparison. It does not identify the integral closures of these valuation rings inside a further function field.

source
theorem BGS.HasseWeil.ratFuncCoefficientAlgHom_intDegree (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (z : RatFunc K) :
((ratFuncCoefficientAlgHom K E) z).intDegree = z.intDegree

Injective coefficient extension preserves rational-function integer degree.

source
theorem BGS.HasseWeil.ratFuncCoefficientAlgHom_C (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] (c : K) :
(ratFuncCoefficientAlgHom K E) (RatFunc.C c) = RatFunc.C ((algebraMap K E) c)

Coefficient extension has the expected value on constants.

source
theorem BGS.HasseWeil.ratFuncCoefficientAlgHom_inftyValuation (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] (z : RatFunc K) :
(RatFunc.inftyValuation E) ((ratFuncCoefficientAlgHom K E) z) = (RatFunc.inftyValuation K) z

Coefficient extension preserves the valuation at infinity exactly.

source
noncomputable def BGS.HasseWeil.ratFuncInfinityIntegersRingHom (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
↥(CorvajaZannier.RatFuncInfinityIntegers K) →+* ↥(CorvajaZannier.RatFuncInfinityIntegers E)

Coefficient extension restricted to the infinity valuation rings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem BGS.HasseWeil.ratFuncInfinityIntegersRingHom_coe (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] (z : ↥(CorvajaZannier.RatFuncInfinityIntegers K)) :
    ↑((ratFuncInfinityIntegersRingHom K E) z) = (ratFuncCoefficientAlgHom K E) ↑z
    source
    theorem BGS.HasseWeil.ratFuncInfinityIntegersRingHom_injective (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
    Function.Injective ⇑(ratFuncInfinityIntegersRingHom K E)
    source
    instance BGS.HasseWeil.ratFuncInfinityIntegersRingHom_isLocalHom (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
    IsLocalHom (ratFuncInfinityIntegersRingHom K E)

    The map of infinity valuation rings is local because it reflects the valuation-one unit condition.

    source
    theorem BGS.HasseWeil.ratFuncInfinityIntegersRingHom_comap_maximalIdeal (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
    Ideal.comap (ratFuncInfinityIntegersRingHom K E) (IsLocalRing.maximalIdeal ↥(CorvajaZannier.RatFuncInfinityIntegers E)) = IsLocalRing.maximalIdeal ↥(CorvajaZannier.RatFuncInfinityIntegers K)

    The maximal ideal at infinity over E contracts to the maximal ideal at infinity over K.

    source
    theorem BGS.HasseWeil.ratFuncInfinityIntegersRingHom_comap_infinityPlace (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
    Ideal.comap (ratFuncInfinityIntegersRingHom K E) (CorvajaZannier.ratFuncInfinityPlace E).asIdeal = (CorvajaZannier.ratFuncInfinityPlace K).asIdeal

    Height-one-place form of maximal-ideal contraction.

    source
    noncomputable def BGS.HasseWeil.ratFuncInfinityResidueFieldRingHom (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
    (CorvajaZannier.ratFuncInfinityPlace K).asIdeal.ResidueField →+* (CorvajaZannier.ratFuncInfinityPlace E).asIdeal.ResidueField

    The induced map between the two infinity residue fields.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.HasseWeil.ratFuncInfinityResidueFieldRingHom_injective (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] :
      Function.Injective ⇑(ratFuncInfinityResidueFieldRingHom K E)