General notation

Stream: FLT-regular

[Riccardo Brasca]

Everything should compile now, using the new general definition is_cyclotomic_extension. Here is a quick summary of the notations, I think it's a good idea to try to be consistent through the whole project.

• If you want to say that a given extension is cyclotomic, use

variables (S : set ℕ+) (A B : Type*) [comm_ring A] [comm_ring B]
class is_cyclotomic_extension : Prop :=
(ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : B, aeval r (cyclotomic a A) = 0)
(adjoint_roots : ∀ x, x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 })

It means that B is a S-th cyclotomic extension of A. We will surely need a good API for this.

• If you want to consider "the" n-th cyclotomic extension of a field, use

variables (n : ℕ+) (K : Type*) [field K]
def cyclotomic_field  := (cyclotomic n K).splitting_field

It is a field and has is_cyclotomic_extension {n} K (cyclotomic_extension n K).

• If you want to consider "the" n-th cyclotomic extension of a domain, things a little trickier. You should use

variables (n : ℕ+) (A K : Type*) [comm_ring A] [field K] [algebra A K] [is_fraction_ring A K]
def cyclotomic_ring  := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }

So you have this K lying around, that mathematically is irrelevant. Note that cyclotomic_field n K andcyclotomic_ring n A K do not have an A-algebra instance (maybe they soon will, but there are diamonds to be solved). If you need them, just use

local attribute [instance] cyclotomic_field.algebra_base --algebra A (cyclotomic_field n K)
local attribute [instance] cyclotomic_ring.algebra_base -- algebra A (cyclotomic_ring n A K)

• We should try to work with is_cyclotomic_extension as much as possible, avoiding the explicit constructions.
• In practice A = ℤ and K = ℚ is enough for us, but very often the proof is the same, I suggest we try to be as general as possible if it's easy.
• If A = ℤ, then the instances algebra ℤ (cyclotomic_field n ℚ) and algebra ℤ (cyclotomic_ring n ℤ ℚ) exist by the general machinery, so in this case you should not use local attribute [instance] (doing so will trigger some diamond-related problems).

[Riccardo Brasca]

• Results about a general cyclotomic extension are in the is_cyclotomic_extension namespace (even if they are only for fields or whatever).
• Results about the explicit construction are in the cyclotomic_field or cyclotomic_ring namespace.

[Alex J. Best]

Thanks for sorting all this out Riccardo, at https://github.com/leanprover-community/flt-regular/runs/4035774913?check_suite_focus=true there are some linter errors still, most are harmless and will be sorted out in time, but I'm curious whether

-- number_theory/cyclotomic/basic.lean
#check @cyclotomic_field.algebra_base /- is a lemma/theorem, should be a def -/
#check @cyclotomic_ring.algebra_base /- is a lemma/theorem, should be a def -/

is intended or not at this point?

[Eric Wieser]

Making your data-carrying instances lemmas is certainly one way to guarantee diamonds!

lemma foo : ℕ := 1
lemma bar : ℕ := 1
example : foo = bar := rfl -- fails!

[Riccardo Brasca]

They are now def.

[Riccardo Brasca]

Everything should compile now, using the new general definition is_cyclotomic_extension. Here is a quick summary of the notations, I think it's a good idea to try to be consistent through the whole project.

• If you want to say that a given extension is cyclotomic, use

variables (S : set ℕ+) (A B : Type*) [comm_ring A] [comm_ring B]
class is_cyclotomic_extension : Prop :=
(ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : B, aeval r (cyclotomic a A) = 0)
(adjoint_roots : ∀ x, x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 })

It means that B is a S-th cyclotomic extension of A. We will surely need a good API for this.

• If you want to consider "the" n-th cyclotomic extension of a field, use

variables (n : ℕ+) (K : Type*) [field K]
def cyclotomic_field  := (cyclotomic n K).splitting_field

It is a field and has is_cyclotomic_extension {n} K (cyclotomic_extension n K).

• If you want to consider "the" n-th cyclotomic extension of a domain, things are a little trickier. You should use

variables (n : ℕ+) (A K : Type*) [comm_ring A] [field K] [algebra A K] [is_fraction_ring A K]
def cyclotomic_ring  := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }

So you have this K lying around, that mathematically is irrelevant. Note that cyclotomic_field n K andcyclotomic_ring n A K do not have an A-algebra instance (maybe they soon will, but there are diamonds to be solved). If you need them, just use

local attribute [instance] cyclotomic_field.algebra_base --algebra A (cyclotomic_field n K)
local attribute [instance] cyclotomic_ring.algebra_base -- algebra A (cyclotomic_ring n A K)

• We should try to work with is_cyclotomic_extension as much as possible, avoiding the explicit constructions.
• In practice A = ℤ and K = ℚ is enough for us, but very often the proof is the same, I suggest we try to be as general as possible if it's easy.
• If A = ℤ, then the instances algebra ℤ (cyclotomic_field n ℚ) and algebra ℤ (cyclotomic_ring n ℤ ℚ) exist by the general machinery, so in this case you should not use local attribute [instance] (doing so will trigger some diamond-related problems).

[Riccardo Brasca]

• Results about a general cyclotomic extension are in the is_cyclotomic_extension namespace (even if they are only for fields or whatever).
• Results about the explicit construction are in the cyclotomic_field or cyclotomic_ring namespace.

[Alex J. Best]

Thanks for sorting all this out Riccardo, at https://github.com/leanprover-community/flt-regular/runs/4035774913?check_suite_focus=true there are some linter errors still, most are harmless and will be sorted out in time, but I'm curious whether

-- number_theory/cyclotomic/basic.lean
#check @cyclotomic_field.algebra_base /- is a lemma/theorem, should be a def -/
#check @cyclotomic_ring.algebra_base /- is a lemma/theorem, should be a def -/

is intended or not at this point?

[Eric Wieser]

Making your data-carrying instances lemmas is certainly one way to guarantee diamonds!

lemma foo : ℕ := 1
lemma bar : ℕ := 1
example : foo = bar := rfl -- fails!

[Riccardo Brasca]

They are now def.