Range of frobenius minus one

Stream: Is there code for X?

[Aaron Liu]

Do we have this already? I need this kind of result for characterizing finite nimber arithmetic.

import Mathlib

theorem FiniteField.ker_trace_eq_range_coe_frobeniusAlgHom_sub_id (K F : Type*)
    [Field K] [Field F] [Algebra K F] [Fintype K] [Module.Finite K F] :
    LinearMap.ker (Algebra.trace K F) =
    LinearMap.range ((FiniteField.frobeniusAlgHom K F).toLinearMap - LinearMap.id) := by
  have : Finite F := Module.finite_of_finite K
  apply SetLike.coe_injective
  refine (Set.eq_of_subset_of_ncard_le ?_ ?_).symm
  · rw [LinearMap.coe_range, Set.range_subset_iff]
    intro x
    rw [SetLike.mem_coe, LinearMap.mem_ker]
    apply (FaithfulSMul.algebraMap_eq_zero_iff K F).mp
    rw [trace_eq_sum_automorphisms]
    simp_rw [LinearMap.sub_apply, map_sub, Finset.sum_sub_distrib]
    conv =>
      enter [1, 1, 2, σ]
      change (Equiv.mulRight (FiniteField.frobeniusAlgEquiv K F (ringExpChar F)) σ) x
    rw [Equiv.sum_comp (Equiv.mulRight (FiniteField.frobeniusAlgEquiv K F
      (ringExpChar F))) (fun σ => σ x)]
    exact sub_self _
  · classical
    trans Nat.card F / Nat.card K
    · let T : Polynomial F := ∑ n ∈ Finset.range (Module.finrank K F), .X ^ Nat.card K ^ n
      have hT : T.natDegree ≤ Nat.card F / Nat.card K := by
        have ll : Nat.card K ^ Module.finrank K F = Nat.card F := by
          conv =>
            enter [1, 1]
          rw [← Module.natCard_eq_pow_finrank]
        apply Polynomial.natDegree_sum_le_of_forall_le
        intro i hi
        rw [Polynomial.natDegree_pow, Polynomial.natDegree_X, Nat.mul_one,
          Nat.le_div_iff_mul_le Nat.card_pos, ← Nat.pow_add_one, ← ll,
          Nat.pow_le_pow_iff_right Finite.one_lt_card]
        rwa [Finset.mem_range, Nat.lt_iff_add_one_le] at hi
      have hz : T ≠ 0 := by
        apply ne_of_apply_ne (Polynomial.coeff · 1)
        simp [T, eq_comm.trans Nat.pow_eq_one, Fintype.one_lt_card.ne', Module.finrank_pos]
      refine le_trans ?_ hT
      refine le_trans (le_trans ?_ (Multiset.toFinset_card_le _)) (Polynomial.card_roots' _)
      rw [← Set.ncard_coe_finset]
      refine (Set.ncard_le_ncard ?_)
      intro x hx
      rw [Finset.mem_coe, Multiset.mem_toFinset, Polynomial.mem_roots hz]
      rw [SetLike.mem_coe, LinearMap.mem_ker] at hx
      apply (FaithfulSMul.algebraMap_eq_zero_iff K F).mpr at hx
      rw [FiniteField.algebraMap_trace_eq_sum_pow] at hx
      simpa [T, Polynomial.eval_finset_sum] using hx
    · set L := (FiniteField.frobeniusAlgHom K F).toLinearMap - LinearMap.id
      rw [← Nat.card_coe_set_eq]
      refine le_of_le_of_eq ?_ (Nat.card_congr (LinearMap.quotKerEquivRange L).toEquiv)
      apply Nat.div_le_of_le_mul
      suffices np : Nat.card (LinearMap.ker L) = Nat.card K by
        rw [Submodule.card_eq_card_quotient_mul_card (LinearMap.ker L), np]
      apply le_antisymm
      · have hxx : (.X ^ Nat.card K - .X : Polynomial F).natDegree = Nat.card K := by
          compute_degree
          · simp [Fintype.one_lt_card.ne]
          · simp
          · simp [Nat.one_le_iff_ne_zero]
        refine le_trans
          (le_trans ?_ (Multiset.toFinset_card_le _))
          (le_of_le_of_eq (Polynomial.card_roots' _) hxx)
        rw [← Set.ncard_coe_finset]
        refine le_of_eq_of_le
          (Nat.card_coe_set_eq (LinearMap.ker L : Set F)) (Set.ncard_le_ncard ?_)
        intro x hx
        rw [Finset.mem_coe, Multiset.mem_toFinset, Polynomial.mem_roots
          (ne_of_apply_ne (Polynomial.coeff · 1) (by simp [Fintype.one_lt_card.ne]))]
        simpa [L] using hx
      · exact (Nat.card_le_card_of_injective (fun u => ⟨algebraMap K F u, by simp [L]⟩)
          (by simp [Function.Injective]))

[Aaron Liu]

Also, does this only work for finite fields?

[Antoine Chambert-Loir]

It generalizes (with almost the same statement) for Galois extensions whose Galois group is cyclic; the Frobenius automorphism has to be replaced by a generator of the Galois groups.

[Antoine Chambert-Loir]

It also generalizes to any finite extensions $K \to L$ which are Galois of group $G$, under the form $H^1(G, L)=0$.

[Aaron Liu]

oh is this some statement about cohomology

[Aaron Liu]

oh I see it now

[Kevin Buzzard]

And indeed you already proved $H^1(G,L)=0$ earlier this year because $H^1(G,K[G])=0$ because $K[G]$ has no higher group cohomology, and the normal basis theorem shows $L=K[G]$ as $K[G]$-modules (certainly not as rings but this is just a question about $G$-modules).

Historically I imagine that this is how group cohomology got invented, there were lots of calculations which had similar answers and then eventually people stumbled upon a general definition of $H^1$, $H^2$ and then $H^n$. All the theorems of class field theory were proved without any use of cohomology at all, I never looked at the papers but I just imagine it's people stumbling around in the dark.

[Aaron Liu]

that's great but really I want something that tells me when $X^2+X+\alpha$ has a root (in char2) based on the absolute trace of $\alpha$ which has a nice formula which I can prove inductively

[Aaron Liu]

and I thought "oh I can generalize this" so I did

[Aaron Liu]

but I don't want it generalized so much that it becomes hard to apply to my use case

[Kevin Buzzard]

We have a concrete description of $H^1$ as 1-cocycles over 1-coboundaries, and should probably have API saying "if $H^1=0$ then 1-cocycles = 1-coboundaries"; we also have concrete descriptions of what a 1-cocycle and 1-coboundary are. The API for group cohomology was designed to be useful in situations like this.

[Kevin Buzzard]

Aaron Liu said:

that's great but really I want something that tells me when $X^2+X+\alpha$ has a root (in char2) based on the absolute trace of $\alpha$ which has a nice formula which I can prove inductively

Do you know about Artin-Schreier theory?

[Aaron Liu]

oh that's great

[Aaron Liu]

Kevin Buzzard said:

Aaron Liu said:

that's great but really I want something that tells me when $X^2+X+\alpha$ has a root (in char2) based on the absolute trace of $\alpha$ which has a nice formula which I can prove inductively

Do you know about Artin-Schreier theory?

I think I know a little

[Violeta Hernández]

It does seem to be a common theme that all of these results on nimbers follow from Artin-Schreier theory

[Kevin Buzzard]

Crash course: if $K$ is a perfect field of char 2 (and hence an $\mathbb{F}_2$-vector space) then $P:K\to K$ defined by $P(x)=x^2+x$ is $\mathbb{F}_2$-linear and the quotient $K/P(K)-{0}$ canonically bijects with the set of iso classes of quadratic extensions of $K$, with the map sending $a\in K$ to the splitting field of $x^2+x+a$.

[Aaron Liu]

yes that makes sense

[Aaron Liu]

so you're saying there's at most one quadratic extension

[Aaron Liu]

or no that's not right

[Aaron Liu]

I definitely knew this before

[Kevin Buzzard]

For K finite there's exactly one because you can do dimension counting (the kernel of $P$ is $\{0,1\}$ so it's 1-dimensional, so the cokernel is 1-dimensional). If $K$ is algebraically closed then even though the kernel is 1-dimensional, the map is still surjective, because $\infty-1$ is still $\infty$ as it were.

[Kevin Buzzard]

For $K$ finite the image of $P$ is precisely the kernel of the trace map, and the trace map is surjective onto $\{0,1\}$.

[Aaron Liu]

after the first infinite nimber field up to the algebraic closure of 2 are all quadratically closed

[Aaron Liu]

so for now I only care about the finite case I think

[Aaron Liu]

Should I just PR the version for cyclic extensions to mathlib