Other results

Results named in the rest of Tau Ceti's TauCeti.FieldTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCapelli's theorem#

Over any field K and for n ≠ 0, the binomial Xⁿ - a is irreducible if and only if a is not a p-th power for any prime p ∣ n and, when 4 ∣ n, a is not of the form -4b⁴. For odd n this is Mathlib's X_pow_sub_C_irreducible_iff_forall_prime_of_odd.

TauCeti.X_pow_sub_C_irreducible_iff_forall_prime.{u_1} {K : Type u_1} [Field K] {n : ℕ} (hn : n ≠ 0)
  {a : K} :
  Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔
    (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) ∧ (4 ∣ n → ∀ (b : K), -4 * b ^ 4 ≠ a)

Lean

Formalized in Tau Ceti as TauCeti.X_pow_sub_C_irreducible_iff_forall_prime.

Other forms

Capelli's theorem, sufficiency. Formalized in Tau Ceti as TauCeti.X_pow_sub_C_irreducible_of_forall_prime.

TauCeti.X_pow_sub_C_irreducible_of_forall_prime.{u_1} {K : Type u_1} [Field K] {n : ℕ} (hn : n ≠ 0)
  {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a)
  (ha' : 4 ∣ n → ∀ (b : K), -4 * b ^ 4 ≠ a) : Irreducible (Polynomial.X ^ n - Polynomial.C a)

Sources

• Tau Ceti documentation: TauCeti.X_pow_sub_C_irreducible_iff_forall_prime
• Source of TauCeti.X_pow_sub_C_irreducible_iff_forall_prime in TauCeti/FieldTheory/Kummer/Capelli.lean

LeanTauCeti.X_pow_sub_C_irreducible_iff_forall_prime · TauCeti.X_pow_sub_C_irreducible_of_forall_prime

Uses 1

Proof usesThe two-power case of Capelli's theorem

TheoremThe comparison theorem (TauCeti.fixedField_evenAutSubgroup)#

In a Galois splitting extension, and away from characteristic 2, the discriminant field of a separable polynomial is the field fixed by the automorphisms acting on the roots by an even permutation.

TauCeti.fixedField_evenAutSubgroup.{u, v} {F : Type u} [Field F] {E : Type v} [Field E]
  [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] [IsGalois F E]
  (hsep : f.Separable) (hchar : ringChar F ≠ 2) :
  IntermediateField.fixedField (TauCeti.evenAutSubgroup f E) = TauCeti.discrField f E

Lean

Formalized in Tau Ceti as TauCeti.fixedField_evenAutSubgroup.

Other forms

The comparison theorem, from the other side. Formalized in Tau Ceti as TauCeti.fixingSubgroup_discrField.

TauCeti.fixingSubgroup_discrField.{u, v} {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
  {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] (hsep : f.Separable)
  (hchar : ringChar F ≠ 2) : (TauCeti.discrField f E).fixingSubgroup = TauCeti.evenAutSubgroup f E

Sources

• Tau Ceti documentation: TauCeti.fixedField_evenAutSubgroup
• Source of TauCeti.fixedField_evenAutSubgroup in TauCeti/FieldTheory/GaloisGroups/Discriminant/Field.lean

LeanTauCeti.fixedField_evenAutSubgroup · TauCeti.fixingSubgroup_discrField

Uses 1

Proof usesPolynomial.Gal.sign

TheoremThe cup-norm theorem#

For units a and b of a field in which 2 is invertible, the cup product (a) ∪ (b) ∈ H²(G_K, 𝔽₂) of their Kummer classes vanishes if and only if the norm equation b = x² - a y² has a solution in K.

TauCeti.cup_kummerClass_eq_zero_iff.{u} {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) :
  (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1) (TauCeti.kummerClass a))
        (TauCeti.kummerClass b) =
      0 ↔
    ∃ x y, ↑b = x ^ 2 - ↑a * y ^ 2

Lean

Formalized in Tau Ceti as TauCeti.cup_kummerClass_eq_zero_iff.

Sources

• Tau Ceti documentation: TauCeti.cup_kummerClass_eq_zero_iff
• Source of TauCeti.cup_kummerClass_eq_zero_iff in TauCeti/FieldTheory/GaloisCohomology/MuTwo/CupNorm.lean

LeanTauCeti.cup_kummerClass_eq_zero_iff

Uses 5 · Used by 5

Proof usesArtin--Wedderburn over a separably closed field · The comparison isomorphism · The Skolem-Noether theorem · The splitting criterion for quaternion algebras · Wedderburn-Artin for central simple algebras

Used byQuadratic reciprocity is Hilbert reciprocity for two odd primes · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Hilbert's product formula · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field

TheoremDummit's formula for the resolvent of a quintic trinomial#

Over every commutative ring, the specialization of the quintic F₂₀ specification at X⁵ + aX + b is X⁶ + 8aX⁵ + 40a²X⁴ + 160a³X³ + 400a⁴X² + (512a⁵ - 3125b⁴)X + (256a⁶ - 9375ab⁴).

TauCeti.quinticF20Spec_specialize_X_pow_five_add_C_mul_X_add_C.{u_1} {R : Type u_1} [CommRing R]
  (a b : R) :
  TauCeti.quinticF20Spec.specialize R
      (Polynomial.X ^ 5 + Polynomial.C a * Polynomial.X + Polynomial.C b) =
    Polynomial.X ^ 6 + Polynomial.C (8 * a) * Polynomial.X ^ 5 +
              Polynomial.C (40 * a ^ 2) * Polynomial.X ^ 4 +
            Polynomial.C (160 * a ^ 3) * Polynomial.X ^ 3 +
          Polynomial.C (400 * a ^ 4) * Polynomial.X ^ 2 +
        Polynomial.C (512 * a ^ 5 - 3125 * b ^ 4) * Polynomial.X +
      Polynomial.C (256 * a ^ 6 - 9375 * a * b ^ 4)

Lean

Formalized in Tau Ceti as TauCeti.quinticF20Spec_specialize_X_pow_five_add_C_mul_X_add_C.

Other forms

Dummit's formula (2′) for the resolvent sextic of the integral quintic X⁵ + aX + b. Formalized in Tau Ceti as TauCeti.resolventSextic_X_pow_five_add_C_mul_X_add_C.

TauCeti.resolventSextic_X_pow_five_add_C_mul_X_add_C (a b : ℤ) :
  TauCeti.resolventSextic (Polynomial.X ^ 5 + Polynomial.C a * Polynomial.X + Polynomial.C b) =
    Polynomial.X ^ 6 + Polynomial.C (8 * a) * Polynomial.X ^ 5 +
              Polynomial.C (40 * a ^ 2) * Polynomial.X ^ 4 +
            Polynomial.C (160 * a ^ 3) * Polynomial.X ^ 3 +
          Polynomial.C (400 * a ^ 4) * Polynomial.X ^ 2 +
        Polynomial.C (512 * a ^ 5 - 3125 * b ^ 4) * Polynomial.X +
      Polynomial.C (256 * a ^ 6 - 9375 * a * b ^ 4)

Sources

• Tau Ceti documentation: TauCeti.quinticF20Spec_specialize_X_pow_five_add_C_mul_X_add_C
• Source of TauCeti.quinticF20Spec_specialize_X_pow_five_add_C_mul_X_add_C in TauCeti/FieldTheory/GaloisGroups/Resolvent/Quintic/Trinomial.lean

LeanTauCeti.quinticF20Spec_specialize_X_pow_five_add_C_mul_X_add_C · TauCeti.resolventSextic_X_pow_five_add_C_mul_X_add_C

Uses 2

Statement usesTauCeti.ResolventSpec

Proof usesVieta's formulas, in the form the symmetric descent uses

TheoremThe equivariant Kummer isomorphism on Kummer classes (TauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv)#

Under kummerH1FiniteRepresentationEquiv, the Kummer class of a power class x corresponds to the homomorphism μₙ → Lˣ ⧸ (Lˣ)ⁿ sending ξ to log ξ • x, with log : μₙ ≃ ℤ/n the identification kummerCoeffAddEquivZMod.

TauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv.{u, v} {K : Type u} [Field K] {L : Type v}
  [Field L] [Algebra K L] [Normal K L] (sigma : L →ₐ[K] SeparableClosure K) (n : ℕ) (hn : IsUnit ↑n)
  (hN : ∀ g ∈ sigma.fieldRange.fixingSubgroup, ∀ (xi : TauCeti.KummerCoeff K n), g • xi = xi)
  (x : Additive (TauCeti.powerClassQuotient Lˣ n)) (xi : TauCeti.KummerCoeff K n) :
  ((dualTensorHom (ZMod n) (TauCeti.KummerCoeff K n) (Additive (TauCeti.powerClassQuotient Lˣ n)))
        ((TauCeti.kummerH1FiniteRepresentationEquiv sigma n hn hN)
          ((TauCeti.fixingSubgroupKummerEquivOfTrivial sigma hn (TauCeti.kummerCoeffAddEquivZMod hn)
              ⋯ hN)
            x)))
      xi =
    (TauCeti.kummerCoeffAddEquivZMod hn) xi • x

Lean

Formalized in Tau Ceti as TauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv.

Sources

• Tau Ceti documentation: TauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv
• Source of TauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv in TauCeti/FieldTheory/GaloisCohomology/EquivariantKummer.lean

LeanTauCeti.dualTensorHom_kummerH1FiniteRepresentationEquiv

Uses 1

Statement usesThe Kummer isomorphism

TheoremEuler's criterion in a finite field#

If n ∣ #F - 1, then a nonzero a ∈ F is an n-th power exactly when a ^ ((#F - 1) / n) = 1.

TauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one.{u_1} {F : Type u_1} [Field F]
  [Finite F] {n : ℕ} (hn : n ∣ Nat.card F - 1) {a : F} (ha : a ≠ 0) :
  (∃ b, b ^ n = a) ↔ a ^ ((Nat.card F - 1) / n) = 1

Lean

Formalized in Tau Ceti as TauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one.

Sources

• Tau Ceti documentation: TauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one
• Source of TauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one in TauCeti/FieldTheory/Finite/EulerCriterion.lean

LeanTauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one

Used by 1

Used byEuler's criterion in a finite residue domain

TheoremSerre's formula for the Evens norm of a Kummer class (Serre, Théorème 1′ at n = 2)#

for an orthogonal basis y of the twisted trace form Tr_*⟨a⟩ : z ↦ Tr (a z²) whose values w_j = Tr (a y_j²) are units,

N^{Ev}((a)) = (w₁) ∪ (w₀) + (2) ∪ (d),

where d is the square of a generator x of L = K(x). Since (w₀) ∪ (w₁) is the second Stiefel–Whitney class of ⟨w₀, w₁⟩ ≅ Tr_*⟨a⟩, this is w₂(Tr_*⟨a⟩) = N^{Ev}((a)) + (2) ∪ (d).

TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup.{u} {K : Type u} [Field K] [Invertible 2]
  {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
  [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L}
  (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (a : Lˣ)
  (y : Fin 2 → L) (hy : (Algebra.trace K L) (↑a * y 0 * y 1) = 0) (w : Fin 2 → Kˣ)
  (hw : ∀ (i : Fin 2), ↑(w i) = (Algebra.trace K L) (↑a * y i ^ 2)) :
  TauCeti.galoisEvens K L σ hdeg (TauCeti.kummerClass a) =
    (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1)
          (TauCeti.kummerClass (w 1)))
        (TauCeti.kummerClass (w 0)) +
      (((TauCeti.trivialF2TopPairing (TauCeti.AbsoluteGaloisGroup K)).cup 1 1)
          (TauCeti.kummerClass (unitOfInvertible 2)))
        (TauCeti.kummerClass d)

Lean

Formalized in Tau Ceti as TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup.

Sources

• Tau Ceti documentation: TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup
• Source of TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup in TauCeti/FieldTheory/QuadraticForm/StiefelWhitney/Evens/Kummer/Value.lean

LeanTauCeti.galoisEvens2_kummerClass_eq_cup_add_cup

Uses 1 · Used by 3

Statement usesThe index-two degree-one Evens norm

Used byThe Evens norm of a Kummer class over a local field, as an element of H²(G_K, 𝔽₂) · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field

TheoremThe two-power case of Capelli's theorem#

Over any field K, if a is not a square in K and, when k ≥ 2, a is not of the form -4b⁴, then X^(2ᵏ) - a is irreducible. The second condition cannot be dropped: X⁴ + 4 is reducible over ℚ.

TauCeti.X_pow_two_pow_sub_C_irreducible.{u_1} {K : Type u_1} [Field K] (k : ℕ) {a : K}
  (ha : ∀ (b : K), b ^ 2 ≠ a) (ha' : 2 ≤ k → ∀ (b : K), -4 * b ^ 4 ≠ a) :
  Irreducible (Polynomial.X ^ 2 ^ k - Polynomial.C a)

Lean

Formalized in Tau Ceti as TauCeti.X_pow_two_pow_sub_C_irreducible.

Sources

• Tau Ceti documentation: TauCeti.X_pow_two_pow_sub_C_irreducible
• Source of TauCeti.X_pow_two_pow_sub_C_irreducible in TauCeti/FieldTheory/Kummer/Capelli.lean

LeanTauCeti.X_pow_two_pow_sub_C_irreducible

Used by 1

Used byCapelli's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.