Zulip Chat Archive

Stream: general

Topic: diamond: galois_field algebras

Eric Rodriguez (Jun 25 2022 at 10:34):

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 (Jun 25 2022 at 10:34):

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 (Jun 25 2022 at 10:51):

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 (Jun 25 2022 at 11:13):

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

Eric Rodriguez (Jun 25 2022 at 12:07):

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

Eric Rodriguez (Jun 25 2022 at 12:54):

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

Eric Wieser (Jun 25 2022 at 15:10):

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 (Jun 25 2022 at 15:13):

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

Anne Baanen (Jun 26 2022 at 12:20):

docs#zmod.algebra ← for the lazy

Anne Baanen (Jun 26 2022 at 12:22):

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 (Jun 26 2022 at 12:31):

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 (Jun 26 2022 at 13:36):

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 (Jun 26 2022 at 13:38):

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 (Jun 27 2022 at 08:42):

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 (Jun 27 2022 at 08:43):

Do we need zmod_smul?

Eric Wieser (Jun 27 2022 at 08:44):

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

Anne Baanen (Jun 27 2022 at 08:48):

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 (Jul 11 2022 at 11:52):

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 (Jul 11 2022 at 11:53):

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

Anne Baanen (Jul 11 2022 at 12:00):

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 (Jul 11 2022 at 12:01):

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

Eric Rodriguez (Jul 11 2022 at 12:11):

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

Eric Rodriguez (Jul 11 2022 at 12:12):

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 (Jul 11 2022 at 12:13):

that seems very maths-unfriendly though

Yaël Dillies (Jul 11 2022 at 12:13):

Can't the weak one simply be nonempty strong_char_p?

Eric Rodriguez (Jul 11 2022 at 12:13):

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

Eric Wieser (Jul 11 2022 at 16:13):

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

Eric Rodriguez (Jul 11 2022 at 16:24):

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

Last updated: Aug 03 2023 at 10:10 UTC