Documentation

TauCeti.FieldTheory.FunctionField.ConstantExtension.InseparableGenusDrop

The genus can drop under an inseparable constant field extension #

A finite separable constant field extension preserves the genus (TauCeti.genus_eq_genus_of_constantCompositum_eq_top). This file records the standard example showing that separability cannot be dropped (Stichtenoth, Section III.6, which refers to Deuring for it). Let p be an odd prime, k' = ๐”ฝ_p(s) and k = ๐”ฝ_p(t) โŠ† k' with t = s ^ p, so that k' / k is purely inseparable of degree p. Let F' = k'(w) and, inside it, x = w ^ 2 + s and y = w ^ p, which satisfy y ^ 2 = x ^ p - t. The subfield F = k(x, y) of F' is the function field of the curve y ^ 2 = x ^ p - t over k: since X ^ p - t is squarefree of degree p over k, the field F / k has genus (p - 1) / 2 and exact constant field k. The compositum F ยท k' is all of F', because w = y / (x - s) ^ ((p - 1) / 2), and F' = k'(w) has genus 0.

Main declarations #

References #

The constant fields k = ๐”ฝ_p(s ^ p) โŠ† k' = ๐”ฝ_p(s) #

source
@[reducible, inline]
noncomputable abbrev TauCeti.GenusDrop.constants (p : โ„•) [hp : Fact (Nat.Prime p)] :
IntermediateField (ZMod p) (RatFunc (ZMod p))

The constant field k = ๐”ฝ_p(t), realized as the subfield ๐”ฝ_p(s ^ p) of k' = ๐”ฝ_p(s).

Equations
Instances For
    source
    noncomputable def TauCeti.GenusDrop.radicand (p : โ„•) [hp : Fact (Nat.Prime p)] :
    โ†ฅ(constants p)

    The radicand t = s ^ p, as an element of k.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GenusDrop.coe_radicand (p : โ„•) [hp : Fact (Nat.Prime p)] :
      โ†‘(radicand p) = RatFunc.X ^ p
      source
      theorem TauCeti.GenusDrop.finrank_constants (p : โ„•) [hp : Fact (Nat.Prime p)] :
      Module.finrank (โ†ฅ(constants p)) (RatFunc (ZMod p)) = p

      k' / k has degree p.

      source
      theorem TauCeti.GenusDrop.X_notMem_constants (p : โ„•) [hp : Fact (Nat.Prime p)] :
      RatFunc.X โˆ‰ constants p

      s does not lie in k.

      source
      theorem TauCeti.GenusDrop.pow_ne_radicand (p : โ„•) [hp : Fact (Nat.Prime p)] (b : โ†ฅ(constants p)) :
      b ^ p โ‰  radicand p

      t is not a p-th power in k: a p-th root of s ^ p in k' is s, which is not in k.

      source
      theorem TauCeti.GenusDrop.irreducible_X_pow_sub_C_radicand (p : โ„•) [hp : Fact (Nat.Prime p)] :
      Irreducible (Polynomial.X ^ p - Polynomial.C (radicand p))

      X ^ p - t is irreducible over k.

      source
      theorem TauCeti.GenusDrop.not_isSeparable_constants (p : โ„•) [hp : Fact (Nat.Prime p)] :
      ยฌAlgebra.IsSeparable (โ†ฅ(constants p)) (RatFunc (ZMod p))

      k' / k is not separable: it is purely inseparable (TauCeti.RatFunc.isPurelyInseparable_adjoin_X_pow) and s โˆ‰ k.

      The function fields F = k(x, y) โŠ† F' = k'(w) #

      source
      noncomputable def TauCeti.GenusDrop.sElement (p : โ„•) [hp : Fact (Nat.Prime p)] :
      RatFunc (RatFunc (ZMod p))

      s, viewed in F' = k'(w).

      Equations
      Instances For
        source
        noncomputable def TauCeti.GenusDrop.genX (p : โ„•) [hp : Fact (Nat.Prime p)] :
        RatFunc (RatFunc (ZMod p))

        x = w ^ 2 + s.

        Equations
        Instances For
          source
          noncomputable def TauCeti.GenusDrop.genY (p : โ„•) [hp : Fact (Nat.Prime p)] :
          RatFunc (RatFunc (ZMod p))

          y = w ^ p.

          Equations
          Instances For
            source
            theorem TauCeti.GenusDrop.transcendental_genX (p : โ„•) [hp : Fact (Nat.Prime p)] :
            Transcendental (โ†ฅ(constants p)) (genX p)

            x is transcendental over k: otherwise w ^ 2 = x - s, hence w, would be algebraic over k'.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.GenusDrop.instAlgebraRatFunc (p : โ„•) [hp : Fact (Nat.Prime p)] :
            Algebra (RatFunc โ†ฅ(constants p)) (RatFunc (RatFunc (ZMod p)))

            The k(x)-algebra structure of F', with RatFunc.X acting as x.

            Equations
            source
            instance TauCeti.GenusDrop.instIsScalarTowerRatFunc (p : โ„•) [hp : Fact (Nat.Prime p)] :
            IsScalarTower (โ†ฅ(constants p)) (RatFunc โ†ฅ(constants p)) (RatFunc (RatFunc (ZMod p)))
            source
            theorem TauCeti.GenusDrop.algebraMap_radicand (p : โ„•) [hp : Fact (Nat.Prime p)] :
            (algebraMap (โ†ฅ(constants p)) (RatFunc (RatFunc (ZMod p)))) (radicand p) = sElement p ^ p

            t, viewed in F', is s ^ p.

            source
            theorem TauCeti.GenusDrop.sq_genY (p : โ„•) [hp : Fact (Nat.Prime p)] :
            genY p ^ 2 = genX p ^ p - sElement p ^ p

            The equation y ^ 2 = x ^ p - t in F': (w ^ 2 + s) ^ p = w ^ (2 p) + s ^ p in characteristic p.

            source
            theorem TauCeti.GenusDrop.algebraMap_X_pow_sub_C_radicand (p : โ„•) [hp : Fact (Nat.Prime p)] :
            (algebraMap (RatFunc โ†ฅ(constants p)) (RatFunc (RatFunc (ZMod p)))) ((algebraMap (Polynomial โ†ฅ(constants p)) (RatFunc โ†ฅ(constants p))) (Polynomial.X ^ p - Polynomial.C (radicand p))) = genX p ^ p - sElement p ^ p

            The value f(x) of f = X ^ p - C t at x, viewed in F'.

            source
            noncomputable def TauCeti.GenusDrop.curveField (p : โ„•) [hp : Fact (Nat.Prime p)] :
            IntermediateField (RatFunc โ†ฅ(constants p)) (RatFunc (RatFunc (ZMod p)))

            The function field F = k(x, y) of y ^ 2 = x ^ p - t, as the subfield k(x)(y) of F'.

            Equations
            Instances For
              source
              noncomputable def TauCeti.GenusDrop.genY' (p : โ„•) [hp : Fact (Nat.Prime p)] :
              โ†ฅ(curveField p)

              y, as an element of F.

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.GenusDrop.coe_genY' (p : โ„•) [hp : Fact (Nat.Prime p)] :
                โ†‘(genY' p) = genY p
                source
                theorem TauCeti.GenusDrop.adjoin_genY'_eq_top (p : โ„•) [hp : Fact (Nat.Prime p)] :
                (RatFunc โ†ฅ(constants p))โŸฎgenY' pโŸฏ = โŠค

                y generates F over k(x).

                source
                theorem TauCeti.GenusDrop.sq_genY' (p : โ„•) [hp : Fact (Nat.Prime p)] :
                genY' p ^ 2 = (algebraMap (RatFunc โ†ฅ(constants p)) โ†ฅ(curveField p)) ((algebraMap (Polynomial โ†ฅ(constants p)) (RatFunc โ†ฅ(constants p))) (Polynomial.X ^ p - Polynomial.C (radicand p)))

                The defining equation y ^ 2 = x ^ p - t of F, in the form y ^ 2 = f(x) with f = X ^ p - C t.

                source
                theorem TauCeti.GenusDrop.isIntegrallyClosedIn_curveField (p : โ„•) [hp : Fact (Nat.Prime p)] (h2 : p โ‰  2) :
                IsIntegrallyClosedIn โ†ฅ(constants p) โ†ฅ(curveField p)

                k is the exact constant field of F.

                source
                theorem TauCeti.GenusDrop.genus_curveField (p : โ„•) [hp : Fact (Nat.Prime p)] (h2 : p โ‰  2) :
                genus โ†ฅ(constants p) โ†ฅ(curveField p) = (p - 1) / 2

                The genus of y ^ 2 = x ^ p - t over k = ๐”ฝ_p(t) is (p - 1) / 2.

                source
                theorem TauCeti.GenusDrop.X_eq_genY_div (p : โ„•) [hp : Fact (Nat.Prime p)] (h2 : p โ‰  2) :
                RatFunc.X = genY p / (genX p - sElement p) ^ ((p - 1) / 2)

                w = y / (x - s) ^ ((p - 1) / 2).

                source
                theorem TauCeti.GenusDrop.constantCompositum_eq_top (p : โ„•) [hp : Fact (Nat.Prime p)] (h2 : p โ‰  2) :
                constantCompositum (โ†ฅ(curveField p)) (RatFunc (ZMod p)) (RatFunc (RatFunc (ZMod p))) = โŠค

                F' = F ยท k': the extension F' / F is the constant field extension by k'.

                source
                theorem TauCeti.GenusDrop.genus_lt_genus (p : โ„•) [hp : Fact (Nat.Prime p)] (h2 : p โ‰  2) :
                genus (RatFunc (ZMod p)) (RatFunc (RatFunc (ZMod p))) < genus โ†ฅ(constants p) โ†ฅ(curveField p)

                The genus drops: F' / k' is rational, of genus 0, while F / k has genus (p - 1) / 2 โ‰ฅ 1.