galois stuff

Stream: FLT-regular

[Eric Rodriguez]

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]

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]

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

[Eric Rodriguez]

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]

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]

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]

Galois groups are just L \equiv+*[K] L it seems to me

[Eric Rodriguez]

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]

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]

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

[Eric Rodriguez]

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

[Riccardo Brasca]

@Eric Rodriguez What was the solution for the Q-alg diamond? I always forget how to get rid of it...

[Alex J. Best]

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]

This was my first try, not enough

[Riccardo Brasca]

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]

local attribute [-instance] algebra_int too?

[Eric Rodriguez]

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

[Riccardo Brasca]

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

works, thanks!

[Riccardo Brasca]

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]

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]

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]

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

[Eric Rodriguez]

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]

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]

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]

Galois groups are just L \equiv_a[K] L it seems to me (edit: fixed to make them algebra homs)

[Eric Rodriguez]

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]

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]

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

[Eric Rodriguez]

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

[Riccardo Brasca]

@Eric Rodriguez What was the solution for the Q-alg diamond? I always forget how to get rid of it...

[Alex J. Best]

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]

This was my first try, not enough

[Riccardo Brasca]

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]

local attribute [-instance] algebra_int too?

[Eric Rodriguez]

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

[Riccardo Brasca]

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

works, thanks!

[Riccardo Brasca]

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.