Trace of ring-homomorphic image

Stream: Is there code for X?

[Michał Staromiejski]

In the formalization of my results I have proved the following result:

trace_iterateFrobenius_ne_zero (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] (p : ℕ)
  [ExpChar F p] [ExpChar E p] [Algebra.IsSeparable F E] [FiniteDimensional F E] (s : ℕ) (a : E)
  (h : (Algebra.trace F E) a ≠ 0) : (Algebra.trace F E) (a ^ p ^ s) ≠ 0 := sorry

Note that the iterated Frobenius homomorphism E →+* E given by a ↦ a ^ p ^ s is not necessarily the identity on F, so it's not in general true that Algebra.trace F E a = Algebra.trace F E (a ^ p ^ s). Nevertheless, the above result is true with my proof using more intermediate results about minimal polynomials of mapped elements:

import Mathlib.RingTheory.Trace.Basic
import Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E]
variable (p : ℕ) [ExpChar F p] [ExpChar E p]

lemma interateFrobenius_algebraMap_comm (s : ℕ) :
    (algebraMap F E).comp (iterateFrobenius F p s) =
    (iterateFrobenius E p s).comp (algebraMap F E) :=
  RingHom.ext (fun x ↦
    ((algebraMap F E).comp_apply (iterateFrobenius F p s) x).trans <|
    (congrArg (algebraMap F E) (iterateFrobenius_def p s x)).trans <|
    ((algebraMap F E).map_pow x (p ^ s)).trans <|
    (iterateFrobenius_def p s (algebraMap F E x)).symm.trans <|
    ((iterateFrobenius E p s).comp_apply (algebraMap F E) x).symm)

open scoped IntermediateField

variable [Algebra.IsSeparable F E]

/-- For a separable extension `F ⊆ E` of characteristic `p > 0`,
    the minimal polynomial of `a ^ p ^ s` is the minimal polynomial of `a` mapped via `(⬝ ^ p ^ s)`. -/
lemma minpoly_map_frobenius (s : ℕ) (a : E) :
    minpoly F (iterateFrobenius E p s a) = (minpoly F a).map (iterateFrobenius F p s) := by
  let μ := minpoly F a
  let μ₁ := minpoly F (a ^ p ^ s)
  let μ₂ := μ.map (iterateFrobenius F p s)
  /- goal: `μ₁ = μ₂` -/
  have hμ₂aeval : 0 = μ₂.aeval (a ^ p ^ s) :=
    iterateFrobenius_def p s a ▸
    (iterateFrobenius E p s).map_zero ▸
    minpoly.aeval F a ▸
    μ.map_aeval_eq_aeval_map (interateFrobenius_algebraMap_comm F p s) a
  have hai : IsIntegral F a := (Algebra.IsSeparable.isSeparable F a).isIntegral
  have hapi : IsIntegral F (a ^ p ^ s) := hai.pow (p ^ s)
  /- both are monic -/
  have hμ₁monic : μ₁.Monic := minpoly.monic hapi
  have hμ₂monic : μ₂.Monic := (minpoly.monic hai).map (iterateFrobenius F p s)
  /- both have same degree -/
  have hdeg : μ₂.natDegree = μ₁.natDegree := by
    calc μ₂.natDegree
      _ = μ.natDegree := μ.natDegree_map_eq_of_injective (iterateFrobenius F p s).injective
      _ = Module.finrank F F⟮a⟯ := (IntermediateField.adjoin.finrank hai).symm
      _ = Module.finrank F F⟮a ^ p ^ s⟯ := by
        rw [IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' F E a p s]
      _ = μ₁.natDegree := IntermediateField.adjoin.finrank hapi
  /- one divides the other -/
  have hdvd : μ₁ ∣ μ₂ := minpoly.dvd F (a ^ p ^ s) hμ₂aeval.symm
  symm
  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le hμ₁monic hμ₂monic hdvd (le_of_eq hdeg)

variable [FiniteDimensional F E]

/-- If the trace of `a` is non-zero then the trace of `a ^ p ^ s` is non-zero
    in a separable extension of characteristic `p`. -/
lemma trace_iterateFrobenius_ne_zero (s : ℕ) (a : E) (h : Algebra.trace F E a ≠ 0) : Algebra.trace F E (a ^ p ^ s) ≠ 0 :=
  let ⟨hn, hc⟩ := mul_ne_zero_iff.mp (trace_eq_finrank_mul_minpoly_nextCoeff F a ▸ h)
  trace_eq_finrank_mul_minpoly_nextCoeff F (a ^ p ^ s) ▸
    IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' F E a p s ▸
    mul_ne_zero_iff.mpr ⟨hn, neg_ne_zero.mpr <|
      iterateFrobenius_def (R := E) p .. ▸
      minpoly_map_frobenius F p s a ▸
      Polynomial.nextCoeff_map (iterateFrobenius F p s).injective (minpoly F a) ▸
      iterateFrobenius_def (R := F) p .. ▸ pow_ne_zero (p ^ s) (neg_ne_zero.mp hc)⟩

I'm wondering if the following more general fact can be proven:

trace_map_ne_zero (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E]
  [Algebra.IsSeparable F E] [FiniteDimensional F E] (f : E →+* E) (a : E)
  (h : Algebra.trace F E a ≠ 0) : Algebra.trace F E (f a) ≠ 0 := sorry

possibly using similar generalization for minimal polynomials of images via ring homomorphisms?
I have a feeling that separability and field setting are important here but maybe generalization with injective ring homomorphism would also be possible...

Maybe there is something close in Mathlib already?

[Michał Staromiejski]

Here is my approach to generalize minpoly_map_frobenius from my proof :

import Mathlib.FieldTheory.Minpoly.Field
import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

variable (F₁ F₂ K₁ K₂ : Type*)
variable [Field F₁] [Field F₂] [Field K₁] [Field K₂]
variable [Algebra F₁ K₁] [Algebra F₂ K₂]

open scoped IntermediateField

theorem minpoly_map_ringHom (f : F₁ →+* F₂) (φ : K₁ →+* K₂)
    (h : (algebraMap F₂ K₂).comp f = φ.comp (algebraMap F₁ K₁))
    (a : K₁) (hai : IsIntegral F₁ a) :
    minpoly F₂ (φ a) = (minpoly F₁ a).map f := by
  let μ := minpoly F₁ a
  let μ₁ := minpoly F₂ (φ a)
  let μ₂ := μ.map f
  /- goal: `μ₁ = μ₂` -/
  have hμ₂aeval : 0 = μ₂.aeval (φ a) :=
    φ.map_zero ▸
    minpoly.aeval F₁ a ▸
    μ.map_aeval_eq_aeval_map h a
  have hφai : IsIntegral F₂ (φ a) := hai.map_of_comp_eq f φ h
  /- both are monic -/
  have hμ₁monic : μ₁.Monic := minpoly.monic hφai
  have hμ₂monic : μ₂.Monic := (minpoly.monic hai).map f
  /- both have same degree -/
  have hdeg : μ₂.natDegree ≤ μ₁.natDegree := by
    calc μ₂.natDegree
      _ = μ.natDegree := μ.natDegree_map_eq_of_injective f.injective
      _ = Module.finrank F₁ F₁⟮a⟯ := (IntermediateField.adjoin.finrank hai).symm
      _ ≤ Module.finrank F₂ F₂⟮φ a⟯ := by sorry
      _ = μ₁.natDegree := IntermediateField.adjoin.finrank hφai
  /- one divides the other -/
  have hdvd : μ₁ ∣ μ₂ := minpoly.dvd F₂ (φ a) hμ₂aeval.symm
  symm
  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le hμ₁monic hμ₂monic hdvd hdeg

There is only one sorry left, but I'm not sure if it's true in general.

But maybe there is an easier way to approach the main goal (not necessarily using minimal polynomials)?

[Jz Pan]

Michał Staromiejski said:

Note that the iterated Frobenius homomorphism E →+* E given by a ↦ a ^ p ^ s is not necessarily the identity on F, so it's not in general true that Algebra.trace F E a = Algebra.trace F E (a ^ p ^ s).

But they have relationships, no?

[Michał Staromiejski]

Jz Pan said:

Michał Staromiejski said:

Note that the iterated Frobenius homomorphism E →+* E given by a ↦ a ^ p ^ s is not necessarily the identity on F, so it's not in general true that Algebra.trace F E a = Algebra.trace F E (a ^ p ^ s).

But they have relationships, no?

What do you mean by relationships here?

[Junyan Xu]

Algebra.rank_le_of_injective_injective looks relevant for the sorry ...

[Jz Pan]

Michał Staromiejski said:

Jz Pan said:

Michał Staromiejski said:

Note that the iterated Frobenius homomorphism E →+* E given by a ↦ a ^ p ^ s is not necessarily the identity on F, so it's not in general true that Algebra.trace F E a = Algebra.trace F E (a ^ p ^ s).

But they have relationships, no?

What do you mean by relationships here?

I mean although they are not equal, but maybe they satisfy certain equation.

[Michał Staromiejski]

Junyan Xu said:

Algebra.rank_le_of_injective_injective looks relevant for the sorry ...

The problem here is that the "bottom" homomorphism goes in different direction.

The more I think about it, the more I believe that (iterated) Frobenius is kind of special here.

Of course I could always add extra assumption Module.finrank F₁ F₁⟮a⟯ ≤ Module.finrank F₂ F₂⟮φ a⟯ (and maybe state the result for F₁ = F₂ = F only), then for the (iterated) Frobenius we have docs#IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable'.

Another question is: how much minpoly_map_ringHom stated above would be useful for mathlib users?

[Michał Staromiejski]

Ok, the minpoly_map_ringHom as stated above is obv not true in such a generality: take any non-trivial field extension K / F, K₁ = K₂ = K, F₁ = F, F₂ = K, φ = RingHom.id K, f = algebraMap F K. Then it is not in general true that for a : K, minpoly K a = minpoly F a.

But maybe it still is true when F₁ = F₂ :thinking: :

import Mathlib.FieldTheory.Minpoly.Field
import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

variable (F K₁ K₂ : Type*)
variable [Field F] [Field K₁] [Field K₂]
variable [Algebra F K₁] [Algebra F K₂]

open scoped IntermediateField

theorem minpoly_map_ringHom (f : F →+* F) (φ : K₁ →+* K₂)
    (h : (algebraMap F K₂).comp f = φ.comp (algebraMap F K₁))
    (a : K₁) (hsep : IsSeparable F a) :
    minpoly F (φ a) = (minpoly F a).map f := by
  have hai : IsIntegral F a := IsSeparable.isIntegral hsep
  let μ := minpoly F a
  let μ₁ := minpoly F (φ a)
  let μ₂ := μ.map f
  /- goal: `μ₁ = μ₂` -/
  have hμ₂aeval : 0 = μ₂.aeval (φ a) :=
    φ.map_zero ▸
    minpoly.aeval F a ▸
    μ.map_aeval_eq_aeval_map h a
  have hφai : IsIntegral F (φ a) := hai.map_of_comp_eq f φ h
  /- both are monic -/
  have hμ₁monic : μ₁.Monic := minpoly.monic hφai
  have hμ₂monic : μ₂.Monic := (minpoly.monic hai).map f
  /- both have same degree -/
  have hdeg : μ₂.natDegree ≤ μ₁.natDegree := by
    calc μ₂.natDegree
      _ = μ.natDegree := μ.natDegree_map_eq_of_injective f.injective
      _ = Module.finrank F F⟮a⟯ := (IntermediateField.adjoin.finrank hai).symm
      _ ≤ Module.finrank F F⟮φ a⟯ := by sorry
      _ = μ₁.natDegree := IntermediateField.adjoin.finrank hφai
  /- one divides the other -/
  have hdvd : μ₁ ∣ μ₂ := minpoly.dvd F (φ a) hμ₂aeval.symm
  symm
  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le hμ₁monic hμ₂monic hdvd hdeg

My gut feeling is that the sorry would be actually an equality rather than ≤.

[Jz Pan]

I think minpoly F (φ a) = (minpoly F a).map f the sorry (i.e. minpoly F (φ a) = minpoly F a) should be true without IsSeparable F a. The key point is that φ : K₁ →+* K₂ is injective hence it induces an isomorphism of φ(K₁) and K₂ (docs#RingHom.rangeRestrictField and docs#RingHom.rangeRestrictField_bijective, seems that there misses a result similar to docs#AlgEquiv.ofInjectiveField). Then just use the definition of minpoly should deduce the desired result.

[Jz Pan]

docs#minpoly.algHom_eq and docs#minpoly.algebraMap_eq but seems that not what you want...

[Jz Pan]

Or maybe you want to prove μ ∣ μ₁ by showing that μ₁ also annihilates a?

[Michał Staromiejski]

Thanks @Jz Pan. The problem is that φ does not induce identity on F, not even bijective ring homomorphism, so even if it can be considered a semilinear map, I think I can't prove equidimensionality this way.

As for showing that μ₁ also annihilates a, it is also not true in general (not even for the Frobenius map).

Just to be clear: I'm thinking how to generalize some basic technical lemmas from my work to maybe include them in Mathlib. If there is nothing like this and the community would like to have them, I can include what I do have (as in the first post here). If not, I'll keep them in my repo, but I think someone maybe could use them even if they are quite specialized.

[Michał Staromiejski]

(The ultimate goal of mine is actually to prove that for a separable E / F and a purely inseparable K / E with an exponent s, the composition Algebra.trace F E ∘ IsPurelyInseparable.iterateFrobenius E K is non-vanishing.)

[Jz Pan]

That's strange. Seems that back to your original version, f : F₁ →+* F₂ needs to be purely inseparable?

[Jz Pan]

For your original setup F₁ F₂ K₁ K₂, is it equivalent to view F₂ and K₁ as IntermediateField F₁ K₂? Maybe we can work out on such special versions first.

[Jz Pan]

Then you have a : K₂ which satisfies a ∈ K₁ and is finite separable over F₁. Calculating the (finite) separable degree of F₂(a) / F₁ should leads to the desired result.

[Jz Pan]

I don't think this result is true in the general setting. It's true if F₁(a) and F₂ are linearly disjoint over F₁ (the separable and purely inseparable setup is a special case of this).

[Michał Staromiejski]

Jz Pan said:

That's strange. Seems that back to your original version, f : F₁ →+* F₂ needs to be purely inseparable?

What do you mean by "f : F₁ →+* F₂ needs to be purely inseparable"?

Jz Pan said:

For your original setup F₁ F₂ K₁ K₂, is it equivalent to view F₂ and K₁ as IntermediateField F₁ K₂? Maybe we can work out on such special versions first.

It won't help I guess; you can always consider field homomorhisms as inclusions so it is the case here because the maps commute.

Jz Pan said:

I don't think this result is true in the general setting. It's true if F₁(a) and F₂ are linearly disjoint over F₁ (the separable and purely inseparable setup is a special case of this).

I think I demonstrated that it will not be true already :wink: That's why I was thinking about making F₁ and F₂ equal.

[Jz Pan]

Michał Staromiejski said:

What do you mean by "f : F₁ →+* F₂ needs to be purely inseparable"?

I mean when you view F₂ and K₁ as IntermediateField F₁ K₂, then F₂ / F₁ is purely inseparable. (If you only have a ring homomorphism, then you can use docs#IsPRadical instead.) I think in this case I can prove your original result.

[Michał Staromiejski]

My original result with the Frobenius map is done fully in separable setting as this is what I need in my proofs. It uses IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' but everything is separable, otherwise it does not work.

[Jz Pan]

Oh, I mean this:

import Mathlib.FieldTheory.Minpoly.Field
import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
import Mathlib.FieldTheory.IsPerfectClosure

variable (F₁ F₂ K₁ K₂ : Type*)
variable [Field F₁] [Field F₂] [Field K₁] [Field K₂] (p : ℕ) [ExpChar F₁ p]
variable [Algebra F₁ K₁] [Algebra F₂ K₂]

open scoped IntermediateField

theorem minpoly_map_ringHom (f : F₁ →+* F₂) [IsPRadical f p] (φ : K₁ →+* K₂)
    (h : (algebraMap F₂ K₂).comp f = φ.comp (algebraMap F₁ K₁))
    (a : K₁) (hai : IsSeparable F₁ a) :
    minpoly F₂ (φ a) = (minpoly F₁ a).map f := by ...

[Michał Staromiejski]

I decided to add the result for minimal polynomial of the Frobenius map image in the PR #23599. The trace result is not that interesting anyway I think.

[Junyan Xu]

In the general setting of (f : F₁ →+* F₂) (φ : K₁ →+* K₂) [Algebra F₂ K₂], we can regard K₂ as an F₁-algebra via the composition of f with algebraMap F₂ K₂, and if we assume [Algebra F₁ K₁] (h : (algebraMap F₂ K₂).comp f = φ.comp (algebraMap F₁ K₁)), then φ is an F₁-AlgHom from K₁ to K₂, so the F₁-minpolys are equal by minpoly.algHom_eq. The problem reduces to comparing the F₁-minpoly and F₂-minpoly of an element of K₂. Of course, if f is surjective (and therefore bijective), then the minpolys are equal. Otherwise, F₂ is a proper extension of F₁ and the minpolys may differ. This can happen even when F₁ = F₂ (f : F(X) →+* F(X) can send X to X^2), so we get counterexamples to this (even assuming the element is separable).

[Michał Staromiejski]

Good point @Junyan Xu, thanks! For some reason the (iterated) Frobenius maps, even if not surjective, make the statement true, but indeed in general it is not true.