Powers of `ℤˣ` by `ZMod 2`

Stream: maths

[Eric Wieser]

Does the following look like a reasonable instance?

/-- There is a canonical power operation by `ℤˣ` on `ZMod 2`. -/
instance : Pow ℤˣ (ZMod 2) where
  pow s z₂ := s ^ z₂.val

lemma z₂pow_def (s : ℤˣ) (x : ZMod 2) : s ^ x = s ^ x.val := rfl

@[simp] lemma z₂pow_zero (s : ℤˣ) : (s ^ (0 : ZMod 2) : ℤˣ) = (1 : ℤˣ) := pow_zero _
@[simp] lemma z₂pow_one (s : ℤˣ) : (s ^ (1 : ZMod 2) : ℤˣ) = s := pow_one _
lemma z₂pow_add (s : ℤˣ) (x y : ZMod 2) : s ^ (x + y) = s ^ x * s ^ y := by
  simp only [z₂pow_def]
  rw [ZMod.val_add, ←pow_eq_pow_mod, pow_add]
  fin_cases s <;> simp

[Eric Wieser]

(feel free to move to #mathlib4 if this isn't quite mathematical enough)

[Eric Wieser]

Obviously that would all be more readable once we fix lean4#2220

[Eric Wieser]

The motivation is to define the tensor product of graded algebras / graded tensor product / super tensor product in #7394, where I need

$$(a \otimes b) \cdot (a' \otimes b') = (-1)^{\deg a' \deg b} (a \cdot a') \otimes (b \cdot b')$$

to make sense, where $\deg a' :$ ZMod 2

[Riccardo Brasca]

Any group has this instance.

[Riccardo Brasca]

I mean, it should have

[Eric Wieser]

I assume you mean that any group has an instance Pow G (ZMod (orderOf G))?

[Riccardo Brasca]

Yes, sorry

[Riccardo Brasca]

But it is probably not very useful

[Eric Wieser]

Though that feels a little awkward because you need orderOf G to match 2

[Riccardo Brasca]

Yes, your instance is probably better.

[Eric Wieser]

I guess you could either:

1. have a IsOfOrder G 2 typeclass, to match CharP
2. Just have an instance for any ZMod n, where the lemmas only apply if orderOf G = n

[Eric Wieser]

Riccardo Brasca said:

But it is probably not very useful

It wouldn't surprise me if I need this instance for ZMod 2 \times ZMod 2...

[Yaël Dillies]

I actually like this

[Eric Wieser]

My original or Riccardo's extension via one of my two suggestions?

[Yaël Dillies]

Riccardo's via your two suggestions

[Johan Commelin]

And maybe the n in IsOfOrder G n can be an outparam?

[Yaël Dillies]

Until someone adds an IsOfOrder G (OrderOf G)instance...

[Junyan Xu]

Did you see #6720?

[Eric Wieser]

No, but I remember reviewing a very similar PR for mathlib3, !3#11204

[Eric Wieser]

(and being opposed to it)

[Eric Wieser]

I'll ping @Joël Riou though since I see that the ZMod 2 case was specifically mentioned in a comment there

[Joël Riou]

If a good map ZMod 2 → ℤ sending the class of n to (-1)^n is defined, I would not mind redefining Int.negOnePow : ℤ → ℤ as an abbreviation for it, as long as it is as practical to use.

[Eric Wieser]

I guess my objection is to the fact the map goes to ℤ and not ℤˣ

[Eric Wieser]

Why do you want it i nℤ?

[Eric Wieser]

And just to check, is ZMod 2 your only use-case, or do you have some interest in the ZMod (orderOf G) discussion above?

[Eric Rodriguez]

Isn't ZMod (orderOf G) going to be really annoying to use in practice?

[Eric Wieser]

Not if we go via a HasOrderOf typeclass, I would guess

[Eric Wieser]

By analogy we could add a [CharP R p] : AddAction (Zmod p) R instance today if we wanted, which I think would be easy to use, but pretty niche

[Eric Wieser]

But really my question is "can I get away with the p=2 special case and a TODO comment in the short term?".

[Joël Riou]

Eric Wieser said:

Why do you want it i nℤ?

For example, if x : K ⟶ L is a morphism in a preadditive category and n : ℤ, I would like to be able to use a syntax as simple as n.negOnePow • x. I have done experiments with ((-1 : Units ℤ) ^ n : ℤ) • x, and it was not practical. I have also experimented with using the scalar multiplication SMul ℤˣ (K ⟶ L), but handling interactions between neg and SMul ℤˣ (K ⟶ L) was quite annoying.

[Eric Wieser]

Joël Riou said:

I have also experimented with using the scalar multiplication SMul ℤˣ (K ⟶ L), but handling interactions between neg and SMul ℤˣ (K ⟶ L) was quite annoying.

This is the strategy I am advocating

[Eric Wieser]

The main annoyance I'm aware of is that you have to remember to use docs#Units.neg_smul not docs#neg_smul

[Joël Riou]

As I said, I do not care about implementations details, as long as the syntax is simple and the API just works.

[Eric Wieser]

My claim is that the API for SMul ℤˣ already "just works", but it sounds like for you it didn't; I'd like to know where it didn't work so that I can fix it!

[Eric Rodriguez]

Eric Wieser said:

The main annoyance I'm aware of is that you have to remember to use docs#Units.neg_smul not docs#neg_smul

can this be fixed with some of the neg typeclasses?

[Eric Wieser]

We would need a smul version of docs#HasDistribNeg

[Joël Riou]

At the very least, there must be missing lemmas like CategoryTheory.Preadditive.comp_smul_units and CategoryTheory.Preadditive.smul_units_comp.

[Eric Wieser]

Can you link the existing lemmas?

[Joël Riou]

We would need the "units" version of docs#CategoryTheory.Preadditive.comp_zsmul docs#CategoryTheory.Preadditive.zsmul_comp or more generally of docs#CategoryTheory.Linear.comp_smul and docs#CategoryTheory.Linear.smul_comp
We would also need a suitable adaptation of docs#CategoryTheory.Functor.map_zsmul

[Joël Riou]

Presumably, for your applications, you would also need similar lemmas for the interaction between composition of linear maps and the scalar multiplication by a unit.

[Eric Wieser]

In my case I just used ext followed by docs#LinearMap.smul_apply and docs#LinearMap.map_smul_of_tower

[Eric Wieser]

But in fact docs#LinearMap.smul_comp already handles the units case

[Eric Wieser]

I guess the analog for your lemmas would be docs#AddMonoidHom.map_zsmul, which indeed is missing a Units version

[Joël Riou]

The proofs are easy:

lemma comp_smul_units {C : Type*} [Category C] [Preadditive C] {F G H : C}
  (f : F ⟶ G) (g : G ⟶ H) (n : Units ℤ) : f ≫ (n • g) = n • (f ≫ g) :=
  Preadditive.comp_zsmul _ _ _

These are just missing lemmas.

[Eric Wieser]

@loogle Units ℤ, HSMul.hSMul

[Eric Wieser]

@loogle Units ℤ, HSMul.hSMul

[loogle]

:search: AlternatingMap.domDomCongr_perm, AlternatingMap.map_congr_perm, and 16 more

[Eric Wieser]

docs#AbsoluteValue.map_units_int_smul seems to be the only precedent so far for that style of lemma

[Joël Riou]

I am trying to see whether making Preadditive.comp_zsmul a simp lemma (which they are not currently) breaks anything. #7658

[Joël Riou]

Preadditive.comp_zsmul cannot be made a simp lemma (because it is generalized by Linear.comp_smul). Then, the better phrasing of comp_units_smul lemmas etc. should be in terms of linear categories rather than preadditive categories.

[Eric Wieser]

I think the strategy I'm advocating of piling IsScalarTower/SMulCommClass on existing lemmas so they work automatically probably won't help with category theory, so I certainly am happy with #6720 to make things easier in the medium term.

[Eric Wieser]

Eric Wieser said:

But really my question is "can I get away with the p=2 special case and a TODO comment in the short term?".

In the hope the answer is yes, I've created #7661

[Eric Wieser]

I now realize that what I actually wanted was Pow ℤˣ R for any semiring R where this is well-behaved (though really just ℕ, ℤ, and ZMod 2); I guess I could make do with [Module R (Additive ℤˣ)] and use ofAdd (r • toAdd uz) instead of uz ^ r (where uz : ℤˣ)...

[Eric Wieser]

A new LawfulExponent typeclass (to-additivized to Module if possible) would probably be more principled

[Eric Wieser]

That is, something like:

/-- Typeclass for expoentiation actions by additive monoids. -/
class LawfulPow (α : Type*) (β : Type*) [Monoid α] [AddMonoid β] extends Pow α β where
  pow_zero (a : α) : a ^ 0 = 1
  pow_add (a : α) (b₁ b₂ : β) : a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
  one_pow (b : β) : (1 : α) ^ b = 1
  mul_pow (a₁ a₂ : α) (b : β) (ha : Commute a₁ a₂) : (a₁ * a₂) ^ b = a₁ ^ b * a₂ ^ b

[Eric Wieser]

Which I think would cover npow, zpow, NNreal.rpow, and the z₂pow above

[Eric Wieser]

Eric Wieser said:

I guess I could make do with [Module R (Additive ℤˣ)] and use ofAdd (r • toAdd uz) instead of uz ^ r (where uz : ℤˣ)...

#7866 does exactly this and works well enough here, and is much less work than the new typeclass!