Cyclotomic rings and fields and DTT hell

Stream: mathlib4

[Michael Stoll]

I am trying to produce the obvioud ℤ-algebra isomorphism between CyclotomicRing 3 ℤ ℚand the ring of integers of CyclotomicField 3 ℚ. There is docs#IsPrimitiveRoot.adjoinEquivRingOfIntegers', which gives

↥(Algebra.adjoin ℤ {μ}) ≃ₐ[ℤ] ↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ))

(here μ is a primitive cube root of unity in CyclotomicField 3 ℚ). [Aside: this needs Fact (Nat.Prime (3 : ℕ+)) to be available as an instance, which is a minor annoyance.]
So now I'm left with constructing

CyclotomicRing 3 ℤ ℚ ≃ₐ[ℤ] ↥(Algebra.adjoin ℤ {μ})

There is docs#CyclotomicRing.eq_adjoin_primitive_root, which says that

CyclotomicRing 3 ℤ ℚ = ↥(Algebra.adjoin ℤ {μ})

so this should be easy, one would think. However:

import Mathlib

instance PNat.three_prime : Fact (Nat.Prime (3 : ℕ+)) := ⟨Nat.prime_three⟩

variable {μ : CyclotomicField 3 ℚ} (hμ : IsPrimitiveRoot μ (3 : ℕ+))

noncomputable def ι' /- : CyclotomicRing 3 ℤ ℚ ≃ₐ[ℤ] ↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ)) -/ :=
  CyclotomicRing.eq_adjoin_primitive_root 3 ℤ ℚ hμ ▸ hμ.adjoinEquivRingOfIntegers'

#check ι' hμ -- ι' hμ : ↥(Algebra.adjoin ℤ {μ}) ≃ₐ[ℤ] ↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ))

noncomputable def e : CyclotomicRing 3 ℤ ℚ ≃ₐ[ℤ] ↥(Algebra.adjoin ℤ {μ}) := by
  convert AlgEquiv.refl (R := ℤ) (A₁ := ↥(Algebra.adjoin ℤ {μ})) using 1 with h h'
  · exact CyclotomicRing.eq_adjoin_primitive_root 3 ℤ ℚ hμ
  · sorry -- HEq CommSemiring.toSemiring (Subalgebra.toSemiring (Algebra.adjoin ℤ {μ})); more detail:
    -- Heq (@CommSemiring.toSemiring (CyclotomicRing 3 ℤ ℚ) CommRing.toCommSemiring)
    --   (@Subalgebra.toSemiring ℤ (CyclotomicField 3 ℚ) Int.instCommSemiringInt DivisionSemiring.toSemiring
    --   (CyclotomicField.algebra' 3 ℚ) (Algebra.adjoin ℤ {μ}))
  . sorry -- HEq (CyclotomicRing.algebraBase 3 ℤ ℚ) (Subalgebra.algebra (Algebra.adjoin ℤ {μ}))
    -- Heq (@CyclotomicRing.algebraBase 3 ℤ ℚ Int.instCommRingInt Rat.field (algebraInt ℚ)); more detail:
    --   (@Subalgebra.algebra ℤ (CyclotomicField 3 ℚ) Int.instCommSemiringInt DivisionSemiring.toSemiring
    --   (CyclotomicField.algebra' 3 ℚ) (Algebra.adjoin ℤ {μ}))

noncomputable def ι'' : CyclotomicRing 3 ℤ ℚ ≃ₐ[ℤ] ↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ)) :=
  CyclotomicRing.eq_adjoin_primitive_root 3 ℤ ℚ hμ ▸ hμ.adjoinEquivRingOfIntegers'
-- type mismatch
--   IsPrimitiveRoot.adjoinEquivRingOfIntegers' hμ
-- has type
--   @AlgEquiv ℤ (↥(Algebra.adjoin ℤ {μ})) (↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ))) Int.instCommSemiringInt
--     (Subalgebra.toSemiring (Algebra.adjoin ℤ {μ}))
--     (Subalgebra.toSemiring (NumberField.ringOfIntegers (CyclotomicField 3 ℚ)))
--     (Subalgebra.algebra (Algebra.adjoin ℤ {μ}))
--     (Subalgebra.algebra (NumberField.ringOfIntegers (CyclotomicField 3 ℚ))) : Type
-- but is expected to have type
--   @AlgEquiv ℤ (↥(Algebra.adjoin ℤ {μ})) (↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ))) Int.instCommSemiringInt
--     CommSemiring.toSemiring (Subalgebra.toSemiring (NumberField.ringOfIntegers (CyclotomicField 3 ℚ)))
--     (CyclotomicRing.algebraBase 3 ℤ ℚ) (Subalgebra.algebra (NumberField.ringOfIntegers (CyclotomicField 3 ℚ))) : Type

-- (similar error when using `(CyclotomicRing.eq_adjoin_primitive_root 3 ℤ ℚ hμ).symm ▸ ...`)

So I'm stuck, and help would be much appreciated.
I assume the problem is that Lean cannot figure out that the algebra structures on both sides are compatible...
@Riccardo Brasca

[Eric Wieser]

docs#CyclotomicRing.eq_adjoin_primitive_root looks like a very weird lemma to me; equalities of types are almost never what you want

[Michael Stoll]

That's what I thought, too.

[Eric Wieser]

Really the statement should be

example : (Algebra.adjoin A {b : CyclotomicField n K | b ^ ↑n = 1}) = adjoin A ({μ} : Set (CyclotomicField n K))

(which is an equality of subalgebras/sets)

[Michael Stoll]

Then one could probably go via docs#Subalgebra.equivOfEq.

[Michael Stoll]

import Mathlib

instance PNat.three_prime : Fact (Nat.Prime (3 : ℕ+)) := ⟨Nat.prime_three⟩

variable {μ : CyclotomicField 3 ℚ} (hμ : IsPrimitiveRoot μ (3 : ℕ+))

lemma help : (Algebra.adjoin ℤ {b : CyclotomicField 3 ℚ | b ^ 3 = 1}) =
    Algebra.adjoin ℤ ({μ} : Set (CyclotomicField 3 ℚ)) := by
  refine Algebra.adjoin_eq_of_le (Algebra.adjoin ℤ {μ}) (fun x hx ↦ ?_) <|
    Algebra.adjoin_mono <| Set.singleton_subset_iff.mpr hμ.pow_eq_one
  obtain ⟨m, _, hm⟩ := hμ.eq_pow_of_pow_eq_one hx (by norm_num)
  exact hm ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) m

noncomputable def ι' : CyclotomicRing 3 ℤ ℚ ≃ₐ[ℤ] ↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ)) :=
  (Subalgebra.equivOfEq _ _ <| help hμ).trans hμ.adjoinEquivRingOfIntegers'

#check ι' hμ -- CyclotomicRing 3 ℤ ℚ ≃ₐ[ℤ] ↥(NumberField.ringOfIntegers (CyclotomicField 3 ℚ))

[Eric Rodriguez]

I think I wrote this a while ago and over time I think we've deprecated use of cyclotomicring, it's really not worth it and as you say an absolute mess. We should probably do some tidying in this area, cc @Riccardo Brasca

[Michael Stoll]

So what is the Mathlib-canonical way of speaking about ℤ[ζ] for a primitive nth root of unity ζ?

[Michael Stoll]

CyclotomicRing seemed to be the natural thing to use...

[Michael Stoll]

(Filled in the proof of help above.)

[Riccardo Brasca]

Michael Stoll said:

So what is the Mathlib-canonical way of speaking about ℤ[ζ] for a primitive nth root of unity ζ?

I agree with Eric and I would avoid CyclotomicRing. You can use Algebra.adjoin ℤ {ζ}. We have the instance that says that it is the ring of integer of the cyclotomic field.

[Riccardo Brasca]

I suggest to have ζ of type K, it is a little more flexible.

[Michael Stoll]

Are there plans to add the fact that ℤ[ζ] is the ring of integers of ℚ[ζ] for arbitrary n? I think right now it is only in Mathlib when n is a prime power.

[Riccardo Brasca]

I don't think anyone is working on it, but it is something we of course want at some point.

[Riccardo Brasca]

I don't think anyone is working on it, but it is something we of course want at some point.

[Michael Stoll]

Now I am trying to prove that Algebra.adjoin ℤ {μ} ≃ₐ[ℤ] Algebra.adjoin ℤ {μ'}, where μ : CyclotomicField 3 ℚ and μ' : ℂ are primitive cube roots of unity, but I'm finding it hard. E.g., docs#AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly only works over fields. (I did manage to show that minpoly ℤ μ = minpoly ℤ μ', so if this were more general [it should be true over rings when the minimal polynomial is monic], I would be done.)

[Andrew Yang]

I think the better way to go is to construct an embedding $\mathbb{Z}[\zeta_3]\hookrightarrow \mathbb{C}$ sending μ to μ' and use docs#AlgHom.map_adjoin_singleton

[Michael Stoll]

How to I get an AlgEquiv to the image of an injective AlgHom?

[Andrew Yang]

@loogle AlgEquiv, Subalgebra.map, Function.Injective

[loogle]

:shrug: nothing found

[Michael Stoll]

I tried something similar, with the same result.

[Andrew Yang]

We should add an AlgHom version of docs#RingHom.restrict

[Andrew Yang]

And then use docs#AlgEquiv.ofBijective to get something like docs#Submodule.equivMapOfInjective

[Michael Stoll]

BTW, what I did now is this:

import Mathlib

namespace AlgEquiv

open Polynomial AdjoinRoot

noncomputable
def adjoinSingletonEquivAdjoinRootMinpoly' {F R : Type*} [CommRing F] [IsDomain F] [IsIntegrallyClosed F]
    [CommRing R] [IsDomain R] [Algebra F R] [NoZeroSMulDivisors F R] {x : R} (hx : IsIntegral F x) :
    Algebra.adjoin F ({x} : Set R) ≃ₐ[F] AdjoinRoot (minpoly F x) := by
  refine AlgEquiv.symm <| AlgEquiv.ofBijective (Minpoly.toAdjoin F x) ?_
  refine ⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩
  obtain ⟨P, rfl⟩ := mk_surjective P₁
  refine AdjoinRoot.mk_eq_zero.mpr (minpoly.isIntegrallyClosed_dvd hx ?_)
  rwa [Minpoly.toAdjoin_apply', liftHom_mk, ← Subalgebra.coe_eq_zero, aeval_subalgebra_coe] at hP₁

end AlgEquiv

instance PNat.three_prime : Fact (Nat.Prime (3 : ℕ+)) := ⟨Nat.prime_three⟩

noncomputable def μ' : CyclotomicField 3 ℚ := IsCyclotomicExtension.zeta 3 ℚ _

noncomputable abbrev R := Algebra.adjoin ℤ {μ'}

lemma μ_prim : IsPrimitiveRoot μ' (3 : ℕ+) := IsCyclotomicExtension.zeta_spec 3 ℚ _

noncomputable def μℂ' : ℂ := IsCyclotomicExtension.zeta 3 ℂ _

lemma μℂ'_prim : IsPrimitiveRoot μℂ' (3 : ℕ+) := IsCyclotomicExtension.zeta_spec 3 ℂ _

lemma minpoly_eq : minpoly ℤ μ' = minpoly ℤ μℂ' := by
  suffices : minpoly ℚ μ' = minpoly ℚ μℂ'
  · rw [minpoly.isIntegrallyClosed_eq_field_fractions' _ (μ_prim.isIntegral (by norm_num)),
      minpoly.isIntegrallyClosed_eq_field_fractions' _ (μℂ'_prim.isIntegral (by norm_num))] at this
    exact (Polynomial.map_injective _ <| RingHom.injective_int (algebraMap ℤ ℚ)) this
  have h : Irreducible (Polynomial.cyclotomic ↑3 ℚ) :=
    Polynomial.cyclotomic.irreducible_rat (by norm_num)
  rw [← IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible μ_prim h,
    ← IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible μℂ'_prim h]

noncomputable abbrev R' := Algebra.adjoin ℤ {μℂ'}

noncomputable def equiv_R1 : R ≃ₐ[ℤ] AdjoinRoot (minpoly ℤ μ') :=
  AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly' (μ_prim.isIntegral (by norm_num))

noncomputable def equiv_R2 : R' ≃ₐ[ℤ] AdjoinRoot (minpoly ℤ μ') :=
  minpoly_eq ▸ AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly' (μℂ'_prim.isIntegral (by norm_num))

noncomputable def R_equiv_R' := equiv_R1.trans equiv_R2.symm

What I find a bit strange is the occurrence of AlgebraCat in

#check R_equiv_R' -- R_equiv_R' : ↑(AlgebraCat.of ℤ ↥R) ≃ₐ[ℤ] ↑(AlgebraCat.of ℤ ↥R')

Why is this not just ↥R ≃ₐ[ℤ] ↥R'? (It seems I can force it to be this by adding a type ascription. Still, I'd like to know.)

[Eric Wieser]

mwe:

import Mathlib.Algebra.Category.AlgebraCat.Basic

noncomputable abbrev R : Subalgebra ℤ ℤ := sorry

#check R ≃ₐ[ℤ] R -- bad coercion introduced `AlgebraCat.of`

[Andrew Yang]

docs#instCoeOutSubalgebraToCommSemiringToSemiringAlgebraCat

[Eric Wieser]

That's the one, that instance is a disaster

[Eric Wieser]

The caller should be forced to write of _ S to turn a subalgebra into a category

[Riccardo Brasca]

@Michael Stoll all of this is for FLT 3, right? Can you explain a little bit what you need?

I may be completely wrong, but I think all the computations should take place in K = CyclotomicField 3 ℚ or 𝓞 K.

[Michael Stoll]

@Riccardo Brasca At this point, this is for a student's bachelor's thesis, which is about implementing Jacobi sums (following Ireland-Rosen), and the particular goal here is to show that $J(\chi, \chi) = a + b \omega$ when $\chi$ is a cubic character, with integers $a$ and $b$ and a primitive cube root of unity $\omega$. So working with $\mathbb{Z}[\omega]$ is quite natural...

[Riccardo Brasca]

I see. What about working with a general K with IsCyclotomicExtension {p ^ k} ℚ K (of course replacing p^k with n would be very nice) and any primitive root of unity? Your computation can live in 𝓞 K or in Algebra.adjoin ℤ {ζ} depending on what is more convenient, and we know that they're isomorphic, docs#IsPrimitiveRoot.adjoinEquivRingOfIntegers

[Michael Stoll]

I've just started to try that :smile:

[Michael Stoll]

RIght now, I'm stuck at proving

K: Type u_1
inst✝¹: Field K
inst✝: CharZero K
cyc: IsCyclotomicExtension {3} ℚ K
μ: K
μ_prim: IsPrimitiveRoot μ ↑3
⊢ ↑((IsIntegralClosure.lift (↥(Algebra.adjoin ℤ {μ})) K (_ : Algebra.IsIntegral ℤ ↥(NumberField.ringOfIntegers K)))
      (IsPrimitiveRoot.toInteger μ_prim)) =
  μ

Any hints on how to peel off the stack of maps on the left?

[Michael Stoll]

BTW, when working with concrete numbers, it is really a pain in the neck that the cyclotomic machinery uses PNats. E.g., you have to write μ_prim : IsPrimitiveRoot μ (3 : ℕ+) and provide the instance Fact (Nat.Prime (3 : ℕ+)) to make μ_prim.integralPowerBasis' work. I'd propose to change to using Nats, perhaps with a [NeZero n] assumption (or allow zero and just ignore it). @Riccardo Brasca

[Riccardo Brasca]

Michael Stoll said:

RIght now, I'm stuck at proving

K: Type u_1
inst✝¹: Field K
inst✝: CharZero K
cyc: IsCyclotomicExtension {3} ℚ K
μ: K
μ_prim: IsPrimitiveRoot μ ↑3
⊢ ↑((IsIntegralClosure.lift (↥(Algebra.adjoin ℤ {μ})) K (_ : Algebra.IsIntegral ℤ ↥(NumberField.ringOfIntegers K)))
      (IsPrimitiveRoot.toInteger μ_prim)) =
  μ

Any hints on how to peel off the stack of maps on the left?

Can you write down the full result you need? I can give a try.

[Riccardo Brasca]

Michael Stoll said:

BTW, when working with concrete numbers, it is really a pain in the neck that the cyclotomic machinery uses PNats. E.g., you have to write μ_prim : IsPrimitiveRoot μ (3 : ℕ+) and provide the instance Fact (Nat.Prime (3 : ℕ+)) to make μ_prim.integralPowerBasis' work. I'd propose to change to using Nats, perhaps with a [NeZero n] assumption (or allow zero and just ignore it). Riccardo Brasca

Yes, this is something we are aware since the beginning. We chose to work with PNat to simplify things, but we end up with a lot of coercions and we more or less got used to them, but we almost never work with explicit numbers. This was not so bad, so I never found the energy to do the refactor, but I am not against it in principle. Maybe the other FLT-regular people have a different opinion. @Andrew Yang @Eric Rodriguez @Alex J. Best @Chris Birkbeck

[Michael Stoll]

The current state of my proof attempt is this (not yet very polished):

import Mathlib

namespace Polynomial

-- A useful lemma for going from polynomials to linear combinations.
lemma aeval_of_natDegree_lt_2 {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    {f : R[X]} (hf : f.natDegree < 2) (a : A) :
    (aeval (R := R) a) f = f.coeff 0 • 1 + f.coeff 1 • a := by
  have hf' : f = C (f.coeff 0) + C (f.coeff 1) * X
  · ext n -- prove by comparing coefficients
    match n with
    | 0 => simp
    | 1 => simp [-eq_intCast] -- otherwise the coefficient gets changed before other lemmas apply
    | n + 2 => -- show that all higher coefficients are zero on both sides
        simpa only [coeff_add, coeff_C_succ, coeff_mul_X, add_zero]
          using natDegree_le_iff_coeff_eq_zero.mp (Nat.lt_succ.mp hf) _ <| Nat.one_lt_succ_succ n
  rw [hf']
  simp [Algebra.algebraMap_eq_smul_one]

end Polynomial

-- The following instance is needed in some places later.
instance PNat.three_prime : Fact (Nat.Prime (3 : ℕ+)) := ⟨Nat.prime_three⟩

lemma have_repr {K} [Field K] [CharZero K] [cyc : IsCyclotomicExtension {3} ℚ K] {μ : K}
    (μ_prim : IsPrimitiveRoot μ (3 : ℕ+)) {x : K} (hx : x ∈ Algebra.adjoin ℤ {μ}) :
    ∃ a b : ℤ, x = a + b * μ := by
  let B := μ_prim.integralPowerBasis'
  have H₂ : B.dim = 2 := μ_prim.power_basis_int'_dim
  obtain ⟨f, hf₁, hf₂⟩ := B.exists_eq_aeval <| μ_prim.adjoinEquivRingOfIntegers' ⟨x, hx⟩
  refine ⟨f.coeff 0, f.coeff 1, ?_⟩
  apply_fun μ_prim.adjoinEquivRingOfIntegers'.symm at hf₂
  rw [AlgEquiv.symm_apply_apply] at hf₂
  apply_fun Subtype.val at hf₂
  simp only [μ_prim.integralPowerBasis'_gen, μ_prim.adjoinEquivRingOfIntegers'_symm_apply] at hf₂
  rw [hf₂, Polynomial.aeval_of_natDegree_lt_2 (H₂ ▸ hf₁), -- `H₂ ▸ hf₁ : f.natDegree f < 2`
    map_add, map_zsmul, map_zsmul, map_one, zsmul_eq_mul, zsmul_eq_mul, mul_one]
  simp only [Subsemiring.coe_add, Subalgebra.coe_toSubsemiring, SubringClass.coe_intCast,
    Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, add_right_inj, mul_eq_mul_left_iff,
    Int.cast_eq_zero]
  left
  -- this is the tactic state mentioned above
  sorry

[Riccardo Brasca]

Let me have a look.

[Michael Stoll]

Essentially, the task is to transfer the statement that the image of x in the ring of integers of K has the correct form back to x and μ.

[Michael Stoll]

I was just trying to apply the inverse map (and the coercion from the subtype) on both sides and then simplify...

[Riccardo Brasca]

have you tried using docs#Submodule.span_range_natDegree_eq_adjoin ?

[Riccardo Brasca]

It seems relevant

[Michael Stoll]

No; I'm just at the beginning of exploring that part of the library.

[Andrew Yang]

I more or less agree. Using PNats had minor inconveniences that I got used to and it is probably worth trying if using Nat can make things easier.

[Michael Stoll]

???

import Mathlib

#check Submodule.span_range_natDegree_eq_adjoin
-- unknown constant 'Submodule.span_range_natDegree_eq_adjoin'

docs#Submodule.span_range_natDegree_eq_adjoin

[Riccardo Brasca]

Maybe it changed name and you have an old version?

[Riccardo Brasca]

It works for me

[Andrew Yang]

That lemma is relatively new.

[Michael Stoll]

OK, let me bump Mathlib...

[Riccardo Brasca]

I think I can finish the proof, give me 10 minutes

[Riccardo Brasca]

Voilà

import Mathlib

namespace Polynomial

-- A useful lemma for going from polynomials to linear combinations.
lemma aeval_of_natDegree_lt_2 {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    {f : R[X]} (hf : f.natDegree < 2) (a : A) :
    (aeval (R := R) a) f = f.coeff 0 • 1 + f.coeff 1 • a := by
  have hf' : f = C (f.coeff 0) + C (f.coeff 1) * X
  · ext n -- prove by comparing coefficients
    match n with
    | 0 => simp
    | 1 => simp [-eq_intCast] -- otherwise the coefficient gets changed before other lemmas apply
    | n + 2 => -- show that all higher coefficients are zero on both sides
        simpa only [coeff_add, coeff_C_succ, coeff_mul_X, add_zero]
          using natDegree_le_iff_coeff_eq_zero.mp (Nat.lt_succ.mp hf) _ <| Nat.one_lt_succ_succ n
  rw [hf']
  simp [Algebra.algebraMap_eq_smul_one]

end Polynomial

lemma have_repr {K} [Field K] [CharZero K] [cyc : IsCyclotomicExtension {3} ℚ K] {μ : K}
    (μ_prim : IsPrimitiveRoot μ (3 : ℕ+)) {x : K} (hx : x ∈ Algebra.adjoin ℤ {μ}) :
    ∃ a b : ℤ, x = a + b * μ := by
  classical
  have h₁ : Nat.totient 3 = 2 := rfl
  have h₂ : Finset.range 2 = {0, 1} := rfl
  have := minpoly.aeval ℤ μ
  rw [←Polynomial.cyclotomic_eq_minpoly μ_prim (by norm_num)] at this
  change x ∈ Subalgebra.toSubmodule (Algebra.adjoin ℤ {μ}) at hx
  rw [←Submodule.span_range_natDegree_eq_adjoin (Polynomial.cyclotomic.monic 3 ℤ) this,
    Polynomial.natDegree_cyclotomic, h₁, h₂] at hx
  simp only [Finset.image_insert, pow_zero, Finset.image_singleton, pow_one, Finset.coe_insert,
    Finset.coe_singleton] at hx
  obtain ⟨a, b, hx⟩ := Submodule.mem_span_pair.1 hx
  refine ⟨a, b, ?_⟩
  rw [←hx]
  simp

[Riccardo Brasca]

Of course it has nothing to do with cyclotomic extensions

[Riccardo Brasca]

And all the job is done by docs#Submodule.span_range_natDegree_eq_adjoin