# Zulip Chat Archive

## Stream: FLT-regular

### Topic: General notation

#### Riccardo Brasca (Oct 28 2021 at 14:17):

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`

and`cyclotomic_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 (Oct 28 2021 at 14:21):

- 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 (Oct 28 2021 at 14:24):

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 (Oct 28 2021 at 14:26):

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 (Oct 28 2021 at 14:26):

They are now `def`

.

#### Riccardo Brasca (Oct 28 2021 at 14:17):

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`

and`cyclotomic_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 (Oct 28 2021 at 14:21):

- 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 (Oct 28 2021 at 14:24):

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 (Oct 28 2021 at 14:26):

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 (Oct 28 2021 at 14:26):

They are now `def`

.

Last updated: Dec 20 2023 at 11:08 UTC