diamond: galois_field algebras

Stream: general

[Eric Rodriguez]

We have that : zmod.algebra (galois_field p n) p is not defeq to splitting_field.algebra (X ^ p ^ n - X) = galois_field.algebra (and I think this is a known issue). I can't prove the propositional equality; I can't figure out a way to case so that we can actually use the definition of splitting_field_aux. How should we deal with this? I tried disabling the instance docs#galois_field.algebra, but I can't seem to figure out how to as many of the results about splitting fields implicitly use this instance (and I don't have the propeq). I also guess there's not a subsingleton instance for this sort of algebra, due to automorphisms.

[Eric Rodriguez]

this came up in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Algebraic.20Conjugate.20over.20Finite.20Fields/near/287426797

[Kevin Buzzard]

If there were an instance of subsingleton (algebra (zmod n) R) (which there should be, I don't know if it's there already) then convert might be able to do some of the heavy lifting for you. 1 has to go to 1 and that uniquely determines the ring hom from zmod n.

[Eric Rodriguez]

oh, 1 does have to go to 1! I'll try make that instance, I don't think it exists

[Eric Rodriguez]

#14946 has the subsingleton instance; I'll make the followup PR when this compiles

[Eric Rodriguez]

and #14947 fixes everything, hopefully, but maybe not the best solution

[Eric Wieser]

Note that the zmod algebra diamond runs much deeper:

import data.zmod.algebra
-- fails :(
example (p : ℕ) : algebra.id (zmod p) = zmod.algebra _ p := rfl

[Eric Wieser]

We probably shouldn't think too hard about that until we fix the int and nat diamonds

[Anne Baanen]

docs#zmod.algebra ← for the lazy

[Anne Baanen]

Would it be sufficient (help) to extend docs#char_p with a of_zmod/zmod_smul field? Perhaps fin instead of zmod, to avoid having to do even more import hierarchy restructuring.

[Anne Baanen]

The main drawback I foresee is that we break the defeq of algebra_map (zmod n) R = (coe : zmod n → R). I don't think that's likely to undermine a lot of existing results, so I think it's a fine solution to add these fields to char_p.

[Eric Rodriguez]

I think we should use zmod, I just tried removing the import to char_p.basic in zmod.basic and the only thing it broke seemed irrelevant (docs#function.left_inverse.right_inverse_of_card_le) (there's some weird transitive import stuff goin on, as char_p stays imported, but we lose something else?); regardless of that, how will we deal with the 0 case? I think an ite/pattern match in the definition will only cause more problems

[Eric Rodriguez]

I'm happy to try do this refactor, but I'm not sure about the full list of steps - we redefine this algebra instance to use the of_zmod/zmod_smul field, and then what? For example, how concretely do we solve the algebra.id diamond; do we set the zmod.char_p instance to use the zmod_smul equal to the algebra.id one?

[Anne Baanen]

That is indeed basically the idea: we avoid diamonds by ensuring the data-carrying fields of docs#algebra.id and docs#zmod.algebra coincide. Because the fields in the (new) zmod.algebra come from zmod.char_p, we need to supply new values coming from algebra.id. In particular, we should set of_zmod := id and zmod_smul := (*).

[Eric Wieser]

Do we need zmod_smul?

[Eric Wieser]

Oh, I guess it matches what we do for nat and int

[Anne Baanen]

I don't know that we will need it in this case, but I expect it (pretty likely that the case distinction on zmod 0 vs zmod (n+1) happens in a different place). In any case, might as well incorporate it and save some work for when we do need it.

[Eric Rodriguez]

hmm, I finally started trying to do it in earnest and realised one thing that's different here from the other refactors: char_p was a Prop before.

[Eric Rodriguez]

I'm not sure how to deal with that apart from sprinkling nonemptys everywhere, which doesn't seem nice

[Anne Baanen]

Where exactly do you want to put the nonempty? Because we can't solve diamonds by putting the data in nonempty (the diamond would then be expected_coe =?= nonempty.some (nonempty.mk expected_coe)).

[Anne Baanen]

So indeed we'd have to turn char_p into something living in Type*.

[Eric Rodriguez]

I meant for example for theorems such as docs#char_p.exists

[Eric Rodriguez]

I wonder if there should be a "weak" char_p (current version) and a "strong" one (new version), with only the "strong" one providing the algebra instance

[Eric Rodriguez]

that seems very maths-unfriendly though

[Yaël Dillies]

Can't the weak one simply be nonempty strong_char_p?

[Eric Rodriguez]

we could also try and replace all non-tc uses of char_p with ring_char, but that's also odd

[Eric Wieser]

Is making char_p X p carry data any different to just making users write algebra (zmod p) X instead?

[Eric Rodriguez]

not really, actually, and I think that's in some ways the approach taken already in some files