Definitions/Def_IntMatrixOrder_StructureConstants.lean

import Mathlib

set_option autoImplicit false

noncomputable section

open Matrix

namespace IntMatrixOrder

variable {G : Type*} {n K : ℕ} (T : G → Matrix (Fin n) (Fin n) ℤ) (u : Fin K → Matrix (Fin n) (Fin n) ℤ)
  (c : Fin K → Fin K → Fin K → ℤ) (c₁ : Fin K → ℤ) (cT : G → Fin K → ℤ)

section AnyRing

variable (R' : Type*) [CommRing R']

abbrev uC (k : Fin K) : Matrix (Fin n) (Fin n) R' := (u k).map (Int.castRingHom R')

theorem uC_eq (k : Fin K) : uC u R' k = (Int.castRingHom R').mapMatrix (u k) := rfl

abbrev TC (g : G) : Matrix (Fin n) (Fin n) R' := (T g).map (Int.castRingHom R')

theorem TC_eq (g : G) : TC T R' g = (Int.castRingHom R').mapMatrix (T g) := rfl

def elemM (a : Fin K → R') : Matrix (Fin n) (Fin n) R' := ∑ k, a k • uC u R' k

def cstar (a b : Fin K → R') : Fin K → R' := fun m => ∑ k, ∑ l, a k * b l * (c k l m : R')

def Lm (a : Fin K → R') : Matrix (Fin K) (Fin K) R' := Matrix.of fun m l => ∑ k, a k * (c k l m : R')

theorem Lm_mulVec (a b : Fin K → R') : Lm c R' a *ᵥ b = cstar c R' a b := by
  funext m
  simp only [Lm, cstar, Matrix.mulVec, dotProduct, Matrix.of_apply, Finset.sum_mul]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl fun k _ => Finset.sum_congr rfl fun l _ => ?_
  ring

theorem cstar_add_right (a b b' : Fin K → R') : cstar c R' a (b + b') = cstar c R' a b + cstar c R' a b' := by
  rw [← Lm_mulVec, ← Lm_mulVec, ← Lm_mulVec, Matrix.mulVec_add]

theorem cstar_smul_right (z : R') (a b : Fin K → R') : cstar c R' a (z • b) = z • cstar c R' a b := by
  rw [← Lm_mulVec, ← Lm_mulVec, Matrix.mulVec_smul]

theorem cstar_add_left (a a' b : Fin K → R') : cstar c R' (a + a') b = cstar c R' a b + cstar c R' a' b := by
  funext m
  simp only [cstar, Pi.add_apply, add_mul, Finset.sum_add_distrib]

theorem cstar_smul_left (z : R') (a b : Fin K → R') : cstar c R' (z • a) b = z • cstar c R' a b := by
  funext m
  simp only [cstar, Pi.smul_apply, smul_eq_mul, Finset.mul_sum, mul_assoc]

theorem elemM_single (k : Fin K) : elemM u R' (Pi.single k 1) = uC u R' k := by
  rw [elemM, Finset.sum_eq_single k]
  · rw [Pi.single_eq_same, one_smul]
  · intro l _ hl; rw [Pi.single_eq_of_ne hl, zero_smul]
  · intro h; exact absurd (Finset.mem_univ k) h

theorem elemM_add (a b : Fin K → R') : elemM u R' (a + b) = elemM u R' a + elemM u R' b := by
  simp only [elemM, Pi.add_apply, add_smul, Finset.sum_add_distrib]

theorem elemM_smul (z : R') (a : Fin K → R') : elemM u R' (z • a) = z • elemM u R' a := by
  simp only [elemM, Pi.smul_apply, smul_eq_mul, Finset.smul_sum, smul_smul]

theorem elemM_map {R'' : Type*} [CommRing R''] (f : R' →+* R'') (a : Fin K → R') :
    (elemM u R' a).map f = elemM u R'' (f ∘ a) := by
  ext i j
  simp [elemM, uC, Matrix.map_apply, Matrix.sum_apply, map_sum]

theorem cstar_map {R'' : Type*} [CommRing R''] (f : R' →+* R'') (a b : Fin K → R') :
    f ∘ cstar c R' a b = cstar c R'' (f ∘ a) (f ∘ b) := by
  funext m
  simp [cstar, map_sum]

theorem Lm_map {R'' : Type*} [CommRing R''] (f : R' →+* R'') (a : Fin K → R') :
    (Lm c R' a).map f = Lm c R'' (f ∘ a) := by
  ext m l
  simp [Lm, Matrix.map_apply, map_sum]

theorem uC_map {R'' : Type*} [CommRing R''] (f : R' →+* R'') (k : Fin K) :
    (uC u R' k).map f = uC u R'' k := by
  ext i j; simp [Matrix.map_apply]

theorem TC_map {R'' : Type*} [CommRing R''] (f : R' →+* R'') (g : G) :
    (TC T R' g).map f = TC T R'' g := by
  ext i j; simp [Matrix.map_apply]

variable (hu_mul : ∀ k l : Fin K, u k * u l = ∑ m, c k l m • u m) (hu_one : ∑ m, c₁ m • u m = 1)
  (hu_T : ∀ g : G, ∑ m, cT g m • u m = T g)

include hu_mul in
theorem uC_mul (k l : Fin K) : uC u R' k * uC u R' l = ∑ m, (c k l m : R') • uC u R' m := by
  have h := congrArg (Int.castRingHom R').mapMatrix (hu_mul k l)
  rw [map_mul, map_sum] at h
  rw [uC_eq, uC_eq, h]
  refine Finset.sum_congr rfl fun m _ => ?_
  rw [map_zsmul, uC_eq, Int.cast_smul_eq_zsmul]

include hu_one in
theorem elemM_c₁ : elemM u R' (fun m => (c₁ m : R')) = 1 := by
  have h := congrArg (Int.castRingHom R').mapMatrix hu_one
  rw [map_sum, map_one] at h
  rw [← h, elemM]
  refine Finset.sum_congr rfl fun m _ => ?_
  rw [map_zsmul, uC_eq, Int.cast_smul_eq_zsmul]

include hu_T in
theorem elemM_cT (g : G) : elemM u R' (fun m => (cT g m : R')) = TC T R' g := by
  have h := congrArg (Int.castRingHom R').mapMatrix (hu_T g)
  rw [map_sum] at h
  rw [TC_eq, ← h, elemM]
  refine Finset.sum_congr rfl fun m _ => ?_
  rw [map_zsmul, uC_eq, Int.cast_smul_eq_zsmul]

include hu_mul in

theorem elemM_cstar (a b : Fin K → R') : elemM u R' (cstar c R' a b) = elemM u R' a * elemM u R' b := by
  have hR : elemM u R' a * elemM u R' b = ∑ k, ∑ l, ∑ m, (a k * b l * (c k l m : R')) • uC u R' m := by
    simp only [elemM, Finset.sum_mul, Finset.mul_sum, smul_mul_smul_comm, uC_mul u c R' hu_mul,
      Finset.smul_sum, smul_smul]
    exact Finset.sum_comm
  have hL : elemM u R' (cstar c R' a b) = ∑ m, ∑ k, ∑ l, (a k * b l * (c k l m : R')) • uC u R' m := by
    simp only [elemM, cstar]
    refine Finset.sum_congr rfl fun m _ => ?_
    rw [Finset.sum_smul]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Finset.sum_smul]
  rw [hL, hR, Finset.sum_comm]
  refine Finset.sum_congr rfl fun k _ => ?_
  rw [Finset.sum_comm]

theorem Lm_single (κ : Fin K) : Lm c R' (Pi.single κ 1) = Matrix.of fun m l => (c κ l m : R') := by
  ext m l
  simp only [Lm, Matrix.of_apply]
  rw [Finset.sum_eq_single κ (fun b _ hb => by rw [Pi.single_eq_of_ne hb, zero_mul])
    (fun h => (h (Finset.mem_univ κ)).elim), Pi.single_eq_same, one_mul]

theorem Lm_eq_sum (a : Fin K → R') : Lm c R' a = ∑ κ, a κ • Lm c R' (Pi.single κ 1) := by
  simp only [Lm_single]
  ext m l
  simp only [Lm, Matrix.of_apply, Matrix.sum_apply, Matrix.smul_apply, smul_eq_mul]

theorem of_intCast_map {R'' : Type*} [CommRing R''] (f : R' →+* R'') (κ : Fin K) :
    (Matrix.of fun m l => (c κ l m : R')).map f = Matrix.of fun m l => (c κ l m : R'') := by
  ext m l; simp [Matrix.map_apply]

theorem mul_elemM_mul_eq_of_single {m' : Type*} [Fintype m'] (β : Matrix m' (Fin n) R')
    (e : Matrix (Fin n) (Fin n) R') (P : Matrix (Fin K) (Fin K) R' → Matrix m' (Fin n) R')
    (hP : ∀ κ, β * uC u R' κ * e = P (Lm c R' (Pi.single κ 1)))
    (hPadd : ∀ X Y, P (X + Y) = P X + P Y) (hPsmul : ∀ (z : R') X, P (z • X) = z • P X) (hP0 : P 0 = 0)
    (a : Fin K → R') : β * elemM u R' a * e = P (Lm c R' a) := by
  classical
  have h1 : β * elemM u R' a * e = ∑ κ, a κ • (β * uC u R' κ * e) := by
    simp only [elemM, Matrix.mul_sum, Matrix.sum_mul, Matrix.mul_smul, Matrix.smul_mul]
  have h2 : P (Lm c R' a) = ∑ κ, a κ • P (Lm c R' (Pi.single κ 1)) := by
    rw [Lm_eq_sum]
    induction (Finset.univ : Finset (Fin K)) using Finset.induction_on with
    | empty => rw [Finset.sum_empty, Finset.sum_empty, hP0]
    | insert x s hx ih => rw [Finset.sum_insert hx, Finset.sum_insert hx, hPadd, hPsmul, ih]
  rw [h1, h2]
  exact Finset.sum_congr rfl fun κ _ => by rw [hP]

theorem mulVec_elemM_mulVec (β : Matrix (Fin K) (Fin n) R') (e : Matrix (Fin n) (Fin n) R')
    (hIa : ∀ s, β * elemM u R' s * e = (Lm c R' s)ᵀ * β * e) (s : Fin K → R') (x : Fin n → R')
    (hex : e *ᵥ x = x) : β *ᵥ (elemM u R' s *ᵥ x) = (Lm c R' s)ᵀ *ᵥ (β *ᵥ x) := by
  conv_lhs => rw [← hex]
  rw [Matrix.mulVec_mulVec, Matrix.mulVec_mulVec, hIa, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec, hex]

theorem dotProduct_Lm_transpose_mulVec (a s w : Fin K → R') :
    a ⬝ᵥ ((Lm c R' s)ᵀ *ᵥ w) = cstar c R' s a ⬝ᵥ w := by
  rw [Matrix.dotProduct_mulVec, ← Matrix.mulVec_transpose, Matrix.transpose_transpose, Lm_mulVec]

end AnyRing

section Descent

variable (R : Type*) [CommRing R] [CharZero R]

theorem linearIndependent_int_of_uC (huind : LinearIndependent R (fun k : Fin K => uC u R k)) :
    LinearIndependent ℤ u := by
  rw [Fintype.linearIndependent_iff] at huind ⊢
  intro g hg k
  have h := congrArg (Int.castRingHom R).mapMatrix hg
  rw [map_sum, map_zero] at h
  have h' : ∑ i, (g i : R) • uC u R i = 0 := by
    rw [← h]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [map_zsmul, uC_eq, Int.cast_smul_eq_zsmul]
  exact (Int.castRingHom R).injective_int (by rw [map_zero]; exact huind _ h' k)

theorem u_comm_of_uC_comm (h : ∀ k l : Fin K, uC u R k * uC u R l = uC u R l * uC u R k) (k l : Fin K) :
    u k * u l = u l * u k := by
  have h1 : (Int.castRingHom R).mapMatrix (u k * u l) = (Int.castRingHom R).mapMatrix (u l * u k) := by
    rw [map_mul, map_mul]
    exact h k l
  exact Matrix.map_injective (RingHom.injective_int (Int.castRingHom R)) h1

omit [CharZero R] in

theorem uC_comm_of_TC_comm (hmem : ∀ k, uC u R k ∈ Algebra.adjoin R (Set.range (TC T R)))
    (hT : ∀ g h : G, TC T R g * TC T R h = TC T R h * TC T R g) (k l : Fin K) :
    uC u R k * uC u R l = uC u R l * uC u R k := by
  have hgen : ∀ a ∈ Set.range (TC T R), ∀ b ∈ Set.range (TC T R), Commute a b := by
    rintro _ ⟨g, rfl⟩ _ ⟨h, rfl⟩
    exact hT g h
  have h1 : ∀ b ∈ Set.range (TC T R), Commute (uC u R k) b := fun b hb =>
    (Algebra.commute_of_mem_adjoin_of_forall_mem_commute (hmem k) fun a ha => hgen b hb a ha).symm
  exact (Algebra.commute_of_mem_adjoin_of_forall_mem_commute (hmem l) h1).eq

end Descent

section Basis

variable (R : Type*) [CommRing R]
variable (huind : LinearIndependent R (fun k : Fin K => (u k).map (Int.castRingHom R)))
  (huspan : Submodule.span R (Set.range fun k : Fin K => (u k).map (Int.castRingHom R)) =
    Subalgebra.toSubmodule (Algebra.adjoin R (Set.range fun g : G => (T g).map (Int.castRingHom R))))

abbrev AR : Subalgebra R (Matrix (Fin n) (Fin n) R) := Algebra.adjoin R (Set.range (TC T R))

include huspan in
theorem uC_mem (k : Fin K) : uC u R k ∈ AR T R := by
  have : uC u R k ∈ Submodule.span R (Set.range fun k : Fin K => (u k).map (Int.castRingHom R)) :=
    Submodule.subset_span ⟨k, rfl⟩
  rw [huspan] at this
  exact this

def uA (k : Fin K) : ↥(AR T R) := ⟨uC u R k, uC_mem T u R huspan k⟩

include huind in
theorem linearIndependent_uA : LinearIndependent R (uA T u R huspan) := by
  apply LinearIndependent.of_comp (AR T R).val.toLinearMap
  exact huind

theorem span_uA : ⊤ ≤ Submodule.span R (Set.range (uA T u R huspan)) := by
  rintro ⟨x, hx⟩ -
  have hx' : x ∈ Submodule.span R (Set.range fun k : Fin K => (u k).map (Int.castRingHom R)) := by
    rw [huspan]; exact hx
  have hinj : Function.Injective ((AR T R).val.toLinearMap) := Subtype.val_injective
  rw [← Submodule.apply_mem_span_image_iff_mem_span hinj, ← Set.range_comp]
  exact hx'

def basisA : Module.Basis (Fin K) R ↥(AR T R) :=
  Module.Basis.mk (linearIndependent_uA T u R huind huspan) (span_uA T u R huspan)

@[simp] theorem coe_basisA (k : Fin K) :
    ((basisA T u R huind huspan k : ↥(AR T R)) : Matrix (Fin n) (Fin n) R) = uC u R k := by
  rw [basisA, Module.Basis.coe_mk]; rfl

def crd : ↥(AR T R) →ₗ[R] (Fin K → R) := (basisA T u R huind huspan).equivFun.toLinearMap

theorem crd_apply (x : ↥(AR T R)) : crd T u R huind huspan x = (basisA T u R huind huspan).equivFun x := rfl

theorem elemM_crd (x : ↥(AR T R)) : elemM u R (crd T u R huind huspan x) = (x : Matrix (Fin n) (Fin n) R) := by
  have h := (basisA T u R huind huspan).sum_equivFun x
  have h' := congrArg Subtype.val h
  rw [AddSubmonoidClass.coe_finsetSum] at h'
  rw [← h', elemM]
  refine Finset.sum_congr rfl fun k _ => ?_
  rw [Subalgebra.coe_smul, coe_basisA]
  rfl

theorem crd_eq_of_elemM_eq (x : ↥(AR T R)) (a : Fin K → R)
    (h : (x : Matrix (Fin n) (Fin n) R) = elemM u R a) : crd T u R huind huspan x = a := by
  have hx : x = ∑ k, a k • basisA T u R huind huspan k := by
    apply Subtype.ext
    rw [AddSubmonoidClass.coe_finsetSum, h, elemM]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Subalgebra.coe_smul, coe_basisA]
  rw [crd_apply, hx]
  funext k
  rw [map_sum, Finset.sum_apply, Finset.sum_eq_single k]
  · rw [map_smul, Pi.smul_apply, (basisA T u R huind huspan).equivFun_self, if_pos rfl, smul_eq_mul, mul_one]
  · intro l _ hl
    rw [map_smul, Pi.smul_apply, (basisA T u R huind huspan).equivFun_self, if_neg hl, smul_zero]
  · intro hk; exact absurd (Finset.mem_univ k) hk

theorem crd_basisA (k : Fin K) : crd T u R huind huspan (basisA T u R huind huspan k) = Pi.single k 1 := by
  apply crd_eq_of_elemM_eq
  rw [elemM_single, coe_basisA]

variable (hu_mul : ∀ k l : Fin K, u k * u l = ∑ m, c k l m • u m) (hu_one : ∑ m, c₁ m • u m = 1)
  (hu_T : ∀ g : G, ∑ m, cT g m • u m = T g)

include hu_mul in

theorem crd_mul (x y : ↥(AR T R)) :
    crd T u R huind huspan (x * y) = cstar c R (crd T u R huind huspan x) (crd T u R huind huspan y) := by
  apply crd_eq_of_elemM_eq
  rw [elemM_cstar u c R hu_mul, elemM_crd, elemM_crd, Subalgebra.coe_mul]

include hu_one in
theorem crd_one : crd T u R huind huspan 1 = fun m => (c₁ m : R) := by
  apply crd_eq_of_elemM_eq
  rw [elemM_c₁ u c₁ R hu_one, Subalgebra.coe_one]

include hu_T in
theorem crd_TC (g : G) (hg : TC T R g ∈ AR T R) :
    crd T u R huind huspan ⟨TC T R g, hg⟩ = fun m => (cT g m : R) := by
  apply crd_eq_of_elemM_eq
  rw [elemM_cT T u cT R hu_T]

end Basis

end IntMatrixOrder

end