General group homomorphism definition

Stream: new members

[gjohn]

I am trying to prove the homomorphism between Z4 and $$M2R\4$$. the two have group structure defined using + and * respectively.
I found MulEquiv and AddEquiv but what i need is a general definition: toFun( a * b) = toFun(a) + toFun(b).
Here is the full code:

import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.Group.Hom.Defs
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import Mathlib.Data.ZMod.Basic
import Mathlib.Util.Delaborators

namespace GTheory_Physics


abbrev Z4 := ZMod 4

def Z4Group: AddGroup Z4 where
  add := (· + · )
  add_assoc a b c:= by apply add_assoc
  zero := 0
  zero_add a := by apply zero_add
  add_zero a:= by apply add_zero
  nsmul := nsmulRec
  neg a := -a
  zsmul:= zsmulRec
  neg_add_cancel a := by apply neg_add_cancel
  sub_eq_add_neg := by
    intro a b
    simp
    exact sub_eq_add_neg a b


abbrev M2R := Matrix ( Fin 2) (Fin 2) ℚ

namespace M2R

@[simp] def e : M2R := !![1,0; 0,1]

@[simp] def a : M2R := !![0, -1; 1,  0]

@[simp] def b : M2R := !![-1,  0; 0, -1]

@[simp] def c : M2R := !![0,  1;-1, 0]


@[simp] def S: Finset M2R := {e, a, b, c}

abbrev M2R₄ := {m: M2R // m ∈ S}

theorem mul_closed (a b: M2R) (ha: a ∈ S) (hb: b ∈ S ) : (a * b) ∈ S := by
    fin_cases ha <;>  fin_cases hb <;> simp

instance: Mul M2R₄ where
    mul a b := ⟨a.val * b.val, mul_closed a.val b.val a.prop b.prop ⟩


@[simp]
noncomputable def m2r_inv (x: M2R) : M2R :=
    x⁻¹

theorem inv_closed (a : M2R) (ha: a ∈ S) : m2r_inv a ∈ S := by
    fin_cases ha <;> simp [Matrix.inv_def]

noncomputable instance: Inv M2R₄ where
    inv a := ⟨m2r_inv a.val, inv_closed a.val a.prop⟩

instance : One M2R₄  :=
    ⟨e, by decide⟩

@[simp]
theorem mul_def (a b: M2R₄) :
    a * b = ⟨a.val * b.val, mul_closed a.val b.val a.prop b.prop ⟩ :=
    rfl

@[simp]
theorem inv_def (a: M2R₄) :
    a⁻¹ = ⟨m2r_inv a.val, inv_closed a.val a.prop⟩ :=
    rfl

@[simp]
theorem one_def : ( 1: M2R₄) = ⟨e, by decide⟩ :=
    rfl

@[to_additive M2RAddGroup]
noncomputable def M2RGroup: Group M2R₄ where
  mul := ( · * · )
  mul_assoc a b c := by
    simp
    apply Matrix.mul_assoc
  one := 1
  one_mul := by
    intro x
    simp
    ext i j
    fin_cases i <;> fin_cases j <;> fin_cases x <;> simp
  mul_one := by
    intro x
    simp
    ext i j
    fin_cases i <;> fin_cases j <;> fin_cases x <;> simp
  inv := ( · ⁻¹ )
  inv_mul_cancel := by
    intro x
    simp
    rw [Matrix.nonsing_inv_mul]
    .  decide
    .  fin_cases x <;> simp


def m2r_eq_z4 : M2R.M2R₄ ≃ Z4 where
  toFun := fun x =>
    if x.val = M2R.e then 0
    else if x.val = M2R.a then 1
    else if x.val = M2R.b then 2
    else if x.val = M2R.c then 3
    else 3  -- This must be M2R.c due to the subset type constraint

  invFun := fun x =>
    if x = 0 then ⟨M2R.e, by decide⟩
    else if x = 1 then ⟨M2R.a, by decide⟩
    else if x = 2 then ⟨M2R.b, by decide⟩
    else if x = 3 then ⟨M2R.c, by decide⟩
    else ⟨M2R.c, by decide⟩  -- This must be 3 due to Z4 having only 4 elements

  left_inv := by
    intro x
    fin_cases x
    any_goals try simp
    any_goals try exact rfl

  right_inv := by
    intro x
    fin_cases x
    any_goals try simp
    any_goals try exact rfl

-- M2R₄ has `*` and Z4 has `+`
def m2r_group_eq_z4_group: M2R₄ ≃* Z4 where
  toFun := m2r_eq_z4.toFun
  invFun := m2r_eq_z4.invFun
  left_inv := m2r_eq_z4.left_inv
  right_inv := m2r_eq_z4.right_inv
  -- CHANGE: I want toFun ( a * b) = toFun(a) + toFun(b)
  -- While i have only toFun(a*b) = toFun(a) * toFun(b)
  -- Or toFun(a+b) = toFun(a) + toFun(b)
  map_mul' := by

obviously one can define the expected structure separately but i wonder if lean already has it?

[Aaron Liu]

You could say that M2R₄ ≃* Multiplicative Z4 or that Additive M2R₄ ≃+ Z4

[Aaron Liu]

See #new members > ✔ Homomorphisms from additive group to multiplicative @ 💬

[Jireh Loreaux]

import Mathlib.Tactic
import Mathlib.Util.Delaborators

lemma foo : (!![1,0; 0,1] : Matrix (Fin 2) (Fin 2) ℚ) = 1 := by
  ext i j; fin_cases i <;> fin_cases j <;> norm_num

def a : Matrix (Fin 2) (Fin 2) ℚ := !![0, -1; 1,  0]

def b : Matrix (Fin 2) (Fin 2) ℚ := !![-1,  0; 0, -1]

def c : Matrix (Fin 2) (Fin 2) ℚ := !![0,  1;-1, 0]

open Additive

def Z4_to_M2R : ZMod 4 →+ Additive (Matrix (Fin 2) (Fin 2) ℚ) where
  toFun := fun
    | 0 => ofMul 1
    | 1 => ofMul a
    | 2 => ofMul b
    | 3 => ofMul c
  map_zero' := by simp
  map_add' x y := by
    fin_cases x <;> fin_cases y
    all_goals simp [a, b, c, ← ofMul_mul, foo]
    all_goals norm_num

[Jireh Loreaux]

I would not define your matrix group the way you do. Instead, I would define it in terms of this morphism (as its range), and then prove that its coercion to set is {ofMul 1, ofMul a, ofMul b, ofMul c}. Then you get the isomorphism for free.

[gjohn]

Thanks @Aaron Liu and @Jireh Loreaux
Let me try these

[Edward van de Meent]

this reminds me of my dream of structures for exponential and logarithmic maps

[Aaron Liu]

We are already duplicating additive and multiplicative api, that sound like less of a dream and more of a nightmare

[Aaron Liu]

Composition for example, now you're adding 6 new ways to compose maps

[Aaron Liu]

And that's 6 new ways to compose homomorphisms, and 6 new ways to compose isomorphisms, and 14 new lemmas that say composition is associative, and again for the isomorphisms, and ...

[Edward van de Meent]

like i said, a dream, not something realistic

[Yaël Dillies]

docs#AddChar already exists, so half your dream is in mathlib already