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