Simplifying hidden function coercion mess

Stream: new members

[Gareth Ma]

I have the following proof:

import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
/- import Mathlib.RingTheory.SimpleModule -/

open LinearMap Module Submodule Representation FiniteDimensional Function Pointwise CategoryTheory
  MonoidAlgebra

variable {n : ℕ} (hn : 1 < n) {𝕜 : Type} [Field 𝕜] {ζ : 𝕜} (hζ : ζ ∈ primitiveRoots n 𝕜)

example {k : ℕ} : (FGModuleCat.of 𝕜 𝕜) → (FGModuleCat.of 𝕜 𝕜) :=
  -- Without the cast rfl it doesn't work, even when marking as (x : 𝕜)
  fun x ↦ (cast rfl x : 𝕜) * (ζ : 𝕜) ^ k

-- this is very weird
theorem aux (f : (FGModuleCat.of 𝕜 𝕜).obj →ₗ[𝕜] (FGModuleCat.of 𝕜 𝕜).obj) :
    f = (1 : End (FGModuleCat.of 𝕜 𝕜)) ↔ f.toFun = _root_.id := by
  constructor <;> intro h
  · subst h; ext; simp; exact CategoryTheory.id_apply _
  · ext; change f.toFun _ = _; rw [h]; rfl

-- what?
@[ext] theorem af (f g : End (FGModuleCat.of 𝕜 𝕜)) (h : f.toFun = g.toFun) : f = g := by
  cases f; cases g; congr!; simpa using h

lemma zeta_pow_mod_eq {k : ℕ} : ζ ^ (k % n) = ζ ^ k := by
  nth_rw 2 [← Nat.mod_add_div k n]
  rw [mem_primitiveRoots (zero_lt_one.trans hn)] at hζ
  rw [pow_add, pow_mul, hζ.pow_eq_one, one_pow, mul_one]

def cyc_rep : FdRep 𝕜 (Multiplicative (ZMod n)) where
  V := FGModuleCat.of 𝕜 𝕜
  ρ := by
    refine MonCat.ofHom <| MonoidHom.mk (OneHom.mk ?_ ?_) ?_
    · intro k
      refine ⟨⟨fun x ↦ (cast rfl x : 𝕜) * ζ ^ k.val, ?_⟩, ?_⟩
      · intros; simp [add_mul]
      · intros; simp [← mul_assoc]
    · have : (1 : Multiplicative (ZMod n)).val = 0 := (ZMod.val_eq_zero _).mpr rfl
      rw [aux]; ext; simp [this]
    · -- this proof is disgusting
      intro x y
      ext z
      simp [obj_carrier]
      have : ζ ^ (x * y).val = ζ ^ y.val * ζ ^ x.val := by
        have : x * y = Multiplicative.toAdd x + Multiplicative.toAdd y := by rw [← toAdd_mul]; rfl
        rw [this, mul_comm, @ZMod.val_add _ ⟨by omega⟩, zeta_pow_mod_eq hn hζ, pow_add]
        rfl
      -- I still don't know what this is doing
      rw [LinearMap.mul_apply, this, ← mul_assoc]
      rfl

And this is currently sorry-free, but I feel like I did it the "wrong way", as in there is a lot of weird function coercion steps in the middle in some weird ways, as commented above. If anyone has some extra time can someone try to simplify the proof and/or point out how this could've been better

[Gareth Ma]

Also this top example

example {k : ℕ} : (FGModuleCat.of 𝕜 𝕜) → (FGModuleCat.of 𝕜 𝕜) :=
  -- Without the cast rfl it doesn't work, even when marking as (x : 𝕜)
  fun x ↦ (cast rfl x : 𝕜) * (ζ : 𝕜) ^ k

is very confusing to me, but I can't tell if it's a bug or not

[Gareth Ma]

(I have a way shorter definition now, but I still want to use the categorical definition just as demonstration)

def cyc_rep' : Multiplicative (ZMod n) →* (𝕜 →ₗ[𝕜] 𝕜) where
  toFun := fun k ↦ {
    toFun := fun x ↦ x * ζ ^ k.val
    map_add' := by intros; simp [add_mul]
    map_smul' := by intros; simp [← mul_assoc]
  }
  map_one' := by ext; simp; convert pow_zero ζ; simp only [ZMod.val_eq_zero]; rfl
  map_mul' := by
    intros x y
    ext
    have : x * y = Multiplicative.toAdd x + Multiplicative.toAdd y := by rw [← toAdd_mul]; rfl
    simp
    rw [this, mul_comm, @ZMod.val_add _ ⟨by omega⟩, zeta_pow_mod_eq hn hζ, pow_add]
    rfl

noncomputable def cyc_rep'' : FdRep 𝕜 (Multiplicative (ZMod n)) := FdRep.of (cyc_rep' hn hζ)

[Kevin Buzzard]

Gareth Ma said:

Also this top example

example {k : ℕ} : (FGModuleCat.of 𝕜 𝕜) → (FGModuleCat.of 𝕜 𝕜) :=
  -- Without the cast rfl it doesn't work, even when marking as (x : 𝕜)
  fun x ↦ (cast rfl x : 𝕜) * (ζ : 𝕜) ^ k

is very confusing to me, but I can't tell if it's a bug or not

How about

example {k : ℕ} : (FGModuleCat.of 𝕜 𝕜) → (FGModuleCat.of 𝕜 𝕜) :=
  fun x ↦ (ζ : 𝕜) ^ k • x

?

[Kevin Buzzard]

-- this is very weird
theorem aux (f : (FGModuleCat.of 𝕜 𝕜).obj →ₗ[𝕜] (FGModuleCat.of 𝕜 𝕜).obj) :
    f = (1 : End (FGModuleCat.of 𝕜 𝕜)) ↔ f.toFun = _root_.id := by

I think f.toFun is a code smell, whatever you're trying to do. Use coercions to function.

[Gareth Ma]

I can replace it with f.toAddHom = AddHom.id _, is that better?

[Gareth Ma]

How about

example {k : ℕ} : (FGModuleCat.of 𝕜 𝕜) → (FGModuleCat.of 𝕜 𝕜) :=
  fun x ↦ (ζ : 𝕜) ^ k • x

Oh! That's why * doesn't work. I changed my proof below but that doesn't shorten the proof

[Gareth Ma]

At least it makes more sense

[Eric Wieser]

Or write ⇑f = _root_.id

[Gareth Ma]

Ahh,. I see

[Kevin Buzzard]

Here's my effort to make the fdRep:

import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
/- import Mathlib.RingTheory.SimpleModule -/

open LinearMap Module Submodule Representation FiniteDimensional Function Pointwise CategoryTheory
  MonoidAlgebra

variable {n : ℕ} (hn : 1 < n) {𝕜 : Type} [Field 𝕜] {ζ : 𝕜} (hζ : ζ ∈ primitiveRoots n 𝕜)

-- this proof should work with just `NeZero n`
lemma zeta_pow_mod_eq {k : ℕ} : ζ ^ (k % n) = ζ ^ k := by
  nth_rw 2 [← Nat.mod_add_div k n]
  rw [mem_primitiveRoots (zero_lt_one.trans hn)] at hζ
  rw [pow_add, pow_mul, hζ.pow_eq_one, one_pow, mul_one]

-- and what you really want is ζ ^ a = ζ ^ b ↔ a % n = b % n

-- missing API?
lemma foo (a b : ZMod n) : (a + b).val % n = (a.val + b.val) % n := by
  have : NeZero n := ⟨by omega⟩ -- that should be the assumption
  simp [← ZMod.natCast_eq_natCast_iff']

open Multiplicative in
def Representation.cyc_rep : Representation 𝕜 (Multiplicative (ZMod n)) 𝕜 where
  toFun mk := lsmul 𝕜 𝕜 (ζ ^ (toAdd mk).val)
  map_one' := by ext; simp
  map_mul' x y := by
    ext
    simp
    rw [← pow_add, ← zeta_pow_mod_eq hn hζ, foo hn, zeta_pow_mod_eq hn hζ]

noncomputable def cyc_rep :
    FdRep 𝕜 (Multiplicative (ZMod n)) :=
  FdRep.of (Representation.cyc_rep hn hζ)

[Gareth Ma]

Damn, I look back at my original attempt and I have no idea what I'm doing. This is a lot cleaner, thanks

[Yaël Dillies]

Are you looking for docs#ZMod.cast_add, Kevin?

[Eric Wieser]

I'd split that further and go with

/-- Like `zpowersHom` but for `ZMod` and primitive roots. -/
@[simps]
def zmodpowersHom {ζ : 𝕜} (hζ : ζ ∈ primitiveRoots n 𝕜) : Multiplicative (ZMod n) →* 𝕜 where
  toFun := fun mk => (ζ ^ mk.toAdd.val)
  map_one' := by simp
  map_mul' := fun x y => by
    simp
    rw [← pow_add, ← zeta_pow_mod_eq hn hζ, foo hn, zeta_pow_mod_eq hn hζ]

open Multiplicative in
def Representation.cyc_rep : Representation 𝕜 (Multiplicative (ZMod n)) 𝕜 :=
  (Algebra.lsmul 𝕜 𝕜 𝕜).toMonoidHom.comp (zmodpowersHom hn hζ)