# Zulip Chat Archive

## Stream: FLT-regular

### Topic: galois stuff

#### Eric Rodriguez (Jan 30 2022 at 21:21):

over the last two days i've proved that the galois group of a cyclotomic extension is `≤ (ℤ/nℤ)ˣ`

. Hopefully soon, I'm going to finish the proof for ℚ being a bijection too -- I'm following this proof, and realised I don't know how conjugate elements work in Mathlib

#### Eric Rodriguez (Jan 30 2022 at 21:22):

what is the "correct" Lean way to get that if we have `n-1`

conjugates then the galois group is full? (and therefore the embedding I have is actually a bijection)

#### Adam Topaz (Jan 30 2022 at 21:34):

https://leanprover-community.github.io/mathlib_docs/field_theory/polynomial_galois_group.html#polynomial.gal.card_of_separable is probably useful.

#### Eric Rodriguez (Feb 02 2022 at 00:21):

image.png the computation of the galois group of ℚ[ζₙ[ is done! it's on the `ne_zero`

branch, though, as the main branch is currently waiting for some PRs to make it usable again.

#### Eric Rodriguez (Feb 02 2022 at 00:22):

there's also weaker results showing that for general cyclotomic extensions, it's injective, so it basically covers things in some decent generality

#### Riccardo Brasca (Feb 02 2022 at 09:38):

This is great! Is this the mathlib way of stating the result? I was looking for something like `galois_group`

, but I don't see it.

#### Kevin Buzzard (Feb 02 2022 at 10:14):

Galois groups are just `L \equiv+*[K] L`

it seems to me

#### Eric Rodriguez (Feb 02 2022 at 10:23):

yeah, there's also `polynomial.gal`

but that's for polynomials. I just pushed those results, too, because they're pretty much defeq and follow from our `is_splitting_field`

instances.

#### Riccardo Brasca (Feb 02 2022 at 11:01):

Instead of working over `Q`

, can you generalize to any field `K`

such that `cyclotomic n K`

is irreducible? I guess the proof is the same.

#### Riccardo Brasca (Feb 02 2022 at 11:01):

(this can really happen for finite fields, so it is worth to have it)

#### Eric Rodriguez (Feb 02 2022 at 16:58):

done! also stops me from dealing with the diamond ^^

#### Riccardo Brasca (Feb 08 2022 at 17:21):

@Eric Rodriguez What was the solution for the `Q`

-alg diamond? I always forget how to get rid of it...

#### Alex J. Best (Feb 08 2022 at 17:23):

I think last time one of the solutions was to generalize away from Q :grinning:

Maybe `local attribute [-instance] algebra_rat`

is ok?

#### Riccardo Brasca (Feb 08 2022 at 17:24):

This was my first try, not enough

#### Riccardo Brasca (Feb 08 2022 at 17:24):

```
invalid type ascription, term has type
@is_cyclotomic_extension {n} ℤ
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
int.comm_ring
(@cyclotomic_ring.comm_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@cyclotomic_ring.algebra_base n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
but is expected to have type
@is_cyclotomic_extension {n} ℤ
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
int.comm_ring
(@cyclotomic_ring.comm_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@algebra_int
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@comm_ring.to_ring
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@cyclotomic_ring.comm_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)))
```

#### Alex J. Best (Feb 08 2022 at 17:26):

`local attribute [-instance] algebra_int`

too?

#### Eric Rodriguez (Feb 08 2022 at 17:26):

Convert + there's a lemma for Q algebra being a subsingleton that nerds to become an instance locally

#### Riccardo Brasca (Feb 08 2022 at 17:29):

```
convert cyclotomic_ring.is_cyclotomic_extension n ℤ ℚ,
exact subsingleton.elim (algebra_int _) _
```

works, thanks!

#### Riccardo Brasca (Feb 08 2022 at 17:33):

BTW it's very nice that working with general ring such that the cyclotomic polynomial is irreducible makes all these problem disappear.

At the end we will need to specialize to `Z`

, but at least we can postpone this problem as much as possible.

#### Eric Rodriguez (Jan 30 2022 at 21:21):

over the last two days i've proved that the galois group of a cyclotomic extension is `≤ (ℤ/nℤ)ˣ`

. Hopefully soon, I'm going to finish the proof for ℚ being a bijection too -- I'm following this proof, and realised I don't know how conjugate elements work in Mathlib

#### Eric Rodriguez (Jan 30 2022 at 21:22):

what is the "correct" Lean way to get that if we have `n-1`

conjugates then the galois group is full? (and therefore the embedding I have is actually a bijection)

#### Adam Topaz (Jan 30 2022 at 21:34):

https://leanprover-community.github.io/mathlib_docs/field_theory/polynomial_galois_group.html#polynomial.gal.card_of_separable is probably useful.

#### Eric Rodriguez (Feb 02 2022 at 00:21):

image.png the computation of the galois group of ℚ[ζₙ[ is done! it's on the `ne_zero`

branch, though, as the main branch is currently waiting for some PRs to make it usable again.

#### Eric Rodriguez (Feb 02 2022 at 00:22):

there's also weaker results showing that for general cyclotomic extensions, it's injective, so it basically covers things in some decent generality

#### Riccardo Brasca (Feb 02 2022 at 09:38):

This is great! Is this the mathlib way of stating the result? I was looking for something like `galois_group`

, but I don't see it.

#### Kevin Buzzard (Feb 02 2022 at 10:14):

Galois groups are just `L \equiv_a[K] L`

it seems to me (edit: fixed to make them algebra homs)

#### Eric Rodriguez (Feb 02 2022 at 10:23):

yeah, there's also `polynomial.gal`

but that's for polynomials. I just pushed those results, too, because they're pretty much defeq and follow from our `is_splitting_field`

instances.

#### Riccardo Brasca (Feb 02 2022 at 11:01):

Instead of working over `Q`

, can you generalize to any field `K`

such that `cyclotomic n K`

is irreducible? I guess the proof is the same.

#### Riccardo Brasca (Feb 02 2022 at 11:01):

(this can really happen for finite fields, so it is worth to have it)

#### Eric Rodriguez (Feb 02 2022 at 16:58):

done! also stops me from dealing with the diamond ^^

#### Riccardo Brasca (Feb 08 2022 at 17:21):

@Eric Rodriguez What was the solution for the `Q`

-alg diamond? I always forget how to get rid of it...

#### Alex J. Best (Feb 08 2022 at 17:23):

I think last time one of the solutions was to generalize away from Q :grinning:

Maybe `local attribute [-instance] algebra_rat`

is ok?

#### Riccardo Brasca (Feb 08 2022 at 17:24):

This was my first try, not enough

#### Riccardo Brasca (Feb 08 2022 at 17:24):

```
invalid type ascription, term has type
@is_cyclotomic_extension {n} ℤ
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
int.comm_ring
(@cyclotomic_ring.comm_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@cyclotomic_ring.algebra_base n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
but is expected to have type
@is_cyclotomic_extension {n} ℤ
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
int.comm_ring
(@cyclotomic_ring.comm_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@algebra_int
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@comm_ring.to_ring
(@cyclotomic_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)
(@cyclotomic_ring.comm_ring n ℤ ℚ int.comm_ring rat.field _
(@algebra_int ℚ
(@normed_ring.to_ring ℚ
(@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
rat.is_fraction_ring)))
```

#### Alex J. Best (Feb 08 2022 at 17:26):

`local attribute [-instance] algebra_int`

too?

#### Eric Rodriguez (Feb 08 2022 at 17:26):

Convert + there's a lemma for Q algebra being a subsingleton that nerds to become an instance locally

#### Riccardo Brasca (Feb 08 2022 at 17:29):

```
convert cyclotomic_ring.is_cyclotomic_extension n ℤ ℚ,
exact subsingleton.elim (algebra_int _) _
```

works, thanks!

#### Riccardo Brasca (Feb 08 2022 at 17:33):

BTW it's very nice that working with general ring such that the cyclotomic polynomial is irreducible makes all these problem disappear.

At the end we will need to specialize to `Z`

, but at least we can postpone this problem as much as possible.

Last updated: Dec 20 2023 at 11:08 UTC