/-
  StarG/Basic.lean, Lean 4.29 / current Mathlib compatible
-/
import Mathlib

set_option linter.unusedSectionVars false

open Finset BigOperators Matrix

noncomputable section

abbrev GroupTensor (G : Type*) [Fintype G] (ℓ m : ℕ) :=
  G → Matrix (Fin ℓ) (Fin m) ℝ

namespace GroupTensor

variable {G : Type*} [Group G] [Fintype G] [DecidableEq G]
variable {ℓ m p : ℕ}

def convTensor (a b c : G) : ℝ :=
  if a * b = c then 1 else 0

@[simp] theorem convTensor_eq (a b : G) : convTensor a b (a * b) = 1 := by
  simp [convTensor]

@[simp] theorem convTensor_ne {a b c : G} (h : a * b ≠ c) :
    convTensor a b c = 0 := by
  simp [convTensor, h]

theorem convTensor_eq_ite (a b c : G) :
    convTensor a b c = if a * b = c then 1 else 0 := rfl

theorem convTensor_assoc (a b c e : G) :
    ∑ d : G, convTensor a b d * convTensor d c e =
    ∑ d : G, convTensor a d e * convTensor b c d := by
  have lhs : ∑ d : G, convTensor a b d * convTensor d c e =
      convTensor (a * b) c e := by
    rw [Fintype.sum_eq_single (a * b)]
    · simp
    · intro d hd; simp [convTensor_eq_ite, Ne.symm hd]
  have rhs : ∑ d : G, convTensor a d e * convTensor b c d =
      convTensor a (b * c) e := by
    rw [Fintype.sum_eq_single (b * c)]
    · simp
    · intro d hd; simp [convTensor_eq_ite, Ne.symm hd]
  rw [lhs, rhs, convTensor_eq_ite, convTensor_eq_ite, mul_assoc]

theorem convTensor_identity_left (b c : G) :
    convTensor (1 : G) b c = if b = c then 1 else 0 := by
  simp [convTensor, one_mul]

theorem convTensor_identity_right (a c : G) :
    convTensor a (1 : G) c = if a = c then 1 else 0 := by
  simp [convTensor, mul_one]

theorem convTensor_permutation (a : G) :
    ∀ b : G, ∃! c : G, convTensor a b c = 1 := by
  intro b; exact ⟨a * b, by simp, fun c hc => by
    simp [convTensor] at hc; exact hc.symm⟩

def starG (A : GroupTensor G ℓ m) (B : GroupTensor G m p) :
    GroupTensor G ℓ p :=
  fun c i j => ∑ k : Fin m, ∑ a : G, A a i k * B (a⁻¹ * c) k j

infixl:70 " ⋆ " => starG

def starTranspose (A : GroupTensor G ℓ m) : GroupTensor G m ℓ :=
  fun g i j => A g⁻¹ j i

scoped postfix:max "ᴴ" => starTranspose

def starIdentity : GroupTensor G ℓ ℓ :=
  fun g => if g = 1 then (1 : Matrix (Fin ℓ) (Fin ℓ) ℝ) else 0

notation "ℐ" => starIdentity

end GroupTensor
end