type transfer

Stream: new members

[Chengyan Hu]

Hi! I'm really confused that when I wrote NeZero ((l^i):L), lean always transfer it into NeZero (l:L)^i, but when I trying to apply this, lean respect them as different things:

import Mathlib
open Ideal Padic Nat
open scoped algebraMap

theorem pow_eq_ex_eq {L : Type*} [Field L] (ζ : L) (n : ℕ) [NeZero n] (hζ : IsPrimitiveRoot ζ n)
    {a b : ℤ} : ζ ^ a = ζ ^ b ↔ (a:ZMod n) = (b:ZMod n) := by
  constructor
  · rintro h
    have hζ0 : ζ ≠ 0 := hζ.ne_zero (NeZero.ne n)
    have h1:ζ^((b-a)) =1 := by
      rw [zpow_sub₀ hζ0,div_eq_one_iff_eq (zpow_ne_zero _ hζ0)]
      simp only[h]
    have h3: (n:Int) ∣ (b - a) := by
      rwa [hζ.zpow_eq_one_iff_dvd] at h1
    exact (ZMod.intCast_eq_intCast_iff_dvd_sub a b n).mpr h3
  · rintro h
    have hζ0 : ζ ≠ 0 := hζ.ne_zero (NeZero.ne n)
    rw[←div_eq_one_iff_eq (zpow_ne_zero _ hζ0),←zpow_sub₀ hζ0,hζ.zpow_eq_one_iff_dvd]
    exact (ZMod.intCast_eq_intCast_iff_dvd_sub b a n).mp (id (Eq.symm h))

theorem pow_eq_ex_eq' {L : Type*} [Field L] (ζ : L) (n : ℕ) [NeZero n] (hζ : IsPrimitiveRoot ζ n)
    {a b : ℕ} : ζ ^ a = ζ ^ b ↔ (a:ZMod n) = (b:ZMod n) := by
    convert pow_eq_ex_eq ζ n hζ (a := a) (b := b) <;> simp

lemma isDomain_of_faithfulSMul (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : IsDomain B :=
  Function.Injective.isDomain (algebraMap B L) <| by
  rwa [← faithfulSMul_iff_algebraMap_injective B L]

lemma faithfulSMul_of_isIntegralClosure (A B L : Type*) [CommRing A] [CommSemiring B] [CommRing L]
    [Algebra A L] [Algebra B L] [IsIntegralClosure B A L] : FaithfulSMul B L where
  eq_of_smul_eq_smul {b₁ b₂} h := by
    apply IsIntegralClosure.algebraMap_injective B A L
    simp [Algebra.algebraMap_eq_smul_one, h 1]








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)





-- the value of the cyclotomic character at Frob_I is #A/PA where P = I ∩ A
include L K
omit [NumberField K] in
lemma algclosure_HasEnoughRootOfUnity (n:ℕ) [NeZero (n:L)]:
 HasEnoughRootsOfUnity L n := by
  have : IsAlgClosed L := IsAlgClosure.isAlgClosed K
  exact IsSepClosed.hasEnoughRootsOfUnity L n

include hI hF hlp A B L K
theorem cyclo_thing :
    ((cyclotomicCharacter L l (MulSemiringAction.toRingEquiv G L F)) : ℤ_[l]) =
      Nat.card (A ⧸ I.under A) := by
      set q:= ↑(Nat.card (A ⧸ under A I))
      set g:= (MulSemiringAction.toRingEquiv G L F)


      --∀i:ℕ , ↑(l^i) ∉ I
      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

      --B in an integral domain, should be tautology
      have DomainB: IsDomain B:= by
        have := faithfulSMul_of_isIntegralClosure A B L
        exact isDomain_of_faithfulSMul B L

      --reduce modular l^i
      rw[← PadicInt.ext_of_toZModPow]
      intro i
      simp
      have H1 := H i

      --have enough roots in B
      have N1:NeZero (l:B):=by
        have: (l:B)≠0 := by
          by_contra Y
          apply hlp
          rw[Y]
          exact Submodule.zero_mem I
        exact { out := this }
      have N1': ∀ (i:ℕ),NeZero ((l^i):B) := by
        exact fun i => NeZero.pow
      have N2: NeZero (l:L):= by
        sorry
      have N2': ∀ (i:ℕ),NeZero ((l^i):L) := by
        exact fun i => NeZero.pow

      have ineed : ∀ (i : ℕ), HasEnoughRootsOfUnity L (l ^ i):=by
        intro i
        specialize N2' i
        apply algclosure_HasEnoughRootOfUnity (l^i)

[Chengyan Hu]

By the way, I do believe the sorry there should be an easy sorry, but I stuck on prove it.

[Aaron Liu]

You can write NeZero ((l ^ i : ℕ) : L) or you can write NeZero (↑(l ^ i) : L)

[Kenny Lau]

@Chengyan Hu this is due to a fundamental misunderstanding of how type ascription works. Lean elaborates from left to right.

For example, suppose we have x y : Z, and we write (x + y : R). Here is what Lean thinks:

1. I need to interpret the expression x + y with the goal of landing in R.
2. The first thing I see is the +. (Remember, x + y just means Add.add x y.)
3. I see + and I need to land in R, so the two subexpressions must both be assigned type R. (In particular, in this step Lean has already decided that the + is to be interpreted as addition on R)
4. I see x which was given type Z, so I need to coerce it to R.
5. I see y which was given type Z, so I need to coerce it to R.

Result: Real.add (Int.toReal x) (Int.toReal y) (fake notation)

You can verify this yourself here:

import Mathlib.Data.Real.Basic

set_option pp.notation false
set_option pp.coercions false
set_option pp.explicit true
variable (x y : ℤ)
#check (x + y : ℝ)
/-
@HAdd.hAdd Real Real Real
  (@instHAdd Real Real.instAdd)
  (@Int.cast Real Real.instIntCast x)
  (@Int.cast Real Real.instIntCast y) : Real
-/

In summary:

• When you type ((l^i) : L), it is interpreted as L.pow (Nat.toL l) i, i.e. (↑l) ^ i.
• Due to a fundamental misunderstanding, you thought you typed Nat.toL (Nat.pow l i), but that's just not how Lean works.
• This doesn't mean that Lean treats those two expressions as the same, it just means that you thought you were typing one thing, but Lean interpreted it to mean another thing.
• If you want to emphasize that you want to coerce to L only at the very last step, then indeed Aaron's suggestion is ((l ^ i : ℕ) : L). Try to reread my paragraph above to see why this makes sense.

[Chengyan Hu]

Thank you so much for the really in detailed explain!