Algebraic closure of field and a type mismatch

Stream: new members

[Chengyan Hu]

Hi! I got stuck on a part of my proof, I wanna prove all p^i th primitive roots exist in L, where L is the algebraic closure of K (The sorry in line 51).

import Mathlib
open Ideal Padic Nat

variable
    -- let K be a number field with ring of integers A
    {A K : Type*}
    [CommRing A] [IsDedekindDomain A]
    [Field K] [NumberField K] [Algebra A K]
    [IsFractionRing A K]
    [IsIntegralClosure A ℤ K]
    -- let L be an algebraic closure of K
    {L : Type*} [Field L] [Algebra K L]
    [Algebra A L] [IsScalarTower A K L]
    [IsAlgClosure K L]
    -- and let B be the integral closure of A in L
    {B : Type*} [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]
    -- Let G be the Galois group of L/K
    variable {G : Type*} [Group G]
    [MulSemiringAction G L]
    [SMulCommClass G K L]
    [Algebra.IsInvariant K L G]
    [MulSemiringAction G B]
    [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [IsScalarTower G B L]
    -- Let F be an element of G
    (F : G)
    -- Let I be a maximal ideal of B
    (I : Ideal B) (hI : I.IsMaximal)
    -- assume F is a Frobenius element at I
    (hF : IsArithFrobAt A F I)
    -- Then for a prime ell not in I...
    (l : ℕ) [Fact (Nat.Prime l)](hlp : ↑l ∉ I)
    {ζ:L}

-- the value of the cyclotomic character at Frob_I is #A/PA where P = I ∩ A
include hI hF hlp in
theorem cyclo_thing :
    ((cyclotomicCharacter L l (MulSemiringAction.toRingEquiv G L F)) : ℤ_[l]) =
      Nat.card (A ⧸ I.under A) := by
      have primeI: I.IsPrime := hI.isPrime
      have H: ∀i:ℕ , ↑(l^i) ∉ I := by
        by_contra hi
        simp at hi
        rw[← mem_radical_iff,IsPrime.radical primeI] at hi
        exact hlp hi
      rw[← PadicInt.ext_of_toZModPow]
      intro i
      have ext_root : ∀ (i : ℕ), ∃ ζ : L,IsPrimitiveRoot ζ (l ^ i):= sorry
      obtain ⟨ζ,hζ⟩ := ext_root i
      specialize H i
      refine AlgHom.IsArithFrobAt.apply_of_pow_eq_one hζ.pow_eq_one H
      sorry

#check AlgHom.IsArithFrobAt.apply_of_pow_eq_one

I tried to use L.IsAlgClosed directly but it doesn't work.

[Chengyan Hu]

Also, I believe AlgHom.IsArithFrobAt.apply_of_pow_eq_one requires two hypothesis, $\zeta$ is a m-th root of unit, and m should not be in the ideal. It seems like hζ.pow_eq_one should give the first hypothesis well, but actually it doesn't.

[Ruben Van de Velde]

No, the first argument to apply_of_pow_eq_one is an IsArithFrobAt, the second argument is hζ.pow_eq_one

[Ruben Van de Velde]

Also the lemma doesn't seem to match the goal

[Chengyan Hu]

My idea is after rewrite ← PadicInt.ext_of_toZModPow, the remaining goal is equivalent to apply_of_pow_eq_one in case $\zeta$ is a $l^i$ th root. But I do stuck on how to finish this in lean.

[Edison Xie]

apply_of_pow_eq_one would not directly get you to the goal so you shouldn't try to refine it

[Chengyan Hu]

Sadly refine doesn't work as well, I don't quit understand what parameter should be input into apply_of_pow_eq_one

[Ruben Van de Velde]

I don't see why you think that lemma applies here

[Chengyan Hu]

I believe you are right if you are talking about the form of goal in lean. Maybe something like cyclotomicCharacter.spec should be apply here to match the form of the lemma? I'm not quit sure.

[Edison Xie]

if you think the lemma is helpful but it currently can't close the goal, you should probably have it

[Edison Xie]

also I believe your ζ should probly be an element of B

[Chengyan Hu]

I believe $\zeta$ should be in L?

[Chengyan Hu]

As cyclotomicCharacter L p g is the unique j : ℤₚ such that g(ζ) = ζ ^ (j mod pⁱ) for all pⁱ'th roots of unity ζ, where L is a domain containing all pⁱ-th primitive roots with p a prime , and g is a ring automorphism of L.
In math, we just have to say $g(\zeta)=\zeta^{Nat.card (R ⧸ Q.under R)}$ for all p^i th root of unit. Which is exactly proved in AlgHom.IsArithFrobAt.apply_of_pow_eq_one. Quit straighforward in math.
Hence I believe we only have to apply something to change the goal in to a good form matching that lemma. And I stuck here.