Define cyclotomic fields

[icecream17]

The way FLT3 is proved in lean is by proving an even more general FLT3 where cyclotomic fields are used. This structure seems interesting and connected to some useful library building.

The two relevant subdefinitions needed are:

• splitting field of a polynomial (smallest field extension such that a polynomial 'splits': factors into linear terms) (the Lean implementation seems similar to this somewhat recursive generation from wikipedia: https://en.wikipedia.org/wiki/Splitting_field#The_construction)
• cyclotomic polynomial (??? but probably uses df-minply, looking at wikipedia)

Note that IsCyclotomicExtension is a separate property which includes:

• Algebra.adjoin (the minimal subalgebra that includes a set S, Lean implements it as ((scalars lifted to vectors) union s) closure under addition and multiplication) (edit: this exists, df-asp (aspval2))

(Existing definitions)

• Algebra --> df-assa
• algebraMap --> df-ascl
• IsPrimitiveRoot --> df-primroots
• (field extension) --> df-fldext

[tirix]

There is ~ df-sfl for splitting fields, but this is only a definition - it was not used to prove any theorem yet - and it might need some tweaking.

Yes, for cyclotomic polynomials, we should be able define them using ~ df-minply!

Maybe:

|- cyctmPly = ( n e. NN |-> ( ( CCfld minPoly QQ ) ` ( exp ` ( ( _i x. ( 2 x. _pi ) ) / n ) ) ) )

[metakunt]

Ah, glad I see someone is also "stealing" content from lean.

@icecream17 I will also need splitting fields, as I want to eventually down the line prove the existence of finite fields. Would it make sense if we have a discussion and design a blueprint, so that we don't duplicate efforts?

I think @digama0 definition is good, if you want to consider the case for finite fields, or any construction that is Toset-compatible. I would define (as in lean) the splitting field as the "smallest" subalgebra L, such that f splits over L and then prove the theorems needing splitting fields axiomatically. After that one would have to show that df-sfl is indeed a splitting field. Remember that in lean nearly all constructions are noncomputable and heavily rely on the axiom of choice.

I am not there yet as I likely need to prove three more things.

• The Z/nZ reduction that eliminates the introspective relation.
• Units of an integral domain are a cyclic group.
• A cyclic group of order n has a primitive root for any divisor d | n.

After that I'll start developing the blueprint for finite fields.

[digama0]

I thought we had something about cyclotomic polynomials, but I forget... EDIT: see df-cytp

[icecream17]

I will also need splitting fields, as I want to eventually down the line prove the existence of finite fields. Would it make sense if we have a discussion and design a blueprint, so that we don't duplicate efforts?

yes it would

Though, I currently have very little knowledge on the subject, other than ~ df-sfl1's explanation of how it should work without the axiom of choice, and that df-sfl uses df-sfl1 uses df-plfl

Although, in ~ df-plfl,

... sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩

this part:

(℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))

doesn't look right: deg1 takes one argument and I would expect that multiple possible values satisfy <.

[tirix]

deg1 takes one argument

It should work if replacing ( s deg1 q ) with ( ( deg1 ` s ) ` q ).

The same remark can be made of the definition just below, df-sfl1 (it should be possible to shorten that other definition by using minPly).

(Edit: I think r should be replaced by s here, as r is the original field, while s represents the polynomials over that field - and we can only take degrees of the polynomials)

[tirix]

I would expect that multiple possible values satisfy <

Actually there would be only one polynomial satisfying the inequality: this is a similar construct as ~ df-q1p. Maybe a more elegant way here would be to use the polynomial division remainder rem1p (which was only introduced in set.mm a few months after this definition is dated).

This is what I've used in the "degree of a field extension" proof algextdeg, see for example the function H of algextdeglem7.

Recalling of the formula:

|- polyFld = ( r e. _V , p e. _V |-> [_ ( Poly1 ` r ) / s ]_
      [_ ( ( RSpan ` s ) ` { p } ) / i ]_
      [_ ( z e. ( Base ` r ) |->
           [ ( z ( .s ` s ) ( 1r ` s ) ) ] ( s ~QG i ) ) / f ]_
      <. [_ ( s /s ( s ~QG i ) ) / t ]_ ( ( t toNrmGrp ( iota_ n e.
        ( AbsVal ` t ) ( n o. f ) = ( norm ` r ) ) ) sSet <. ( le ` ndx ) ,
          [_ ( z e. ( Base ` t ) |->
            ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) / g ]_
          ( `' g o. ( ( le ` s ) o. g ) ) >. ) , f >. )

So we could replace ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) with ( z e. ( Base ` t ) |-> ( z ( rem1p ` s ) p ) ).

[icecream17]

Edit: nevermind, I didn't read the substitution for f correctly

I think I found another type error in `polyFld` ``` ( iota_ n e. ( AbsVal ` t ) ( n o. f ) = ( norm ` r ) )

where
z e. ( Base ` r )

[ ( z ( .s s ) ( 1r s ) ) ] ( s ~QG i ) ) / f ]_

[_ ( s /s ( s ~QG i ) ) / t ]_

In `( n o. f )`, `f` is trying to lift something in `r` to an equivalence class, which is an element of the quotient structure `t`. From there ``n e. ( AbsVal ` t )`` is the norm (distance from zero):

( n ( f x ) ) = ( ( norm r ) x )

But `f` is not a function, rather it's an equivalence class itself.
</details>

[icecream17]

I'm now working on the basic properties of df-plfl

First is the idea behind

So we could replace ( z e. ( Base ` t ) |-> ( iota_ q e. z ( r deg1 q ) < ( r deg1 p ) ) ) with ( z e. ( Base ` t ) |-> ( z ( rem1p ` s ) p ) )

This didn't work since z is an ideal, and rem1p expects polynomials instead, but a variant of it should work: |-> ( iota_ q e. z ( q rem p ) = q )

(Although, only for unitic polynomials. I'm not sure if df-plfl should have a more specific domain, but the phrase "if one exists and the extension is unique" at the end of df-plfl's comment seems to imply the norm doesn't have to be valid)

I made some theorems expanding on this idea, but I have a feeling those theorems are mostly irrelevant. I'm not sure what properties will be useful.

theorems

  ${
    $d ph x y $.  $d ps y $.  $d ch x $.  $d X x $.  $d B x $.
    cbvrexima.s $e |- ( x = X -> ( ps <-> ch ) ) $.
    cbvrexima.x $e |- ( ph -> ( x e. A <-> E. y e. B x = X ) ) $.
    cbvrexima.a $e |- ( ph -> X e. V ) $.
    $( Rewrite existential quantification using a function's image.  The second
       hypothesis corresponds to ~ elrnmpt , ~ elimampt , et al.  (Contributed
       by SN, 19-Jun-2025.) $)
    cbvrexima $p |- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) ) $=
      ( wrex cv wceq wex wa wcel rexbii bitr3i anbi1d pm5.32i exbidv df-rex syl
      r19.41v bitr4di 19.41v rexcom4 3bitr4g elisset biantrurd rexbidv bitr4d )
      ABDFMZDNZIOZDPZCQZEGMZCEGMAUPFRZBQZDPUQCQZEGMZDPZUOUTAVBVDDAVBUQEGMZBQZVD
      AVAVFBKUAVDUQBQZEGMVGVHVCEGUQBCJUBSUQBEGUFTUGUCBDFUDUTVCDPZEGMVEVIUSEGUQC
      DUHSVCEDGUITUJACUSEGAURCAIHRURLDIHUKUEULUMUN $.
  $}

  ${
    rspssbasd.k $e |- K = ( RSpan ` R ) $.
    rspssbasd.b $e |- B = ( Base ` R ) $.
    rspssbasd.r $e |- ( ph -> R e. Ring ) $.
    rspssbasd.g $e |- ( ph -> G C_ B ) $.
    $( The span of a set of ring elements is a set of ring elements.
       (Contributed by SN, 19-Jun-2025.) $)
    rspssbasd $p |- ( ph -> ( K ` G ) C_ B ) $=
      ( cfv clidl wcel wss crg eqid rspcl syl2anc lidlss syl ) ADEJZCKJZLZTBMAC
      NLDBMUBHIBCUADEFGUAOZPQBTUACGUCRS $.
  $}

  ${
    $d B k $.  $d R k $.  $d .x. k $.  $d U k $.  $d N k $.  $d X k $.
    elrspsn.b $e |- B = ( Base ` R ) $.
    elrspsn.t $e |- .x. = ( .r ` R ) $.
    elrspsn.i $e |- I = ( ( RSpan ` R ) ` { X } ) $.
    elrspsn.r $e |- ( ph -> R e. Ring ) $.
    elrspsn.x $e |- ( ph -> X e. B ) $.
    $( Membership in the span of a singleton.  ( ~ lspsnel , ~ elspansn analog)
       (Contributed by SN, 19-Jun-2025.) $)
    elrspsn $p |- ( ph -> ( U e. I <-> E. k e. B U = ( k .x. X ) ) ) $=
      ( wcel cfv wceq wrex cbs crg syl csn crsp cv co eleq2i crglmod csca clmod
      wb rlmlmod rlmbas eqtri cmulr cvsca rlmvsca rspval lspsnel syl2anc rlmsca
      eqid fveq2d eqtrid rexeqdv bitr4d bitrid ) EGNEHUACUBOZOZNZAEFUCHDUDPZFBQ
      ZGVGEKUEAVHVIFCUFOZUGOZROZQZVJAVKUHNZHBNVHVNUIACSNZVOLCUJTMDEFVLVMVFBVKHV
      LUTVMUTBCROZVKROICUKULDCUMOVKUNOJCUOULCUPUQURAVIFBVMABVQVMIACVLRAVPCVLPLC
      SUSTVAVBVCVDVE $.
  $}

  ${
    $d B i x y $.  $d R i y $.  $d I i $.  $d M i y $.  $d X x $.  $d Z i y $.
    $d ph i x y $.  $d .~ i x $.  $d .+ i y $.  $d .x. i y $.
    ellcsrspsn.b $e |- B = ( Base ` R ) $.
    ellcsrspsn.p $e |- .+ = ( +g ` R ) $.
    ellcsrspsn.t $e |- .x. = ( .r ` R ) $.
    ellcsrspsn.e $e |- .~ = ( R ~QG I ) $.
    ellcsrspsn.u $e |- U = ( R /s .~ ) $.
    ellcsrspsn.i $e |- I = ( ( RSpan ` R ) ` { M } ) $.
    ellcsrspsn.r $e |- ( ph -> R e. Ring ) $.
    ellcsrspsn.m $e |- ( ph -> M e. B ) $.
    ellcsrspsn.x $e |- ( ph -> X e. ( Base ` U ) ) $.
    $( Membership in a left coset in a quotient of a ring by the span of a
       singleton (that is, by the ideal generated by an element).
       (Contributed by SN, 19-Jun-2025.) $)
    ellcsrspsng $p |- ( ph -> E. x e. B ( X = [ x ] .~ /\
      ( Z e. X <-> E. y e. B Z = ( x .+ ( y .x. M ) ) ) ) ) $=
      ( vi cv cec wceq wrex wcel co wb cbs cfv quselbas syl2anc mpbid cmpt cima
      crg cgrp wss ringgrpd adantr csn crsp eqid snssd rspssbasd eqsstrid simpr
      wa eqglact syl3anc eleq2d cvv wi elex a1i eleq1 mpbiri rexlimivw ad2antrr
      ovex elimampt oveq2 eqeq2d elrspsn ovexd cbvrexima bitrd pm5.21ndd bibi1d
      ex eleq2 syl5ibrcom ancld reximdva mpd ) ALBUDZFUEZUFZBDUGZWTMLUHZMWRCUDZ
      KHUIZEUIZUFZCDUGZUJZVJZBDUGALIUKULZUHZXAUBAGURUHZXKXKXAUJTUBBDFJIGURXJLQR
      NUMUNUOAWTXIBDAWRDUHZVJZWTXHXNXHWTMWSUHZXGUJXNXOMUCDWRUCUDZEUIZUPZJUQZUHZ
      XGXNWSXSMXNGUSUHZJDUTZXMWSXSUFAYAXMAGTVAVBAYBXMAJKVCZGVDULZULDSADGYCYDYDV
      ENTAKDUAVFVGVHZVBAXMVIUCWREFGDJNQOVKVLVMXNMVNUHZXTXGXTYFVOXNMXSVPVQXGYFVO
      XNXFYFCDXFYFXEVNUHWRXDEWBMXEVNVRVSVTVQXNYFXTXGUJXNYFVJZXTMXQUFZUCJUGXGYGU
      CDXQMJXRVNXRVEXNYFVIAYBXMYFYEWAWCYGYHXFUCCJDVNXDXPXDUFXQXEMXPXDWREWDWEYGD
      GHXPCJKNPSAXLXMYFTWAAKDUHXMYFUAWAWFYGXCKHWGWHWIWLWJWIWTXBXOXGLWSMWMWKWNWO
      WPWQ $.
  $}

1. convert ply1divalg2 to use addition
2. use it with ellcsrspsng to show uniqueness:
   ( iota_ q e. z ( ( deg1 ` r ) ` q ) < ( ( deg1 ` r ) ` p ) )
3. show the remainder works ( x .+ ( y .x. M ) ) rem M = x rem M and so is equal to
   the unique value

Tada, the change to use remainder is valid.

[tirix]

I think rspsnel is similar to your elrspsn - but you've got the naming right, I don't know why I put the el at the end! :)

[tirix]

I'm not sure what properties will be useful.

I assume the useful properties will be:

• the obtained polyFld is a field extension of the original field: Ideally, ( R polyFld P ) /FldExt R , or R e. ( SubDRing ` ( R polyFld P ) ), however there is more to it, since the statement is that ( R polyFld P ) is homomorphic with a field extension of R
• the given polynomial P is the minimal polynomial of that extension : ( ( R polyFld P ) minPoly R ) = P , but again this is too simplistic as we have to take a homomorphism into account.

Overall I believe the definition of /FldExt might have to be developed so that that homomorphism is taken into account.

[metakunt]

@tirix I thought when I asked you about if your results could be relevant you said not really, since yours assume an existence of a bigger field, like the complex numbers.

But for splitting fields, wouldn't we need to construct them and prove that they are actual fields?

Maybe it would be helpful to encode the invariants of a splitting field and prove it based on those axioms only?

Then the definition of a splitting field would be, given K,L fields, and L an K-algebra and f: K[X] we have the following data:
f is a product of linear factors in L
There exists no proper subfield L' of L such that f splits over L'.

Maybe it makes sense to prove it based on this API only, kind of how I did it for primitive roots.