diff --git a/src/linear_algebra/my_ips/frob.lean b/src/linear_algebra/my_ips/frob.lean
index 91bd9c1756..7441920c1e 100644
--- a/src/linear_algebra/my_ips/frob.lean
+++ b/src/linear_algebra/my_ips/frob.lean
@@ -201,6 +201,10 @@ noncomputable def matrix_direct_sum_from_to (i j : k) :
   (matrix (s i) (s i) ℂ) →ₗ[ℂ] (matrix (s j) (s j) ℂ) :=
 @direct_sum_from_to ℂ _ k _ (λ a, matrix (s a) (s a) ℂ) _ (λ a, matrix.module) i j
 
+lemma matrix_direct_sum_from_to_same (i : k) :
+  (matrix_direct_sum_from_to i i : matrix (s i) (s i) ℂ →ₗ[ℂ] _) = 1 :=
+direct_sum_from_to_apply_same _
+
 lemma linear_map.pi_mul'_apply_include_block' {i j : k} :
   (linear_map.mul' ℂ ℍ₂) ∘ₗ
     (tensor_product.map (include_block : (ℍ_ i) →ₗ[ℂ] ℍ₂) (include_block : (ℍ_ j) →ₗ[ℂ] ℍ₂))
@@ -295,104 +299,70 @@ begin
     { refl, }, },
 end
 
--- lemma pi_frobenius_equation [hθ : Π i, fact (θ i).is_faithful_pos_map]
---   {i j : k} (x y : ℍ₂) :
+lemma direct_sum_tensor_to_kronecker_apply
+  (x y : ℍ₂) (r : k × k) (a b : s r.1 × s r.2) :
+  (direct_sum_tensor_to_kronecker (x ⊗ₜ[ℂ] y))
+  r a b
+  = x r.1 a.1 b.1 * y r.2 a.2 b.2 :=
+begin
+  simp_rw [direct_sum_tensor_to_kronecker,
+    linear_equiv.coe_mk, direct_sum_tensor_matrix, direct_sum_tensor_apply,
+    tensor_product.to_kronecker_apply, kronecker_map, of_apply],
+end
+
+-- lemma pi_frobenius_equation [hθ : Π i, fact (θ i).is_faithful_pos_map] :
 --   ((linear_map.mul' ℂ ℍ₂  ⊗ₘ (1 : l(ℍ₂)))
 --     ∘ₗ ↑(tensor_product.assoc ℂ ℍ₂ ℍ₂ ℍ₂).symm
 --       ∘ₗ ((1 : l(ℍ₂)) ⊗ₘ ((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] (ℍ₂ ⊗[ℂ] ℍ₂))))
---         (include_block (x i) ⊗ₜ[ℂ] include_block (y j))
---     = (((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂) ∘ₗ (linear_map.mul' ℂ ℍ₂ : ℍ₂ ⊗[ℂ] ℍ₂ →ₗ[ℂ] ℍ₂))
---       (include_block (x i) ⊗ₜ[ℂ] include_block (y j)) :=
+--     = (((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂) ∘ₗ (linear_map.mul' ℂ ℍ₂ : ℍ₂ ⊗[ℂ] ℍ₂ →ₗ[ℂ] ℍ₂)) :=
 -- begin
---   -- letI := λ a, (hθ a).normed_add_comm_group,
---   -- letI := λ a, (hθ a).inner_product_space,
---   have := calc
+--   apply tensor_product.ext',
+--   intros x y,
+--   rw [← sum_include_block x, ← sum_include_block y],
+--   calc
 --   ((linear_map.mul' ℂ ℍ₂ ⊗ₘ (1 : l(ℍ₂)))
---     ∘ₗ (tensor_product.assoc ℂ ℍ₂ ℍ₂ ℍ₂).symm.to_linear_map
+--     ∘ₗ ↑(tensor_product.assoc ℂ ℍ₂ ℍ₂ ℍ₂).symm
 --       ∘ₗ ((1 : l(ℍ₂)) ⊗ₘ ((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] (ℍ₂ ⊗[ℂ] ℍ₂))))
---         (include_block (x i) ⊗ₜ[ℂ] include_block (y j))
---     =
---     (linear_map.mul' ℂ ℍ₂ ⊗ₘ (1 : l(ℍ₂)))
---       ((tensor_product.assoc ℂ ℍ₂ ℍ₂ ℍ₂).symm
---       ((include_block ⊗ₘ (include_block ⊗ₘ include_block))
---       (x i ⊗ₜ[ℂ] (linear_map.mul' ℂ (ℍ_ j)).adjoint (y j)))) : _
---   ... = (linear_map.mul' ℂ ℍ₂ ⊗ₘ (1 : l(ℍ₂)))
---       (((include_block ⊗ₘ include_block) ⊗ₘ include_block)
---       ((tensor_product.assoc ℂ (ℍ_ i) (ℍ_ j) (ℍ_ j)).symm
---       (x i ⊗ₜ[ℂ] (linear_map.mul' ℂ (ℍ_ j)).adjoint (y j)))) : _
---   ... = if (i = j) then (
---       (((include_block : (ℍ_ j) →ₗ[ℂ] ℍ₂) ⊗ₘ include_block) ∘ₗ
---       ((linear_map.mul' ℂ (ℍ_ j) ⊗ₘ (1 : l(ℍ_ j)))
---        ∘ₗ ↑(tensor_product.assoc ℂ (ℍ_ j) (ℍ_ j) (ℍ_ j)).symm
---        ∘ₗ ((1 : l(ℍ_ j)) ⊗ₘ (linear_map.mul' ℂ (ℍ_ j)).adjoint)))
---         (x j ⊗ₜ[ℂ] y j)) else 0 : _,
---   -- ... = if (i = j) then (
---   --     ((include_block ⊗ₘ include_block) ∘ₗ
---   --       ((linear_map.mul' ℂ (ℍ_ j)).adjoint ∘ₗ (linear_map.mul' ℂ (ℍ_ j)))) (x j ⊗ₜ[ℂ] y j)) else 0 : _,
---   -- ... = if (i = j) then (
---   --     (include_block ⊗ₘ include_block)
---   --     ((linear_map.mul' ℂ (ℍ_ j)).adjoint
---   --     ((linear_map.mul' ℂ (ℍ_ j)) (x j ⊗ₜ[ℂ] y j)))) else 0 : _,
---   { rw [linear_equiv.to_linear_map_eq_coe] at this,
---     simp_rw [frobenius_equation], }
---   -- ... = (M ⊗ₘ (1 : l(ℍ₂)))
---   --     (((include_block ⊗ₘ include_block) ⊗ₘ include_block)
---   --     ((tensor_product.assoc ℂ (ℍ_ i) (ℍ_ j) (ℍ_ j)).symm
---   --     (x ⊗ₜ[ℂ] (linear_map.mul' ℂ (ℍ_ j)).adjoint y))) : _
---   -- ... = (M ∘ₗ (include_block ⊗ₘ include_block) ⊗ₘ include_block)
---   --     ((tensor_product.assoc ℂ (ℍ_ i) (ℍ_ j) (ℍ_ j)).symm
---   --     (x ⊗ₜ[ℂ] (linear_map.mul' ℂ (ℍ_ j)).adjoint y)) : _
---   -- ... = 0 : _,
---   -- rw ← (direct_sum_tensor_to_kronecker : ℍ₂ ⊗[ℂ] ℍ₂ ≃ₗ[ℂ] Π i : (k × k), matrix (s i.fst × s i.snd) (s i.fst × s i.snd) ℂ).injective.eq_iff,
---   -- ext1 a,
---   -- ext1 b c,
---   -- simp_rw [linear_map.comp_apply, tensor_product.map_tmul, linear_map.mul'_adjoint_single_block,
---   --   linear_map.mul'_adjoint, map_sum, smul_hom_class.map_smul, tensor_product.tmul_sum,
---   --   tensor_product.tmul_smul, map_sum, smul_hom_class.map_smul, linear_equiv.coe_coe,
---   --   tensor_product.map_tmul, tensor_product.assoc_symm_tmul, tensor_product.map_tmul,
---   --   linear_map.one_apply, linear_map.mul'_apply, include_block_mul_include_block,
---   --   direct_sum_tensor_to_kronecker, linear_equiv.coe_mk, direct_sum_tensor_matrix,
---   --   direct_sum_tensor_apply, tensor_product.to_kronecker_apply,
---   --   finset.sum_apply, pi.smul_apply, kronecker_map, of_apply,
---   --   dite_apply, dite_mul, pi.zero_apply, zero_mul, smul_dite, smul_zero,include_block_apply_std_basis_matrix, include_block_apply,
---   --   block_diag'_apply, dite_apply, dite_mul, pi.zero_apply, zero_mul,
---   --   linear_map.apply_dite, map_zero, direct_sum_tensor, linear_equiv.coe_mk,
---   --   linear_map.apply_dite, dite_apply, map_zero, pi.zero_apply, linear_map.apply_dite,
---   --   map_zero, dite_apply, pi.zero_apply, finset.sum_dite_irrel, finset.sum_const_zero],
---   -- congr,
---   -- ext1 h,
---   -- simp only [h, linear_map.mul'_adjoint_single_block, smul_dite, smul_zero,
---   --   finset.sum_dite_irrel, finset.sum_const_zero, std_basis_matrix],
---   -- by_cases j = i,
---   -- { simp only [h, eq_self_iff_true, dif_pos, linear_map.mul'_adjoint_single_block,
---   --     linear_map.mul'_adjoint, map_sum, smul_hom_class.map_smul, pi.smul_apply,
---   --     finset.sum_apply, tensor_product.map_tmul, direct_sum_tensor_apply,
---   --     tensor_product.to_kronecker_apply, kronecker_map, of_apply,
---   --     include_block_apply_std_basis_matrix],
---   --   simp only [std_basis_matrix, block_diag'_apply, mul_ite, mul_one, mul_zero,
---   --     ite_mul, one_mul, zero_mul, smul_ite, smul_zero, smul_dite, mul_dite, dite_mul],
---   --   simp only [finset.sum_dite_irrel, finset.sum_const_zero, finset.sum_ite_irrel,
---   --     ite_and, sigma.mk.inj_iff, finset.sum_ite_eq', finset.sum_ite_eq, finset.sum_dite_eq,
---   --     finset.sum_dite_eq', finset.mem_univ, if_true],
---   --   split_ifs; simp [h_1, h],
---   --   apply finset.sum_congr rfl,
---   --   intros h_2,
---   --   split_ifs;
---   --   simp [h_3], }
-
---   -- rw [matrix_eq_sum_include_block x, matrix_eq_sum_include_block y],
---   -- simp only [tensor_product.sum_tmul, tensor_product.tmul_sum, map_sum,
---   -- simp_rw [← linear_map.comp_apply, ← tensor_product.map_tmul, linear_map.mul'_adjoint_single_block hθ],
---   --   linear_map.one_apply],
---   -- simp_rw [← tensor_product.map_tmul, ← linear_map.comp_apply,
---   --   ← linear_equiv.to_linear_map_eq_coe, tensor_product.assoc_symm_comp_map,
---   --   ← linear_map.comp_assoc, ← tensor_product.map_comp],
-
---   -- have := calc ∑ (x_1 x_2 : k), ((((linear_map.mul' ℂ ℍ₂).comp (include_block ⊗ₘ include_block)) ⊗ₘ include_block).comp
---   --   (tensor_product.assoc ℂ (ℍ_ x_2) (ℍ_ x_1) (ℍ_ x_1).symm.to_linear_map))
---   --   (x x_2 ⊗ₜ[ℂ] (m_ x_1 ⋆) (y x_1))
---   --   = 0 : _,
---   -- rw [linear_map.mul'_direct_sum_apply_include_block'],
+--         ((∑ i, include_block (x i)) ⊗ₜ[ℂ] (∑ j, include_block (y j)))
+--   =
+--   ∑ i j, if (i = j) then (
+--       ((include_block ⊗ₘ include_block) ∘ₗ
+--         ((linear_map.mul' ℂ (ℍ_ j)).adjoint ∘ₗ (linear_map.mul' ℂ (ℍ_ j))))
+--         ((x j) ⊗ₜ[ℂ] (y j))) else 0 :
+--   by { simp_rw [tensor_product.sum_tmul, tensor_product.tmul_sum, map_sum],
+--     repeat { apply finset.sum_congr rfl, intros },
+--     rw [frobenius_equation_direct_sum_aux], }
+--   ... =
+--   ∑ j, ((include_block ⊗ₘ include_block)
+--       ((linear_map.mul' ℂ (ℍ_ j)).adjoint
+--       ((linear_map.mul' ℂ (ℍ_ j))
+--       ((x j) ⊗ₜ[ℂ] (y j))))) :
+--   by { simp_rw [finset.sum_ite_eq, finset.mem_univ, if_true,
+--     linear_map.comp_apply], }
+--   ... =
+--   ∑ j, (((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂)
+--     ∘ₗ (include_block ∘ₗ (linear_map.mul' ℂ (ℍ_ j))))
+--       ((x j) ⊗ₜ[ℂ] (y j)) :
+--   by { simp_rw [linear_map.comp_apply, linear_map.pi_mul'_adjoint_single_block], }
+--   ... =
+--   ∑ i j, ite (i = j)
+--   ((((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂) ∘ₗ
+--   (include_block.comp ((linear_map.mul' ℂ (matrix (s j) (s j) ℂ)).comp (matrix_direct_sum_from_to i j ⊗ₘ 1))))
+--      (x i ⊗ₜ[ℂ] y j)
+--   )
+--    0 :
+--   by { simp_rw [finset.sum_ite_eq, finset.mem_univ, if_true,
+--     matrix_direct_sum_from_to_same, tensor_product.map_one, linear_map.comp_one], }
+--   ... =
+--   ∑ j, (((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂)
+--     ((linear_map.mul' ℂ ℍ₂ : ℍ₂ ⊗[ℂ] ℍ₂ →ₗ[ℂ] ℍ₂)
+--      (include_block (x j) ⊗ₜ[ℂ] include_block (y j)))) :
+--   by { simp_rw [← linear_map.pi_mul'_apply_include_block'], }
+--   ... =
+--   (((linear_map.mul' ℂ ℍ₂).adjoint : ℍ₂ →ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂) ∘ₗ (linear_map.mul' ℂ ℍ₂ : ℍ₂ ⊗[ℂ] ℍ₂ →ₗ[ℂ] ℍ₂))
+--   ((∑ i, include_block (x i)) ⊗ₜ[ℂ] (∑ j, include_block (y j))) :
+--   by {  },
+
 -- end
 
 lemma frobenius_equation' [hφ : fact φ.is_faithful_pos_map] :
diff --git a/src/linear_algebra/my_ips/nontracial.lean b/src/linear_algebra/my_ips/nontracial.lean
index 689af78f4e..9603b77d99 100644
--- a/src/linear_algebra/my_ips/nontracial.lean
+++ b/src/linear_algebra/my_ips/nontracial.lean
@@ -1182,9 +1182,31 @@ begin
   intros i,
   apply_instance,
 end
-private def f₁_equiv :
-  (ℍ₂ ⊗[ℂ] ℍ₂ᵐᵒᵖ) ≃ₗ[ℂ] ℍ₂ ⊗[ℂ] ℍ₂ :=
-linear_equiv.tensor_product.map (1 : ℍ₂ ≃ₗ[ℂ] ℍ₂) (mul_opposite.op_linear_equiv ℂ).symm
+
+@[simps] def pi.transpose_alg_equiv (p : Type*) [fintype p] [decidable_eq p]
+  (n : p → Type*) [Π i, fintype (n i)] [Π i, decidable_eq (n i)] :
+  (Π i, matrix (n i) (n i) ℂ) ≃ₐ[ℂ] (Π i, matrix (n i) (n i) ℂ)ᵐᵒᵖ :=
+{ to_fun := λ A, mul_opposite.op (λ i, (A i)ᵀ),
+  inv_fun := λ A, (λ i, (mul_opposite.unop A i)ᵀ),
+  left_inv := λ A, by
+  { simp only [mul_opposite.unop_op, transpose_transpose], },
+  right_inv := λ A, by
+  { simp only [mul_opposite.op_unop, transpose_transpose], },
+  map_add' := λ A B, by
+  { simp only [pi.add_apply, transpose_add],
+    refl, },
+  map_mul' := λ A B, by
+  { simp only [pi.mul_apply, mul_eq_mul, transpose_mul, ← mul_opposite.op_mul],
+    refl, },
+  commutes' := λ c, by
+  { simp only [algebra.algebra_map_eq_smul_one, pi.smul_apply, pi.one_apply,
+      transpose_smul, transpose_one],
+    refl, }, }
+
+lemma pi.transpose_alg_equiv_symm_op_apply (A : Π i, matrix (s i) (s i) ℂ) :
+  (pi.transpose_alg_equiv k s).symm (mul_opposite.op A) = λ i, (A i)ᵀ :=
+rfl
+
 private def f₂_equiv :
   ℍ₂ ⊗[ℂ] ℍ₂ ≃ₐ[ℂ] Π i : k × k, (matrix (s i.1) (s i.1) ℂ ⊗[ℂ] matrix (s i.2) (s i.2) ℂ) :=
 begin
@@ -1207,15 +1229,14 @@ private def f₄_equiv :
     // x.is_block_diagonal } :=
 is_block_diagonal_pi_alg_equiv.symm
 
+def tensor_product_mul_op_equiv :
+  (ℍ₂ ⊗[ℂ] ℍ₂ᵐᵒᵖ) ≃ₐ[ℂ]
+  Π i : k × k, matrix (s i.1 × s i.2) (s i.1 × s i.2) ℂ :=
+(alg_equiv.tensor_product.map
+  (1 : ℍ₂ ≃ₐ[ℂ] ℍ₂) (pi.transpose_alg_equiv k s : ℍ₂ ≃ₐ[ℂ] ℍ₂ᵐᵒᵖ).symm).trans
+  (f₂_equiv.trans (f₃_equiv))
+
 
-private def f₅_equiv :
-  (ℍ₂ ⊗[ℂ] ℍ₂ᵐᵒᵖ)
-    ≃ₗ[ℂ] { x : matrix (Σ i : k × k, s i.1 × s i.2) (Σ i : k × k, s i.1 × s i.2) ℂ
-      // x.is_block_diagonal } :=
-begin
-  let : ℍ₂ ⊗[ℂ] ℍ₂ ≃ₐ[ℂ] _ := f₂_equiv.trans (f₃_equiv.trans f₄_equiv),
-  exact f₁_equiv.trans this.to_linear_equiv,
-end
 
 noncomputable def module.dual.pi.is_faithful_pos_map.Psi_inv_fun'
   (hψ : Π i, fact (ψ i).is_faithful_pos_map) (t r : ℝ) :
diff --git a/src/quantum_graph/example.lean b/src/quantum_graph/example.lean
index b397dacdf7..fd46020213 100644
--- a/src/quantum_graph/example.lean
+++ b/src/quantum_graph/example.lean
@@ -15,49 +15,53 @@ import quantum_graph.nontracial
 open tensor_product matrix
 open_locale tensor_product big_operators kronecker matrix functional
 
-variables {p n : Type*} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p]
-local notation `ℍ` := matrix n n ℂ
-local notation `⊗K` := matrix (n × n) (n × n) ℂ
+variables {p : Type*} [fintype p] [decidable_eq p] {n : p → Type*}
+  [Π i, fintype (n i)] [Π i, decidable_eq (n i)]
+local notation `ℍ` := Π i, matrix (n i) (n i) ℂ
+local notation `ℍ_`i := matrix (n i) (n i) ℂ
+-- local notation `⊗K` := matrix (n × n) (n × n) ℂ
 local notation `l(` x `)` := x →ₗ[ℂ] x
 
-variables {φ : module.dual ℂ ℍ} [hφ : fact φ.is_faithful_pos_map]
-  {ψ : module.dual ℂ (matrix p p ℂ)} (hψ : ψ.is_faithful_pos_map)
+variables {φ : Π i, module.dual ℂ (ℍ_ i)} [hφ : Π i, fact (φ i).is_faithful_pos_map]
 
 local notation `|` x `⟩⟨` y `|` := @rank_one ℂ _ _ _ _ x y
 local notation `m` := linear_map.mul' ℂ ℍ
 local notation `η` := algebra.linear_map ℂ ℍ
 local notation x ` ⊗ₘ ` y := tensor_product.map x y
 local notation `υ` :=
-  ((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ))
-    : (matrix n n ℂ ⊗[ℂ] matrix n n ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ]
-      matrix n n ℂ ⊗[ℂ] (matrix n n ℂ ⊗[ℂ] matrix n n ℂ))
+  ((tensor_product.assoc ℂ ℍ ℍ ℍ)
+    : (ℍ ⊗[ℂ] ℍ ⊗[ℂ] ℍ) →ₗ[ℂ]
+      ℍ ⊗[ℂ] (ℍ ⊗[ℂ] ℍ))
 local notation `υ⁻¹` :=
-  ((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).symm
-    : matrix n n ℂ ⊗[ℂ] (matrix n n ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ]
-      (matrix n n ℂ ⊗[ℂ] matrix n n ℂ ⊗[ℂ] matrix n n ℂ))
-local notation `ϰ` := (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ)
-  : (matrix n n ℂ ⊗[ℂ] ℂ) →ₗ[ℂ] (ℂ ⊗[ℂ] matrix n n ℂ))
-local notation `ϰ⁻¹` := ((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm
-  : (ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ] (matrix n n ℂ ⊗[ℂ] ℂ))
-local notation `τ` := ((tensor_product.lid ℂ (matrix n n ℂ))
-  : (ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ] matrix n n ℂ)
-local notation `τ⁻¹` := ((tensor_product.lid ℂ (matrix n n ℂ)).symm
-  : matrix n n ℂ →ₗ[ℂ] (ℂ ⊗[ℂ] matrix n n ℂ))
-local notation `id` := (1 : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
-
-noncomputable def qam.complete_graph (hφ : φ.is_faithful_pos_map) :
-  ℍ →ₗ[ℂ] ℍ :=
-begin
-  letI := fact.mk hφ,
-  exact |(1 : ℍ)⟩⟨(1 : ℍ)|,
-end
-
-lemma qam.complete_graph_eq :
-  qam.complete_graph hφ.elim = |(1 : ℍ)⟩⟨(1 : ℍ)| :=
+  ((tensor_product.assoc ℂ ℍ ℍ ℍ).symm
+    : ℍ ⊗[ℂ] (ℍ ⊗[ℂ] ℍ) →ₗ[ℂ]
+      (ℍ ⊗[ℂ] ℍ ⊗[ℂ] ℍ))
+local notation `ϰ` := (↑(tensor_product.comm ℂ ℍ ℂ)
+  : (ℍ ⊗[ℂ] ℂ) →ₗ[ℂ] (ℂ ⊗[ℂ] ℍ))
+local notation `ϰ⁻¹` := ((tensor_product.comm ℂ ℍ ℂ).symm
+  : (ℂ ⊗[ℂ] ℍ) →ₗ[ℂ] (ℍ ⊗[ℂ] ℂ))
+local notation `τ` := ((tensor_product.lid ℂ ℍ)
+  : (ℂ ⊗[ℂ] ℍ) →ₗ[ℂ] ℍ)
+local notation `τ⁻¹` := ((tensor_product.lid ℂ ℍ).symm
+  : ℍ →ₗ[ℂ] (ℂ ⊗[ℂ] ℍ))
+local notation `id` := (1 : ℍ →ₗ[ℂ] ℍ)
+
+noncomputable def qam.complete_graph
+  (E : Type*) [has_one E] [normed_add_comm_group E] [inner_product_space ℂ E] :
+  E →ₗ[ℂ] E :=
+|(1 : E)⟩⟨(1 : E)|
+
+lemma qam.complete_graph_eq {E : Type*} [has_one E]
+  [normed_add_comm_group E] [inner_product_space ℂ E] :
+  qam.complete_graph E = (|(1 : E)⟩⟨(1 : E)|) :=
 rfl
 
-lemma qam.complete_graph_eq' :
-  qam.complete_graph hφ.elim = η ∘ₗ (η).adjoint :=
+
+lemma qam.complete_graph_eq' {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map] :
+  qam.complete_graph (matrix p p ℂ)
+    = (algebra.linear_map ℂ (matrix p p ℂ))
+      ∘ₗ (algebra.linear_map ℂ (matrix p p ℂ)).adjoint :=
 begin
   rw [linear_map.ext_iff],
   intros x,
@@ -67,146 +71,371 @@ begin
   refl,
 end
 
-lemma qam.nontracial.complete_graph.qam :
-  qam φ (qam.complete_graph hφ.elim) :=
+
+lemma pi.qam.complete_graph_eq' [hφ : Π i, fact (φ i).is_faithful_pos_map] :
+  qam.complete_graph ℍ
+    = (η) ∘ₗ (η).adjoint :=
 begin
-  rw [qam.complete_graph, qam, qam.rank_one.refl_idempotent_eq],
-  simp_rw matrix.one_mul,
+  rw [linear_map.ext_iff],
+  intros x,
+  simp_rw [qam.complete_graph_eq, continuous_linear_map.coe_coe, linear_map.comp_apply,
+    rank_one_apply, nontracial.pi.unit_adjoint_eq, module.dual.pi.is_faithful_pos_map.inner_eq, star_one, one_mul],
+  refl,
 end
-lemma qam.nontracial.complete_graph.is_self_adjoint :
-  @qam.is_self_adjoint n _ _ φ _ (qam.complete_graph hφ.elim) :=
+
+lemma qam.nontracial.complete_graph.qam {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] :
+  schur_idempotent (qam.complete_graph E) (qam.complete_graph E) = (qam.complete_graph E) :=
 begin
-  simp_rw [qam.is_self_adjoint, qam.complete_graph,
+  rw [qam.complete_graph, schur_idempotent.apply_rank_one, one_mul],
+end
+lemma qam.nontracial.complete_graph.is_self_adjoint
+  {E : Type*} [has_one E] [normed_add_comm_group E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E] :
+  @_root_.is_self_adjoint _ _ (qam.complete_graph E) :=
+begin
+  simp_rw [_root_.is_self_adjoint, qam.complete_graph, linear_map.star_eq_adjoint,
     ← rank_one_lm_eq_rank_one, rank_one_lm_adjoint],
 end
-lemma qam.nontracial.complete_graph.is_real :
-  (qam.complete_graph hφ.elim).is_real :=
+lemma qam.nontracial.complete_graph.is_real
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map] :
+  (qam.complete_graph (matrix p p ℂ)).is_real :=
 begin
-  simp_rw [linear_map.is_real_iff, qam.complete_graph, rank_one_real_apply,
+  rw [qam.complete_graph, linear_map.is_real_iff, rank_one_real_apply,
     conj_transpose_one, _root_.map_one],
 end
-lemma qam.nontracial.complete_graph.is_symm :
-  linear_equiv.symm_map ℂ ℍ (qam.complete_graph hφ.elim) = qam.complete_graph hφ.elim :=
-by { simp_rw [qam.complete_graph, qam.rank_one.symmetric_eq, conj_transpose_one, _root_.map_one], }
-
-lemma qam.nontracial.complete_graph.is_reflexive :
-  @qam_lm_nontracial_is_reflexive _ _ _ φ _ (qam.complete_graph hφ.elim) :=
+lemma qam.nontracial.complete_graph.is_symm
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map] :
+  linear_equiv.symm_map ℂ (matrix p p ℂ) (qam.complete_graph (matrix p p ℂ))
+    = qam.complete_graph (matrix p p ℂ) :=
+by simp_rw [qam.complete_graph, qam.rank_one.symmetric_eq, conj_transpose_one, _root_.map_one]
+lemma pi.qam.nontracial.complete_graph.is_real
+  [hφ : Π i, fact (φ i).is_faithful_pos_map] :
+  (qam.complete_graph ℍ).is_real :=
 begin
-  obtain ⟨α, β, hαβ⟩ := (1 : l(ℍ)).exists_sum_rank_one,
-  rw [qam_lm_nontracial_is_reflexive],
+  rw [qam.complete_graph, ← rank_one_lm_eq_rank_one,
+    linear_map.is_real_iff, pi.rank_one_lm_real_apply,
+    star_one, _root_.map_one],
+end
+lemma pi.qam.nontracial.complete_graph.is_symm
+  [hφ : Π i, fact (φ i).is_faithful_pos_map] :
+  linear_equiv.symm_map ℂ ℍ (qam.complete_graph ℍ) = qam.complete_graph ℍ :=
+by simp_rw [qam.complete_graph, linear_equiv.symm_map_rank_one_apply, star_one, _root_.map_one]
+
+lemma qam.nontracial.complete_graph.is_reflexive
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] :
+  schur_idempotent (qam.complete_graph E) 1 = 1 :=
+begin
+  obtain ⟨α, β, hαβ⟩ := (1 : l(E)).exists_sum_rank_one,
   nth_rewrite_lhs 0 hαβ,
-  simp_rw [map_sum, qam.complete_graph, qam.rank_one.refl_idempotent_eq, matrix.one_mul, ← hαβ],
+  simp_rw [map_sum, qam.complete_graph, schur_idempotent.apply_rank_one, one_mul, ← hαβ],
+end
+
+lemma linear_map.mul'_comp_mul'_adjoint_of_delta_form
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  {δ : ℂ} [hφ : fact φ.is_faithful_pos_map]
+  (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  linear_map.mul' ℂ (matrix p p ℂ) ∘ₗ (linear_map.mul' ℂ (matrix p p ℂ)).adjoint = δ • 1 :=
+begin
+  rw [qam.nontracial.mul_comp_mul_adjoint, hφ₂],
+end
+
+lemma linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  m ∘ₗ (m).adjoint = δ • id :=
+begin
+  rw [linear_map.pi_mul'_comp_mul'_adjoint_eq_smul_id_iff δ],
+  exact hφ₂,
+  exact _inst_5,
+end
+
+lemma qam.nontracial.delta_ne_zero
+  [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)}
+  {δ : ℂ} [hφ : fact φ.is_faithful_pos_map]
+  (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  δ ≠ 0 :=
+begin
+  rw ← hφ₂,
+  exact matrix.pos_def.trace_ne_zero (pos_def.inv hφ.elim.matrix_is_pos_def),
+end
+
+lemma pi.qam.nontracial.delta_ne_zero
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  δ ≠ 0 :=
+begin
+  have : ∀ i, (φ i).matrix⁻¹.trace ≠ 0,
+  { intro i,
+    exact matrix.pos_def.trace_ne_zero (pos_def.inv (hφ i).elim.matrix_is_pos_def), },
+  have this' : δ ≠ 0 ↔ ∀ i, (φ i).matrix⁻¹.trace ≠ 0,
+  { split; rintros h i,
+    { exact this _, },
+    { rw i at *,
+      let j : p := classical.arbitrary p,
+      exact (h j) (hφ₂ j), }, },
+  rw this',
+  exact this,
 end
 
 @[instance] noncomputable def qam.nontracial.mul'_comp_mul'_adjoint.invertible
-  [hφ : fact φ.is_faithful_pos_map]
-  [nontrivial n] :
-  invertible ((m ∘ₗ (m).adjoint) : ℍ →ₗ[ℂ] ℍ) :=
+  [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)}
+  {δ : ℂ} [hφ : fact φ.is_faithful_pos_map]
+  (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  @invertible (l(matrix p p ℂ)) {mul := (∘ₗ)} {one := 1}
+    (linear_map.mul' ℂ (matrix p p ℂ)
+      ∘ₗ (linear_map.mul' ℂ (matrix p p ℂ)).adjoint)
+     :=
 begin
-  rw qam.nontracial.mul_comp_mul_adjoint,
+  rw linear_map.mul'_comp_mul'_adjoint_of_delta_form hφ₂,
   apply is_unit.invertible,
   rw [linear_map.is_unit_iff_ker_eq_bot, linear_map.ker_smul _ _ _,
     linear_map.one_eq_id, linear_map.ker_id],
-  exact matrix.pos_def.trace_ne_zero (pos_def.inv hφ.elim.matrix_is_pos_def),
+  exact qam.nontracial.delta_ne_zero hφ₂,
+end
+@[instance] noncomputable def pi.qam.nontracial.mul'_comp_mul'_adjoint.invertible
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  @invertible (ℍ →ₗ[ℂ] ℍ) {mul := (∘ₗ)} {one := id}
+    (m ∘ₗ (m).adjoint)
+     :=
+begin
+  rw linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form hφ₂,
+  apply is_unit.invertible,
+  rw [linear_map.is_unit_iff_ker_eq_bot, linear_map.ker_smul _ _ _,
+    linear_map.one_eq_id, linear_map.ker_id],
+  exact pi.qam.nontracial.delta_ne_zero hφ₂,
+end
+
+noncomputable def qam.trivial_graph
+  [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)}
+  {δ : ℂ} (hφ : fact φ.is_faithful_pos_map)
+  (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  l(matrix p p ℂ) :=
+begin
+  letI := hφ,
+  letI := qam.nontracial.mul'_comp_mul'_adjoint.invertible hφ₂,
+  exact ⅟ (linear_map.mul' ℂ (matrix p p ℂ) ∘ₗ (linear_map.mul' ℂ (matrix p p ℂ)).adjoint),
 end
 
-noncomputable def qam.trivial_graph (hφ : φ.is_faithful_pos_map) [nontrivial n] :
+noncomputable def pi.qam.trivial_graph
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} (hφ : Π i, fact (φ i).is_faithful_pos_map)
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
   l(ℍ) :=
 begin
-  letI := fact.mk hφ,
+  letI := hφ,
+  letI := pi.qam.nontracial.mul'_comp_mul'_adjoint.invertible hφ₂,
   exact ⅟ (m ∘ₗ (m).adjoint),
 end
 
-lemma qam.trivial_graph_eq [nontrivial n] :
-  qam.trivial_graph hφ.elim = (φ.matrix⁻¹ : ℍ).trace⁻¹ • (1 : ℍ →ₗ[ℂ] ℍ) :=
+lemma qam.trivial_graph_eq
+  [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  qam.trivial_graph hφ hφ₂ = δ⁻¹ • (1 : l(matrix p p ℂ)) :=
 begin
-  haveI := @qam.nontracial.mul'_comp_mul'_adjoint.invertible n _ _ φ _ _,
+  haveI := @qam.nontracial.mul'_comp_mul'_adjoint.invertible p _ _ _ φ δ hφ hφ₂,
   simp_rw [qam.trivial_graph],
   apply inv_of_eq_right_inv,
-  rw [qam.nontracial.mul_comp_mul_adjoint, smul_mul_smul, one_mul, mul_inv_cancel, one_smul],
-  { exact matrix.pos_def.trace_ne_zero (pos_def.inv hφ.elim.matrix_is_pos_def), },
+  rw [linear_map.mul'_comp_mul'_adjoint_of_delta_form hφ₂, smul_mul_smul, one_mul, mul_inv_cancel, one_smul],
+  { exact qam.nontracial.delta_ne_zero hφ₂, },
+end
+
+lemma pi.qam.trivial_graph_eq
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  pi.qam.trivial_graph hφ hφ₂ = δ⁻¹ • (1 : ℍ →ₗ[ℂ] ℍ) :=
+begin
+  haveI := @pi.qam.nontracial.mul'_comp_mul'_adjoint.invertible p _ _ n _ _ φ _ _ δ _ hφ₂,
+  simp_rw [pi.qam.trivial_graph],
+  apply inv_of_eq_right_inv,
+  rw [linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form hφ₂, smul_mul_smul, one_mul, mul_inv_cancel, one_smul],
+  { exact pi.qam.nontracial.delta_ne_zero hφ₂, },
 end
 
-lemma qam.nontracial.trivial_graph.qam [nontrivial n] :
-  qam φ (qam.trivial_graph hφ.elim) :=
+lemma qam.nontracial.trivial_graph.qam
+  [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  schur_idempotent (qam.trivial_graph hφ hφ₂) (qam.trivial_graph hφ hφ₂)
+    = qam.trivial_graph hφ hφ₂ :=
 begin
   rw qam.trivial_graph_eq,
-  let hQ := hφ.elim.matrix_is_pos_def,
-  let Q := φ.matrix,
-  simp_rw [qam, smul_hom_class.map_smul, linear_map.smul_apply, qam.refl_idempotent,
-      smul_smul, schur_idempotent, linear_map.coe_mk, tensor_product.map_one, linear_map.one_eq_id,
-      linear_map.id_comp, qam.nontracial.mul_comp_mul_adjoint, smul_smul, mul_assoc],
-    rw [inv_mul_cancel _, mul_one, linear_map.one_eq_id],
-    exact matrix.pos_def.trace_ne_zero (pos_def.inv hφ.elim.matrix_is_pos_def),
-  -- { simp_rw [smul_hom_class.map_smul, qam.symm_one], },
+  let hQ := module.dual.is_faithful_pos_map.matrix_is_pos_def hφ.elim,
+  simp_rw [smul_hom_class.map_smul, linear_map.smul_apply,
+    smul_smul, schur_idempotent, linear_map.coe_mk, tensor_product.map_one, linear_map.one_eq_id,
+    linear_map.id_comp, linear_map.mul'_comp_mul'_adjoint_of_delta_form hφ₂, smul_smul, mul_assoc],
+  rw [inv_mul_cancel _, mul_one, linear_map.one_eq_id],
+  exact qam.nontracial.delta_ne_zero hφ₂,
+end
+
+lemma pi.qam.nontracial.trivial_graph.qam
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  schur_idempotent (pi.qam.trivial_graph hφ hφ₂) (pi.qam.trivial_graph hφ hφ₂)
+    = pi.qam.trivial_graph hφ hφ₂ :=
+begin
+  rw pi.qam.trivial_graph_eq,
+  let hQ := module.dual.pi.is_faithful_pos_map.matrix_is_pos_def hφ,
+  let Q := module.dual.pi.matrix_block φ,
+  simp_rw [smul_hom_class.map_smul, linear_map.smul_apply,
+    smul_smul, schur_idempotent, linear_map.coe_mk, tensor_product.map_one, linear_map.one_eq_id,
+    linear_map.id_comp, linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form hφ₂, smul_smul, mul_assoc],
+  rw [inv_mul_cancel _, mul_one, linear_map.one_eq_id],
+  exact pi.qam.nontracial.delta_ne_zero hφ₂,
 end
 
-lemma qam.nontracial.trivial_graph.qam.is_self_adjoint [nontrivial n] :
-  (qam.trivial_graph hφ.elim).adjoint = qam.trivial_graph hφ.elim :=
+lemma qam.nontracial.trivial_graph.qam.is_self_adjoint [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  (qam.trivial_graph hφ hφ₂).adjoint = qam.trivial_graph hφ hφ₂ :=
 begin
-  simp_rw [qam.trivial_graph_eq, linear_map.adjoint_smul],
-  have : (φ.matrix⁻¹.trace.re : ℂ) = φ.matrix⁻¹.trace,
-  { rw [← complex.conj_eq_iff_re, star_ring_end_apply, trace_star,
-      hφ.elim.matrix_is_pos_def.1.inv.eq], },
-  rw [← this, ← complex.of_real_inv, complex.conj_of_real, linear_map.adjoint_one],
+  simp_rw [qam.trivial_graph_eq, linear_map.adjoint_smul, linear_map.adjoint_one,
+    star_ring_end_apply, star_inv', ← star_ring_end_apply],
+  congr' 2,
+  rw [← hφ₂, star_ring_end_apply, trace_star, hφ.elim.matrix_is_pos_def.1.inv.eq],
 end
 
-lemma qam.nontracial.trivial_graph [nontrivial n] :
-  @qam_lm_nontracial_is_reflexive _ _ _ φ _ (qam.trivial_graph hφ.elim) :=
+lemma pi.qam.nontracial.trivial_graph.qam.is_self_adjoint
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  (pi.qam.trivial_graph hφ hφ₂).adjoint = pi.qam.trivial_graph hφ hφ₂ :=
 begin
-  rw [qam_lm_nontracial_is_reflexive, qam.trivial_graph_eq,
-    smul_hom_class.map_smul, linear_map.smul_apply],
-  simp_rw [qam.refl_idempotent, schur_idempotent, linear_map.coe_mk,
+  simp_rw [pi.qam.trivial_graph_eq, linear_map.adjoint_smul, linear_map.adjoint_one,
+    star_ring_end_apply, star_inv', ← star_ring_end_apply],
+  congr' 2,
+  have : ∀ i, ((φ i).matrix⁻¹.trace.re : ℂ) = (φ i).matrix⁻¹.trace,
+  { intro i,
+    rw [← complex.conj_eq_iff_re, star_ring_end_apply, trace_star,
+      (hφ i).elim.matrix_is_pos_def.1.inv.eq], },
+  simp_rw [hφ₂] at this,
+  rw [← this (nonempty.some _inst_5), complex.conj_of_real],
+end
+
+lemma qam.nontracial.trivial_graph [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  schur_idempotent (qam.trivial_graph hφ hφ₂) 1 = 1 :=
+begin
+  rw [qam.trivial_graph_eq, smul_hom_class.map_smul, linear_map.smul_apply],
+  simp_rw [schur_idempotent, linear_map.coe_mk,
     tensor_product.map_one, linear_map.one_eq_id,
-    linear_map.id_comp, qam.nontracial.mul_comp_mul_adjoint, smul_smul,
-    inv_mul_cancel (matrix.pos_def.trace_ne_zero (pos_def.inv hφ.elim.matrix_is_pos_def)), one_smul,
-    linear_map.one_eq_id],
+    linear_map.id_comp, linear_map.mul'_comp_mul'_adjoint_of_delta_form hφ₂, smul_smul,
+    inv_mul_cancel (qam.nontracial.delta_ne_zero hφ₂), one_smul, linear_map.one_eq_id],
 end
 
-private lemma qam.refl_idempotent_one_one :
-  qam.refl_idempotent hφ.elim (1 : l(ℍ)) (1 : l(ℍ)) = (φ.matrix⁻¹).trace • (1 : l(ℍ)) :=
+lemma pi.qam.nontracial.trivial_graph
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  schur_idempotent (pi.qam.trivial_graph hφ hφ₂) 1 = 1 :=
 begin
-  simp_rw [qam.refl_idempotent, schur_idempotent, linear_map.coe_mk,
-    tensor_product.map_one, linear_map.one_comp, qam.nontracial.mul_comp_mul_adjoint],
+  rw [pi.qam.trivial_graph_eq, smul_hom_class.map_smul, linear_map.smul_apply],
+  simp_rw [schur_idempotent, linear_map.coe_mk,
+    tensor_product.map_one, linear_map.one_eq_id,
+    linear_map.id_comp, linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form hφ₂, smul_smul,
+    inv_mul_cancel (pi.qam.nontracial.delta_ne_zero hφ₂), one_smul, linear_map.one_eq_id],
 end
 
-lemma qam.lm.nontracial.is_unreflexive_iff_reflexive_add_one [nontrivial n] (x : l(ℍ)) :
-  qam.refl_idempotent hφ.elim x 1 = 0
-    ↔ qam.refl_idempotent hφ.elim (((φ.matrix⁻¹ : ℍ).trace : ℂ)⁻¹ • (x + 1)) 1 = 1 :=
+lemma qam.refl_idempotent_one_one_of_delta [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  schur_idempotent (1 : l(matrix p p ℂ)) (1 : l(matrix p p ℂ)) = δ • (1 : l(matrix p p ℂ)) :=
 begin
-  simp_rw [smul_hom_class.map_smul, linear_map.smul_apply,
-    _root_.map_add, linear_map.add_apply, qam.refl_idempotent_one_one,
-    smul_add, smul_smul, ← complex.cpow_neg_one],
-  nth_rewrite 2 ← complex.cpow_one ((φ.matrix⁻¹ : ℍ).trace),
-  rw [← complex.cpow_add _ _ (@matrix.pos_def.trace_ne_zero n _ _ _ _ _ _ _
-      (pos_def.inv hφ.elim.matrix_is_pos_def)),
-    neg_add_self, complex.cpow_zero, one_smul, add_left_eq_self, complex.cpow_neg_one,
-    smul_eq_zero_iff_eq' (inv_ne_zero (@matrix.pos_def.trace_ne_zero n _ _ _ _ _ _ _
-      (pos_def.inv hφ.elim.matrix_is_pos_def)))],
+  simp_rw [schur_idempotent, linear_map.coe_mk,
+    tensor_product.map_one, linear_map.one_comp, linear_map.mul'_comp_mul'_adjoint_of_delta_form hφ₂],
 end
 
-lemma qam.refl_idempotent_complete_graph_left (x : l(ℍ)) :
-  qam.refl_idempotent hφ.elim (qam.complete_graph hφ.elim) x = x :=
+lemma pi.qam.refl_idempotent_one_one_of_delta
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  schur_idempotent (1 : l(ℍ)) (1 : l(ℍ)) = δ • (1 : l(ℍ)) :=
 begin
-  obtain ⟨α, β, rfl⟩ := x.exists_sum_rank_one,
-  simp_rw [_root_.map_sum, qam.complete_graph, qam.rank_one.refl_idempotent_eq, matrix.one_mul],
+  simp_rw [schur_idempotent, linear_map.coe_mk,
+    tensor_product.map_one, linear_map.one_comp, linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form hφ₂],
 end
-lemma qam.refl_idempotent_complete_graph_right (x : l(ℍ)) :
-  qam.refl_idempotent hφ.elim x (qam.complete_graph hφ.elim) = x :=
+
+lemma qam.lm.nontracial.is_unreflexive_iff_reflexive_add_one [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) (x : l(matrix p p ℂ)) :
+  schur_idempotent x 1 = 0
+    ↔ schur_idempotent (δ⁻¹ • (x + 1)) 1 = 1 :=
 begin
-  obtain ⟨α, β, rfl⟩ := x.exists_sum_rank_one,
-  simp_rw [_root_.map_sum, linear_map.sum_apply, qam.complete_graph,
-    qam.rank_one.refl_idempotent_eq, matrix.mul_one],
+  simp_rw [smul_hom_class.map_smul, linear_map.smul_apply,
+    _root_.map_add, linear_map.add_apply, qam.refl_idempotent_one_one_of_delta hφ₂,
+    smul_add, smul_smul, inv_mul_cancel (qam.nontracial.delta_ne_zero hφ₂), one_smul,
+    add_left_eq_self],
+  rw [smul_eq_zero_iff_eq' (inv_ne_zero (qam.nontracial.delta_ne_zero hφ₂))],
 end
 
-noncomputable def qam.complement' (hφ : φ.is_faithful_pos_map) (x : l(ℍ)) :
-  l(ℍ) :=
-(qam.complete_graph hφ) - x
+lemma pi.qam.lm.nontracial.is_unreflexive_iff_reflexive_add_one [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) (x : l(ℍ)) :
+  schur_idempotent x 1 = 0
+    ↔ schur_idempotent (δ⁻¹ • (x + 1)) 1 = 1 :=
+begin
+  simp_rw [smul_hom_class.map_smul, linear_map.smul_apply,
+    _root_.map_add, linear_map.add_apply, pi.qam.refl_idempotent_one_one_of_delta hφ₂,
+    smul_add, smul_smul, inv_mul_cancel (pi.qam.nontracial.delta_ne_zero hφ₂), one_smul,
+    add_left_eq_self],
+  rw [smul_eq_zero_iff_eq' (inv_ne_zero (pi.qam.nontracial.delta_ne_zero hφ₂))],
+end
 
-lemma qam.nontracial.complement'.qam (x : l(ℍ)) :
-  qam φ x ↔ qam φ (qam.complement' hφ.elim x) :=
+lemma qam.refl_idempotent_complete_graph_left {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (x : l(E)) :
+  schur_idempotent (qam.complete_graph E) x = x :=
+schur_idempotent_one_one_left _
+lemma qam.refl_idempotent_complete_graph_right
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : l(E)) :
+  schur_idempotent x (qam.complete_graph E) = x :=
+schur_idempotent_one_one_right _
+
+noncomputable def qam.complement'
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (x : l(E)) :
+  l(E) :=
+(qam.complete_graph E) - x
+
+lemma qam.nontracial.complement'.qam
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : l(E)) :
+  schur_idempotent x x = x ↔
+    schur_idempotent (qam.complement' x) (qam.complement' x) = (qam.complement' x) :=
 begin
-  simp only [qam.complement', qam, _root_.map_sub, linear_map.sub_apply,
+  simp only [qam.complement', _root_.map_sub, linear_map.sub_apply,
     qam.refl_idempotent_complete_graph_left,
     qam.refl_idempotent_complete_graph_right,
     qam.nontracial.complete_graph.qam],
@@ -214,23 +443,43 @@ begin
   simp only [sub_eq_zero, @eq_comm _ x],
 end
 
-lemma qam.nontracial.complement'.qam.is_real (x : l(ℍ)) :
-  x.is_real ↔ (qam.complement' hφ.elim x).is_real :=
+lemma qam.nontracial.complement'.qam.is_real
+  {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map]
+  (x : l(matrix p p ℂ)) :
+  x.is_real ↔ (qam.complement' x).is_real :=
+begin
+  simp only [qam.complement', linear_map.is_real_iff,
+    linear_map.real_sub, (linear_map.is_real_iff _).mp
+      (@qam.nontracial.complete_graph.is_real p _ _ φ _)],
+  simp only [sub_right_inj],
+end
+
+lemma pi.qam.nontracial.complement'.qam.is_real
+  [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (x : l(ℍ)) :
+  x.is_real ↔ (qam.complement' x).is_real :=
 begin
   simp only [qam.complement', linear_map.is_real_iff,
     linear_map.real_sub, (linear_map.is_real_iff _).mp
-      (@qam.nontracial.complete_graph.is_real n _ _ φ _)],
+      (@pi.qam.nontracial.complete_graph.is_real p _ _ n _ _ φ _)],
   simp only [sub_right_inj],
 end
 
-lemma qam.complement'_complement' (x : l(ℍ)) :
-  qam.complement' hφ.elim (qam.complement' hφ.elim x) = x :=
+lemma qam.complement'_complement'
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (x : l(E)) :
+  qam.complement' (qam.complement' x) = x :=
 sub_sub_cancel _ _
 
-lemma qam.nontracial.complement'.ir_reflexive (x : l(ℍ)) (α : Prop)
-  [decidable α] :
-  qam.refl_idempotent hφ.elim x (1 : l(ℍ)) = ite α (1 : l(ℍ)) (0 : l(ℍ))
-    ↔ qam.refl_idempotent hφ.elim (qam.complement' hφ.elim x) (1 : l(ℍ)) = ite α (0 : l(ℍ)) (1 : l(ℍ)) :=
+lemma qam.nontracial.complement'.ir_reflexive
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (x : l(E)) (α : Prop) [decidable α] :
+  schur_idempotent x (1 : l(E)) = ite α (1 : l(E)) (0 : l(E))
+    ↔ schur_idempotent (qam.complement' x) (1 : l(E)) = ite α (0 : l(E)) (1 : l(E)) :=
 begin
   simp_rw [qam.complement', _root_.map_sub, linear_map.sub_apply,
     qam.refl_idempotent_complete_graph_left],
@@ -239,139 +488,265 @@ begin
   { simp_rw [if_false, sub_eq_self], },
 end
 
-def qam_reflexive (hφ : φ.is_faithful_pos_map) (x : l(ℍ)) : Prop :=
-@qam n _ _ φ (fact.mk hφ) x ∧ qam.refl_idempotent hφ x 1 = 1
-def qam_irreflexive (hφ : φ.is_faithful_pos_map) (x : l(ℍ)) : Prop :=
-@qam n _ _ φ (fact.mk hφ) x ∧ qam.refl_idempotent hφ x 1 = 0
-
-lemma qam.complement'_is_irreflexive_iff (x : l(ℍ)) :
-  qam_irreflexive hφ.elim (qam.complement' hφ.elim x) ↔ qam_reflexive hφ.elim x :=
+def qam_reflexive
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : l(E)) : Prop :=
+schur_idempotent x x = x ∧ schur_idempotent x 1 = 1
+def qam_irreflexive {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : l(E)) : Prop :=
+schur_idempotent x x = x ∧ schur_idempotent x 1 = 0
+
+lemma qam.complement'_is_irreflexive_iff
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (x : l(E)) :
+  qam_irreflexive (qam.complement' x) ↔ qam_reflexive x :=
 begin
-  have := @qam.nontracial.complement'.ir_reflexive n _ _ φ _ x true _,
+  have := qam.nontracial.complement'.ir_reflexive x true,
   simp_rw [if_true] at this,
   rw [qam_reflexive, qam_irreflexive, ← qam.nontracial.complement'.qam],
   simp_rw [this],
 end
-lemma qam.complement'_is_reflexive_iff (x : l(ℍ)) :
-  qam_reflexive hφ.elim (qam.complement' hφ.elim x) ↔ qam_irreflexive hφ.elim x :=
+lemma qam.complement'_is_reflexive_iff
+  {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (x : l(E)) :
+  qam_reflexive (qam.complement' x) ↔ qam_irreflexive x :=
 begin
   have := qam.nontracial.complement'.ir_reflexive x false,
   simp_rw [if_false] at this,
   rw [qam_reflexive, qam_irreflexive, ← qam.nontracial.complement'.qam, this],
 end
 
-noncomputable def qam.complement'' (hφ : φ.is_faithful_pos_map) [nontrivial n] {x : l(ℍ)} (hx : x.is_real) :
+noncomputable def qam.complement'' [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  {δ : ℂ} (hφ : fact φ.is_faithful_pos_map)
+  (hφ₂ : φ.matrix⁻¹.trace = δ) (x : l(matrix p p ℂ)) :
+  l(matrix p p ℂ) :=
+x - (qam.trivial_graph hφ hφ₂)
+noncomputable def pi.qam.complement'' [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} (hφ : Π i, fact (φ i).is_faithful_pos_map)
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) (x : l(ℍ)) :
   l(ℍ) :=
-x - (qam.trivial_graph hφ)
+x - (pi.qam.trivial_graph hφ hφ₂)
+
+lemma single_schur_idempotent_real {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  (x y : l(matrix p p ℂ)) :
+  (schur_idempotent x y).real = schur_idempotent y.real x.real :=
+begin
+  obtain ⟨α, β, rfl⟩ := x.exists_sum_rank_one,
+  obtain ⟨γ, δ, rfl⟩ := y.exists_sum_rank_one,
+  simp only [linear_map.real_sum, map_sum, linear_map.sum_apply,
+    rank_one_real_apply, schur_idempotent.apply_rank_one,
+    mul_eq_mul, conj_transpose_mul],
+  simp only [← mul_eq_mul, _root_.map_mul],
+  rw finset.sum_comm,
+end
 
+lemma schur_idempotent_reflexive_of_is_real
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {x : l(matrix p p ℂ)} (hx : x.is_real) :
+  schur_idempotent x 1 = 1 ↔ schur_idempotent 1 x = 1 :=
+begin
+  rw [linear_map.real_inj_eq, single_schur_idempotent_real, linear_map.real_one, x.is_real_iff.mp hx],
+end
 
+lemma pi.schur_idempotent_reflexive_of_is_real
+  [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  {x : l(ℍ)} (hx : x.is_real) :
+  schur_idempotent x 1 = 1 ↔ schur_idempotent 1 x = 1 :=
+begin
+  rw [linear_map.real_inj_eq, schur_idempotent_real, linear_map.real_one, x.is_real_iff.mp hx],
+end
 
-lemma qam.complement''_is_irreflexive_iff [nontrivial n] {x : l(ℍ)}
-  (hx : x.is_real) :
-  qam_irreflexive hφ.elim (qam.complement'' hφ.elim hx) ↔ qam_reflexive hφ.elim x :=
+lemma qam.complement''_is_irreflexive_iff [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  {δ : ℂ} [hφ : fact φ.is_faithful_pos_map]
+  (hφ₂ : φ.matrix⁻¹.trace = δ) {x : l(matrix p p ℂ)} (hx : x.is_real) :
+  qam_irreflexive (qam.complement'' hφ hφ₂ x)
+    ↔ qam_reflexive x :=
 begin
   rw [qam_reflexive, qam_irreflexive],
-  have t1 := @qam.nontracial.trivial_graph.qam n _ _ φ _ _,
-  rw [qam] at t1 ⊢,
-  have t2 := @qam.nontracial.trivial_graph n _ _ φ _ _,
-  rw qam_lm_nontracial_is_reflexive at t2,
-  have t3 : qam.refl_idempotent hφ.elim (qam.complement'' hφ.elim hx) 1 = 0
-    ↔ qam.refl_idempotent hφ.elim x 1 = 1,
+  have t1 := qam.nontracial.trivial_graph.qam hφ₂,
+  have t2 := qam.nontracial.trivial_graph hφ₂,
+  have t3 : schur_idempotent (qam.complement'' hφ hφ₂ x) 1 = 0
+    ↔ schur_idempotent x 1 = 1,
   { simp_rw [qam.complement'', map_sub, linear_map.sub_apply,
       t2, sub_eq_zero], },
   rw [t3],
-  simp_rw [qam, qam.complement'', map_sub, linear_map.sub_apply, t1, sub_sub],
-  refine ⟨λ h, ⟨_, h.2⟩, λ h, ⟨_, h.2⟩⟩,
-  all_goals { have := (@qam.ir_refl_iff_ir_refl'_of_real n _ _ φ _ _ hx true _).mp,
-    simp_rw [if_true] at this,
-    rcases h with ⟨h1, h2⟩,
-    specialize this h2,
+  simp_rw [qam.complement'', map_sub, linear_map.sub_apply, t1, sub_sub],
+  split; rintros ⟨h1, h2⟩; refine ⟨_, h2⟩,
+
+  all_goals {
     simp only [qam.trivial_graph_eq, smul_hom_class.map_smul, linear_map.smul_apply,
-      h2, this, sub_self, add_zero, sub_left_inj] at h1 ⊢,
+      h2, (schur_idempotent_reflexive_of_is_real hx).mp h2,
+      sub_self, add_zero, sub_left_inj] at h1 ⊢,
+    exact h1, },
+end
+
+lemma pi.qam.complement''_is_irreflexive_iff [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} (hx : x.is_real) :
+  qam_irreflexive (pi.qam.complement'' hφ hφ₂ x)
+    ↔ qam_reflexive x :=
+begin
+  rw [qam_reflexive, qam_irreflexive],
+  have t1 := @pi.qam.nontracial.trivial_graph.qam p _ _ n _ _ φ _ _ δ _ hφ₂,
+  have t2 := @pi.qam.nontracial.trivial_graph p _ _ n _ _ φ _ _ δ _ hφ₂,
+  have t3 : schur_idempotent (pi.qam.complement'' hφ hφ₂ x) 1 = 0
+    ↔ schur_idempotent x 1 = 1,
+  { simp_rw [pi.qam.complement'', map_sub, linear_map.sub_apply,
+      t2, sub_eq_zero], },
+  rw [t3],
+  simp_rw [pi.qam.complement'', map_sub, linear_map.sub_apply, t1, sub_sub],
+  split; rintros ⟨h1, h2⟩; refine ⟨_, h2⟩,
+
+  all_goals {
+    simp only [pi.qam.trivial_graph_eq, smul_hom_class.map_smul, linear_map.smul_apply,
+      h2, (pi.schur_idempotent_reflexive_of_is_real hx).mp h2,
+      sub_self, add_zero, sub_left_inj] at h1 ⊢,
     exact h1, },
 end
 
-noncomputable def qam.irreflexive_complement (hφ : φ.is_faithful_pos_map)
-  [nontrivial n] {x : l(ℍ)} (hx : x.is_real) :
+noncomputable def pi.qam.irreflexive_complement [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} (hφ : Π i, fact (φ i).is_faithful_pos_map)
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) (x : l(ℍ)) :
   l(ℍ) :=
-(qam.complete_graph hφ) - (qam.trivial_graph hφ) - x
-noncomputable def qam.reflexive_complement (hφ : φ.is_faithful_pos_map)
-  [nontrivial n] {x : l(ℍ)} (hx : x.is_real) :
+(qam.complete_graph ℍ) - (pi.qam.trivial_graph hφ hφ₂) - x
+noncomputable def pi.qam.reflexive_complement [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} (hφ : Π i, fact (φ i).is_faithful_pos_map)
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) (x : l(ℍ)) :
   l(ℍ) :=
-(qam.complete_graph hφ) + (qam.trivial_graph hφ) - x
+(qam.complete_graph ℍ) + (pi.qam.trivial_graph hφ hφ₂) - x
+
+lemma qam.nontracial.trivial_graph.is_real [nonempty p]
+  {φ : module.dual ℂ (matrix p p ℂ)}
+  [hφ : fact φ.is_faithful_pos_map]
+  {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) :
+  (qam.trivial_graph hφ hφ₂).is_real :=
+begin
+  rw [linear_map.is_real_iff, qam.trivial_graph_eq, linear_map.real_smul,
+    linear_map.real_one, star_ring_end_apply, star_inv'],
+  congr,
+  rw ← hφ₂, 
+  rw [trace_star, hφ.elim.matrix_is_pos_def.inv.1.eq],
+end
 
-lemma qam.nontracial.trivial_graph.is_real [nontrivial n] :
-  (qam.trivial_graph hφ.elim).is_real :=
+lemma pi.qam.nontracial.trivial_graph.is_real [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  (pi.qam.trivial_graph hφ hφ₂).is_real :=
 begin
-  simp only [linear_map.is_real_iff, qam.trivial_graph_eq, linear_map.real_smul,
-    linear_map.real_one],
+  rw [linear_map.is_real_iff, pi.qam.trivial_graph_eq, linear_map.real_smul,
+    linear_map.real_one, star_ring_end_apply, star_inv'],
   congr,
-  rw [star_ring_end_apply, star_inv', trace_star, hφ.elim.matrix_is_pos_def.inv.1.eq],
+  rw ← hφ₂ (nonempty.some _inst_5), 
+  rw [trace_star, (hφ _).elim.matrix_is_pos_def.inv.1.eq],
 end
 
-lemma qam.irreflexive_complement.is_real [nontrivial n] {x : l(ℍ)} (hx : x.is_real) :
-  (qam.irreflexive_complement hφ.elim hx).is_real :=
+lemma pi.qam.irreflexive_complement.is_real
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} (hx : x.is_real) :
+  (pi.qam.irreflexive_complement hφ hφ₂ x).is_real :=
 begin
-  simp only [linear_map.is_real_iff, qam.irreflexive_complement, linear_map.real_sub,
-    (linear_map.is_real_iff (qam.complete_graph hφ.elim)).mp
-      qam.nontracial.complete_graph.is_real,
-    (linear_map.is_real_iff (qam.trivial_graph hφ.elim)).mp
-      qam.nontracial.trivial_graph.is_real,
+  rw [linear_map.is_real_iff, pi.qam.irreflexive_complement, linear_map.real_sub,
+    linear_map.real_sub,
+    (linear_map.is_real_iff (qam.complete_graph ℍ)).mp
+      pi.qam.nontracial.complete_graph.is_real,
+    (linear_map.is_real_iff (pi.qam.trivial_graph hφ hφ₂)).mp
+      (pi.qam.nontracial.trivial_graph.is_real hφ₂),
     (linear_map.is_real_iff x).mp hx],
 end
-lemma qam.reflexive_complement.is_real [nontrivial n] {x : l(ℍ)} (hx : x.is_real) :
-  (qam.reflexive_complement hφ.elim hx).is_real :=
+lemma pi.qam.reflexive_complement.is_real
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ)
+  {x : l(ℍ)} (hx : x.is_real) :
+  (pi.qam.reflexive_complement hφ hφ₂ x).is_real :=
 begin
-  simp only [linear_map.is_real_iff, qam.reflexive_complement, linear_map.real_sub,
+  rw [linear_map.is_real_iff, pi.qam.reflexive_complement, linear_map.real_sub,
     linear_map.real_add,
-    (linear_map.is_real_iff (qam.complete_graph hφ.elim)).mp
-      qam.nontracial.complete_graph.is_real,
-    (linear_map.is_real_iff (qam.trivial_graph hφ.elim)).mp
-      qam.nontracial.trivial_graph.is_real,
+    (linear_map.is_real_iff (qam.complete_graph ℍ)).mp
+      pi.qam.nontracial.complete_graph.is_real,
+    (linear_map.is_real_iff (pi.qam.trivial_graph hφ hφ₂)).mp
+      (pi.qam.nontracial.trivial_graph.is_real hφ₂),
     (linear_map.is_real_iff x).mp hx],
 end
 
-lemma qam.irreflexive_complement_irreflexive_complement [nontrivial n] {x : l(ℍ)}
-  (hx : x.is_real) :
-  qam.irreflexive_complement hφ.elim
-    (@qam.irreflexive_complement.is_real n _ _ φ _ _ _ hx) = x :=
+lemma pi.qam.irreflexive_complement_irreflexive_complement [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} :
+  pi.qam.irreflexive_complement hφ hφ₂ (pi.qam.irreflexive_complement hφ hφ₂ x) = x :=
 sub_sub_cancel _ _
-lemma qam.reflexive_complement_reflexive_complement [nontrivial n] {x : l(ℍ)}
-  (hx : x.is_real) :
-  qam.reflexive_complement hφ.elim (@qam.reflexive_complement.is_real n _ _ φ _ _ _ hx) = x :=
+lemma pi.qam.reflexive_complement_reflexive_complement [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} :
+  pi.qam.reflexive_complement hφ hφ₂ (pi.qam.reflexive_complement hφ hφ₂ x) = x :=
 sub_sub_cancel _ _
 
-lemma qam.trivial_graph_reflexive_complement_eq_complete_graph [nontrivial n] :
-  qam.reflexive_complement hφ.elim
-    (@qam.nontracial.trivial_graph.is_real n _ _ φ _ _)
-    = qam.complete_graph hφ.elim :=
+lemma pi.qam.trivial_graph_reflexive_complement_eq_complete_graph
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  pi.qam.reflexive_complement hφ hφ₂ (pi.qam.trivial_graph hφ hφ₂)
+    = qam.complete_graph ℍ :=
 add_sub_cancel _ _
-lemma qam.complete_graph_reflexive_complement_eq_trivial_graph [nontrivial n] :
-  qam.reflexive_complement hφ.elim
-    (@qam.nontracial.complete_graph.is_real n _ _ φ _)
-    = qam.trivial_graph hφ.elim :=
+lemma pi.qam.complete_graph_reflexive_complement_eq_trivial_graph
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) :
+  pi.qam.reflexive_complement hφ hφ₂ (qam.complete_graph ℍ)
+    = pi.qam.trivial_graph hφ hφ₂ :=
 add_sub_cancel' _ _
 
-lemma qam.complement'_eq (a : l(ℍ)) :
-  qam.complement' hφ.elim a = qam.complete_graph hφ.elim - a :=
+lemma qam.complement'_eq {E : Type*} [normed_add_comm_group_of_ring E]
+  [inner_product_space ℂ E] [finite_dimensional ℂ E]
+  [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E]
+  (a : l(E)) :
+  qam.complement' a = qam.complete_graph E - a :=
 rfl
 
-lemma qam.irreflexive_complement_is_irreflexive_qam_iff_irreflexive_qam [nontrivial n] {x : l(ℍ)} (hx : x.is_real) :
-  qam_irreflexive hφ.elim (qam.irreflexive_complement hφ.elim hx)
-    ↔ qam_irreflexive hφ.elim x :=
+lemma pi.qam.irreflexive_complement_is_irreflexive_qam_iff_irreflexive_qam
+  [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} (hx : x.is_real) :
+  qam_irreflexive (pi.qam.irreflexive_complement hφ hφ₂ x)
+    ↔ qam_irreflexive x :=
 begin
-  rw [qam.irreflexive_complement, sub_sub, ← qam.complement'_eq,
-    qam.complement'_is_irreflexive_iff, ← qam.complement''_is_irreflexive_iff,
-    qam.complement'', add_sub_cancel'],
+  rw [pi.qam.irreflexive_complement, sub_sub, ← qam.complement'_eq,
+    qam.complement'_is_irreflexive_iff, ← pi.qam.complement''_is_irreflexive_iff hφ₂,
+    pi.qam.complement'', add_sub_cancel'],
   { rw [linear_map.is_real_iff, linear_map.real_add, x.is_real_iff.mp hx,
-      (qam.trivial_graph hφ.elim).is_real_iff.mp qam.nontracial.trivial_graph.is_real], },
+      (pi.qam.trivial_graph hφ hφ₂).is_real_iff.mp (pi.qam.nontracial.trivial_graph.is_real hφ₂)], },
 end
-lemma qam.reflexive_complment_is_reflfexive_qam_iff_reflexive_qam [nontrivial n] {x : l(ℍ)}
+lemma pi.qam.reflexive_complment_is_reflexive_qam_iff_reflexive_qam [nonempty p]
+  [Π i, nontrivial (n i)]
+  {δ : ℂ} [hφ : Π i, fact (φ i).is_faithful_pos_map]
+  (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)}
   (hx : x.is_real) :
-  qam_reflexive hφ.elim (qam.reflexive_complement hφ.elim hx)
-    ↔ qam_reflexive hφ.elim x :=
+  qam_reflexive (pi.qam.reflexive_complement hφ hφ₂ x)
+    ↔ qam_reflexive x :=
 begin
-  rw [qam.reflexive_complement, ← sub_sub_eq_add_sub, ← qam.complement'_eq,
+  rw [pi.qam.reflexive_complement, ← sub_sub_eq_add_sub, ← qam.complement'_eq,
     qam.complement'_is_reflexive_iff],
-  exact qam.complement''_is_irreflexive_iff hx,
+  exact pi.qam.complement''_is_irreflexive_iff hφ₂ hx,
 end
diff --git a/src/quantum_graph/mess.lean b/src/quantum_graph/mess.lean
index 0b194bc57c..bcb7fac0c3 100644
--- a/src/quantum_graph/mess.lean
+++ b/src/quantum_graph/mess.lean
@@ -889,11 +889,11 @@ begin
   simp_rw [linear_map.comp_apply],
   simp_rw [← ι_linear_equiv_apply_eq, ← ι_linear_equiv_symm_apply_eq,
     linear_equiv.symm_apply_apply],
-  have : (ι_linear_equiv hφ.elim).symm 1 = qam.complete_graph hφ.elim,
+  have : (ι_linear_equiv hφ.elim).symm 1 = qam.complete_graph ℍ,
   { simp_rw [ι_linear_equiv_symm_apply_eq, algebra.tensor_product.one_def,
       ι_inv_map_apply, conj_transpose_one, _root_.map_one],
     refl, },
-  rw [this, qam.refl_idempotent_complete_graph_right],
+  rw [this, qam.refl_idempotent, qam.refl_idempotent_complete_graph_right],
 end
 
 lemma φ_inv'_map_φ_map :
diff --git a/src/quantum_graph/qam_A.lean b/src/quantum_graph/qam_A.lean
index 2ab349905d..fffbf75013 100644
--- a/src/quantum_graph/qam_A.lean
+++ b/src/quantum_graph/qam_A.lean
@@ -773,7 +773,7 @@ begin
 end
 
 lemma qam_A.of_trivial_graph [nontrivial n] :
-  qam_A hφ.elim ⟨φ.matrix⁻¹, hφ.elim.matrix_is_pos_def.inv.ne_zero⟩ = qam.trivial_graph hφ.elim :=
+  qam_A hφ.elim ⟨φ.matrix⁻¹, hφ.elim.matrix_is_pos_def.inv.ne_zero⟩ = qam.trivial_graph hφ rfl :=
 begin
   rw qam_A,
   haveI := hφ.elim.matrix_is_pos_def.invertible,
@@ -789,7 +789,7 @@ end
 lemma qam.unique_one_edge_and_refl [nontrivial n] {A : l(ℍ)}
   (hA : real_qam hφ.elim A) :
   (hA.edges = 1 ∧ qam.refl_idempotent hφ.elim A 1 = 1)
-    ↔ A = qam.trivial_graph hφ.elim :=
+    ↔ A = qam.trivial_graph hφ rfl :=
 begin
   split,
   { rintros ⟨h1, h2⟩,
@@ -799,7 +799,7 @@ begin
     rw [← qam_A_eq, ← qam_A.of_trivial_graph, qam_A.is_almost_injective],
     exact (qam_A.is_reflexive_iff x).mp h2, },
   { rintros rfl,
-    exact ⟨qam.trivial_graph_edges, qam.nontracial.trivial_graph⟩, },
+    exact ⟨qam.trivial_graph_edges, qam.nontracial.trivial_graph rfl⟩, },
 end
 
 private lemma star_alg_equiv.is_isometry_iff [nontrivial n] (f : ℍ ≃⋆ₐ[ℂ] ℍ) :
diff --git a/src/quantum_graph/schur_idempotent.lean b/src/quantum_graph/schur_idempotent.lean
index 18b0ee9f5e..a7d82ad8cc 100644
--- a/src/quantum_graph/schur_idempotent.lean
+++ b/src/quantum_graph/schur_idempotent.lean
@@ -348,6 +348,14 @@ begin
   ext1 h,
   tidy,
 end
+example {ψ : Π i, module.dual ℂ (matrix (s i) (s i) ℂ)}
+  [hψ : Π i, fact (ψ i).is_faithful_pos_map] (x : 𝔹) :
+  (module.dual.pi.is_faithful_pos_map.to_matrix (λ i, (hψ i).elim) (lmul x : l(𝔹))
+    : matrix (Σ i, s i × s i) (Σ i, s i × s i) ℂ)
+  = block_diagonal' (λ i, (hψ i).elim.to_matrix (lmul (x i))) :=
+begin
+  simp_rw [pi_lmul_to_matrix, lmul_eq_mul, linear_map.mul_left_to_matrix],
+end
 lemma pi_rmul_to_matrix
   {ψ : Π i, module.dual ℂ (matrix (s i) (s i) ℂ)}
   [hψ : Π i, fact (ψ i).is_faithful_pos_map] (x : 𝔹) :
@@ -374,6 +382,40 @@ begin
   ext1 h,
   tidy,
 end
+lemma unitary.coe_pi (U : Π i, unitary_group (s i) ℂ) :
+  (unitary.pi U : Π i, matrix (s i) (s i) ℂ) = ↑U :=
+rfl
+lemma unitary.coe_pi_apply (U : Π i, unitary_group (s i) ℂ) (i : n) :
+  (↑U : Π i, matrix (s i) (s i) ℂ) i = U i :=
+rfl
+
+lemma pi_inner_aut_to_matrix
+  {ψ : Π i, module.dual ℂ (matrix (s i) (s i) ℂ)}
+  [hψ : Π i, fact (ψ i).is_faithful_pos_map]
+  (U : Π i, unitary_group (s i) ℂ) :
+  (module.dual.pi.is_faithful_pos_map.to_matrix (λ i, (hψ i).elim) ((unitary.inner_aut_star_alg ℂ (unitary.pi U)).to_alg_equiv.to_linear_map : l(𝔹))
+    : matrix (Σ i, s i × s i) (Σ i, s i × s i) ℂ)
+  =
+  block_diagonal' (λ i,
+    (U i) ⊗ₖ ((hψ i).elim.sig (- (1/2 : ℝ)) ((U i) : matrix (s i) (s i) ℂ))ᴴᵀ) :=
+begin
+  have : ((unitary.inner_aut_star_alg ℂ (unitary.pi U)).to_alg_equiv.to_linear_map : l(𝔹))
+    =
+  (lmul ↑U : l(𝔹)) * (rmul (star ↑U) : l(𝔹)),
+  { ext1,
+    simp_rw [alg_equiv.to_linear_map_apply, star_alg_equiv.coe_to_alg_equiv,
+      linear_map.mul_apply, lmul_apply, rmul_apply, unitary.inner_aut_star_alg_apply,
+      mul_assoc, unitary.coe_star, unitary.coe_pi], },
+  rw [this, _root_.map_mul, pi_lmul_to_matrix, pi_rmul_to_matrix,
+    mul_eq_mul, ← block_diagonal'_mul],
+  simp_rw [← mul_kronecker_mul, matrix.mul_one, matrix.one_mul,
+    pi.star_apply, star_eq_conj_transpose, block_diagonal'_inj, unitary.coe_pi_apply],
+  ext1 i,
+  nth_rewrite 0 [← neg_neg (1 / 2 : ℝ)],
+  simp_rw [← module.dual.is_faithful_pos_map.sig_conj_transpose],
+  refl,
+end
+
 lemma schur_idempotent_one_left_rank_one
   {ψ : Π i, module.dual ℂ (matrix (s i) (s i) ℂ)}
   [hψ : Π i, fact (ψ i).is_faithful_pos_map]
diff --git a/src/quantum_graph/to_projections.lean b/src/quantum_graph/to_projections.lean
index b81402691d..821283e983 100644
--- a/src/quantum_graph/to_projections.lean
+++ b/src/quantum_graph/to_projections.lean
@@ -15,19 +15,23 @@ This file contains the definition of a quantum graph as a projection, and the pr
 
 -/
 
-variables {n p : Type*} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p]
+variables {p : Type*} [fintype p] [decidable_eq p] {n : p → Type*}
+  [Π i, fintype (n i)] [Π i, decidable_eq (n i)]
 
 open_locale tensor_product big_operators kronecker functional
 
-local notation `ℍ` := matrix n n ℂ
-local notation `⊗K` := matrix (n × n) (n × n) ℂ
+-- local notation `ℍ` := matrix (n i) (n i) ℂ
+local notation `ℍ` := matrix p p ℂ
+local notation `ℍ_`i := matrix (n i) (n i) ℂ
+-- local notation `⊗K` := matrix (n × n) (n × n) ℂ
 local notation `l(`x`)` := x →ₗ[ℂ] x
 local notation `L(`x`)` := x →L[ℂ] x
 
 local notation `e_{` i `,` j `}` := matrix.std_basis_matrix i j (1 : ℂ)
 
-variables {φ : module.dual ℂ ℍ} [hφ : fact φ.is_faithful_pos_map]
-  {ψ : module.dual ℂ (matrix p p ℂ)} (hψ : ψ.is_faithful_pos_map)
+variables --{φ : Π i, module.dual ℂ (ℍ_ i)}
+  --[hφ : ∀ i, fact (φ i).is_faithful_pos_map]
+  {φ : module.dual ℂ ℍ} [hφ : fact φ.is_faithful_pos_map]
 
 open_locale matrix
 open matrix
@@ -37,27 +41,96 @@ local notation `m` := linear_map.mul' ℂ ℍ
 local notation `η` := algebra.linear_map ℂ ℍ
 local notation x ` ⊗ₘ ` y := tensor_product.map x y
 local notation `υ` :=
-  ((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ))
-    : (matrix n n ℂ ⊗[ℂ] matrix n n ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ]
-      matrix n n ℂ ⊗[ℂ] (matrix n n ℂ ⊗[ℂ] matrix n n ℂ))
+  ((tensor_product.assoc ℂ (ℍ) (ℍ) (ℍ))
+    : (ℍ ⊗[ℂ] ℍ ⊗[ℂ] ℍ) →ₗ[ℂ]
+      ℍ ⊗[ℂ] (ℍ ⊗[ℂ] ℍ))
 local notation `υ⁻¹` :=
-  ((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).symm
-    : matrix n n ℂ ⊗[ℂ] (matrix n n ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ]
-      (matrix n n ℂ ⊗[ℂ] matrix n n ℂ ⊗[ℂ] matrix n n ℂ))
-local notation `ϰ` := (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ)
-  : (matrix n n ℂ ⊗[ℂ] ℂ) →ₗ[ℂ] (ℂ ⊗[ℂ] matrix n n ℂ))
-local notation `ϰ⁻¹` := ((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm
-  : (ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ] (matrix n n ℂ ⊗[ℂ] ℂ))
-local notation `τ` := ((tensor_product.lid ℂ (matrix n n ℂ))
-  : (ℂ ⊗[ℂ] matrix n n ℂ) →ₗ[ℂ] matrix n n ℂ)
-local notation `τ⁻¹` := ((tensor_product.lid ℂ (matrix n n ℂ)).symm
-  : matrix n n ℂ →ₗ[ℂ] (ℂ ⊗[ℂ] matrix n n ℂ))
-local notation `id` := (1 : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
-
-lemma rank_one_Psi_transpose_to_lin (x y : ℍ) :
-  hφ.elim.to_matrix.symm ((tensor_product.map id (transpose_alg_equiv n ℂ ℂ).symm.to_linear_map)
+  ((tensor_product.assoc ℂ (ℍ) (ℍ) (ℍ)).symm
+    : ℍ ⊗[ℂ] (ℍ ⊗[ℂ] ℍ) →ₗ[ℂ]
+      (ℍ ⊗[ℂ] ℍ ⊗[ℂ] ℍ))
+local notation `ϰ` := (↑(tensor_product.comm ℂ (ℍ) ℂ)
+  : (ℍ ⊗[ℂ] ℂ) →ₗ[ℂ] (ℂ ⊗[ℂ] ℍ))
+local notation `ϰ⁻¹` := ((tensor_product.comm ℂ (ℍ) ℂ).symm
+  : (ℂ ⊗[ℂ] ℍ) →ₗ[ℂ] (ℍ ⊗[ℂ] ℂ))
+local notation `τ` := ((tensor_product.lid ℂ (ℍ))
+  : (ℂ ⊗[ℂ] ℍ) →ₗ[ℂ] ℍ)
+local notation `τ⁻¹` := ((tensor_product.lid ℂ (ℍ)).symm
+  : ℍ →ₗ[ℂ] (ℂ ⊗[ℂ] ℍ))
+local notation `id` := (1 : ℍ →ₗ[ℂ] ℍ)
+
+noncomputable def block_diag'_kronecker_equiv
+  {φ : Π i, module.dual ℂ (ℍ_ i)}
+  (hφ : ∀ i, fact (φ i).is_faithful_pos_map) :
+    matrix (Σ i, n i × n i) (Σ i, n i × n i) ℂ
+    ≃ₗ[ℂ]
+    { x : matrix (Σ i, n i) (Σ i, n i) ℂ // x.is_block_diagonal }
+    ⊗[ℂ]
+    { x : matrix (Σ i, n i) (Σ i, n i) ℂ // x.is_block_diagonal }
+    :=
+((module.dual.pi.is_faithful_pos_map.to_matrix (λ i, (hφ i).elim)).symm.to_linear_equiv.trans
+    ((module.dual.pi.is_faithful_pos_map.Psi hφ 0 0).trans
+      (linear_equiv.tensor_product.map (1 : (Π i, matrix (n i) (n i) ℂ) ≃ₗ[ℂ] _)
+        ((pi.transpose_alg_equiv p n : _ ≃ₐ[ℂ] _ᵐᵒᵖ).symm).to_linear_equiv))).trans
+    (linear_equiv.tensor_product.map (is_block_diagonal_pi_alg_equiv.symm.to_linear_equiv)
+    (is_block_diagonal_pi_alg_equiv.symm.to_linear_equiv))
+
+lemma linear_equiv.coe_one {R : Type*} [semiring R] (M : Type*) [add_comm_monoid M]
+  [module R M] :
+  ↑(1 : M ≃ₗ[R] M) = (1 : M →ₗ[R] M) :=
+rfl
+
+lemma matrix.conj_conj_transpose' {R n₁ n₂ : Type*} [has_involutive_star R] (A : matrix n₁ n₂ R) :
+  ((Aᴴ)ᵀ)ᴴ = Aᵀ :=
+by rw [← conj_conj_transpose A]; refl
+
+lemma to_matrix_mul_left_mul_right_adjoint {φ : Π i, module.dual ℂ (matrix (n i) (n i) ℂ)}
+  (hφ : Π i, fact (φ i).is_faithful_pos_map) (x y : Π i, (ℍ_ i)) :
+  (module.dual.pi.is_faithful_pos_map.to_matrix (λ i, (hφ i).elim))
+    ((linear_map.mul_left ℂ x) * ((linear_map.mul_right ℂ y).adjoint : l(Π i, ℍ_ i)))
+  = block_diagonal' (λ i, (x i) ⊗ₖ ((hφ i).elim.sig (1/2) (y i))ᴴᵀ) :=
+begin
+  have : (1 / 2 : ℝ) + (-1 : ℝ) = - (1 / 2) := by norm_num,
+  simp_rw [_root_.map_mul, ← lmul_eq_mul, ← rmul_eq_mul,
+    rmul_adjoint, pi_lmul_to_matrix, pi_rmul_to_matrix,
+    mul_eq_mul, ← block_diagonal'_mul, ← mul_kronecker_mul,
+    matrix.one_mul, matrix.mul_one, module.dual.pi.is_faithful_pos_map.sig_eq_pi_blocks,
+    pi.star_apply, module.dual.is_faithful_pos_map.sig_apply_sig, star_eq_conj_transpose,
+    this, ← module.dual.is_faithful_pos_map.sig_conj_transpose],
+  refl,
+end
+
+@[instance] private def smul_comm_class_aux {ι₂ : Type*} {E₂ : ι₂ → Type*} [Π i, add_comm_monoid (E₂ i)] [Π i, module ℂ (E₂ i)] :
+  ∀ (i : ι₂), smul_comm_class ℂ ℂ (E₂ i) :=
+λ i, by apply_instance
+
+@[simps] def pi.linear_map.apply {ι₁ ι₂ : Type*} {E₁ : ι₁ → Type*}
+  [decidable_eq ι₁] [fintype ι₁]
+  [Π i, add_comm_monoid (E₁ i)] [Π i, module ℂ (E₁ i)]
+  {E₂ : ι₂ → Type*} [Π i, add_comm_monoid (E₂ i)] [Π i, module ℂ (E₂ i)]
+  (i : ι₁) (j : ι₂) :
+  ((Π a, E₁ a) →ₗ[ℂ] (Π a, E₂ a)) →ₗ[ℂ] (E₁ i →ₗ[ℂ] E₂ j) :=
+{ to_fun := λ x,
+  { to_fun := λ a, (x ((linear_map.single i : E₁ i →ₗ[ℂ] Π b, E₁ b) a)) j,
+    map_add' := λ a b, by
+    { simp only [linear_map.add_apply, map_add, pi.add_apply], },
+    map_smul' := λ c a, by
+    { simp only [linear_map.smul_apply, linear_map.map_smul, pi.smul_apply, ring_hom.id_apply], } },
+  map_add' := λ x y, by
+  { ext a,
+    simp only [linear_map.add_apply, pi.add_apply, linear_map.coe_mk], },
+  map_smul' := λ c x, by
+  { ext a,
+    simp only [linear_map.smul_apply, pi.smul_apply, linear_map.map_smul, ring_hom.id_apply,
+      linear_map.coe_mk], } }
+
+lemma rank_one_Psi_transpose_to_lin {n : Type*} [decidable_eq n] [fintype n]
+  {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact (φ.is_faithful_pos_map)]
+  (x y : matrix n n ℂ) :
+  hφ.elim.to_matrix.symm
+  ((tensor_product.map (1 : l(matrix n n ℂ))
+      (transpose_alg_equiv n ℂ ℂ).symm.to_linear_map)
     ((hφ.elim.Psi 0 (1/2)) (|x⟩⟨y|))).to_kronecker
-  = (linear_map.mul_left ℂ x) *  ((linear_map.mul_right ℂ y).adjoint : l(ℍ)) :=
+  = (linear_map.mul_left ℂ x) * ((linear_map.mul_right ℂ y).adjoint : l(matrix n n ℂ)) :=
 begin
   let b := @module.dual.is_faithful_pos_map.orthonormal_basis n _ _ φ _,
   rw ← function.injective.eq_iff hφ.elim.to_matrix.injective,
@@ -81,8 +154,40 @@ begin
   simp_rw [transpose_apply, std_basis_matrix, and_comm],
 end
 
-lemma rank_one_to_matrix_transpose_Psi_symm (x y : ℍ) :
-  (hφ.elim.Psi 0 (1/2)).symm ((tensor_product.map id (transpose_alg_equiv n ℂ ℂ).to_linear_map)
+-- example :
+--   -- { x : matrix (Σ i, n i × n i) (Σ i, n i × n i) ℂ // x.is_block_diagonal }
+--   matrix (Σ i, n i × n i) (Σ i, n i × n i) ℂ
+--     ≃ₐ[ℂ]
+--   { x : matrix (Σ i : p × p, n i.1 × n i.2) (Σ i : p × p, n i.1 × n i.2) ℂ // x.is_block_diagonal }
+--   -- {x : (matrix (Σ i, n i) (Σ i, n i) ℂ) ⊗[ℂ] (matrix (Σ i, n i) (Σ i, n i) ℂ) // x.is_block_diagonal}
+--   -- {x : matrix (Σ i, n i) (Σ i, n i) ℂ // x.is_block_diagonal} :=
+--   -- (Π i, matrix (n i) (n i) ℂ) ⊗[ℂ] (Π i, matrix (n i) (n i) ℂ)
+--   :=
+-- { to_fun := λ x, by {  },
+--   -- dite (a.1.1 = b.1.1)
+--   -- (λ h1,
+--   --   dite (a.1.1 = a.2.1 ∧ b.1.1 = b.2.1) (
+--   --   λ h : a.1.1 = a.2.1 ∧ b.1.1 = b.2.1,
+--   --   let a' : n a.1.1 := by rw [h.1]; exact a.2.2 in
+--   --   let b' : n b.1.1 := by rw [h.2]; exact b.2.2 in
+--   --   x (⟨a.1.1, a.1.2, a'⟩) (⟨b.1.1, b.1.2, b'⟩))
+--   -- (λ h, 0),
+--   inv_fun := λ x a b, x (⟨a.1, a.2.1⟩, ⟨a.1, a.2.2⟩) (⟨b.1, b.2.1⟩, ⟨b.1, b.2.2⟩),
+--   left_inv := λ x, by
+--   { ext1,
+--     simp only [],
+--     split_ifs,
+--     tidy, },
+--   right_inv := λ x, by
+--   { ext1,
+--     simp only [],
+--     split_ifs,
+--     tidy, },
+--      }
+
+lemma rank_one_to_matrix_transpose_Psi_symm
+  (x y : ℍ) :
+  (hφ.elim.Psi 0 (1/2)).symm ((tensor_product.map id (transpose_alg_equiv p ℂ ℂ).to_linear_map)
       (hφ.elim.to_matrix (|x⟩⟨y|)).kronecker_to_tensor_product)
   = (linear_map.mul_left ℂ (x ⬝ φ.matrix))
     * ((linear_map.mul_right ℂ (φ.matrix ⬝ y)).adjoint : l(ℍ)) :=
@@ -100,7 +205,7 @@ begin
     rank_one_apply, rank_one_to_matrix, conj_transpose_col, ← vec_mul_vec_eq,
     vec_mul_vec_apply, pi.star_apply, linear_map.mul_left_apply, linear_map.mul_right_apply,
     reshape_apply],
-  have : ∀ (i j : n) (a : ℍ), ⟪hφ.elim.sig (-(1/2)) e_{i,j}, a⟫_ℂ
+  have : ∀ (i j : p) (a : ℍ), ⟪hφ.elim.sig (-(1/2)) e_{i,j}, a⟫_ℂ
     = ⟪e_{i,j} ⬝ hφ.elim.matrix_is_pos_def.rpow (-(1/2)), hφ.elim.matrix_is_pos_def.rpow (1/2) ⬝ a⟫_ℂ,
   { intros i j a,
     simp_rw [module.dual.is_faithful_pos_map.sig_apply, matrix.mul_assoc, neg_neg,
@@ -177,9 +282,9 @@ lemma matrix.conj_eq_conj_transpose_transpose {R n₁ n₂ : Type*} [has_star R]
 rfl
 
 noncomputable def one_map_transpose :
-  (ℍ ⊗[ℂ] ℍᵐᵒᵖ) ≃⋆ₐ[ℂ] (matrix (n × n) (n × n) ℂ) :=
+  (ℍ ⊗[ℂ] ℍᵐᵒᵖ) ≃⋆ₐ[ℂ] (matrix (p × p) (p × p) ℂ) :=
 star_alg_equiv.of_alg_equiv ( (alg_equiv.tensor_product.map (1 : ℍ ≃ₐ[ℂ] ℍ)
-          (transpose_alg_equiv n ℂ ℂ).symm).trans tensor_to_kronecker)
+          (transpose_alg_equiv p ℂ ℂ).symm).trans tensor_to_kronecker)
 (begin
   intro x,
   simp only [alg_equiv.trans_apply],
@@ -205,15 +310,15 @@ end)
 
 lemma one_map_transpose_eq (x : ℍ ⊗[ℂ] ℍᵐᵒᵖ) :
   (one_map_transpose : (ℍ ⊗[ℂ] ℍᵐᵒᵖ) ≃⋆ₐ[ℂ] _) x = ((tensor_product.map (1 : l(ℍ))
-    (transpose_alg_equiv n ℂ ℂ).symm.to_linear_map) x).to_kronecker :=
+    (transpose_alg_equiv p ℂ ℂ).symm.to_linear_map) x).to_kronecker :=
 rfl
-lemma one_map_transpose_symm_eq (x : ⊗K) :
+lemma one_map_transpose_symm_eq (x : matrix (p × p) (p × p) ℂ) :
   (one_map_transpose : (ℍ ⊗[ℂ] ℍᵐᵒᵖ) ≃⋆ₐ[ℂ] _).symm x = ((tensor_product.map (1 : l(ℍ))
-    (transpose_alg_equiv n ℂ ℂ).to_linear_map) x.kronecker_to_tensor_product) :=
+    (transpose_alg_equiv p ℂ ℂ).to_linear_map) x.kronecker_to_tensor_product) :=
 rfl
 
 lemma one_map_transpose_apply (x y : ℍ) :
-  (one_map_transpose : _ ≃⋆ₐ[ℂ] ⊗K) (x ⊗ₜ mul_opposite.op y) = x ⊗ₖ yᵀ :=
+  (one_map_transpose : _ ≃⋆ₐ[ℂ] matrix (p × p) (p × p) ℂ) (x ⊗ₜ mul_opposite.op y) = x ⊗ₖ yᵀ :=
 begin
   rw [one_map_transpose_eq, tensor_product.map_tmul, alg_equiv.to_linear_map_apply,
     tensor_product.to_kronecker_apply, transpose_alg_equiv_symm_op_apply],
@@ -230,10 +335,10 @@ begin
     linear_map.star_eq_adjoint, linear_map.adjoint_inner_right, is_R_or_C.star_def,
     inner_conj_symm, module.dual.is_faithful_pos_map.basis_repr_apply],
 end
-private lemma ffsugh {x : matrix (n × n) (n × n) ℂ} {y : l(ℍ)} :
+private lemma ffsugh {x : matrix (p × p) (p × p) ℂ} {y : l(ℍ)} :
   hφ.elim.to_matrix.symm x = y ↔ x = hφ.elim.to_matrix y :=
 equiv.symm_apply_eq _
-lemma to_matrix''_symm_map_star (x : ⊗K) :
+lemma to_matrix''_symm_map_star (x : matrix (p × p) (p × p) ℂ) :
   hφ.elim.to_matrix.symm (star x) = ((hφ.elim.to_matrix.symm x).adjoint) :=
 begin
   rw [ffsugh, to_matrix''_map_star, alg_equiv.apply_symm_apply],
@@ -243,7 +348,7 @@ lemma qam.idempotent_and_real_iff_exists_ortho_proj (A : l(ℍ)) :
   (qam.refl_idempotent hφ.elim A A = A ∧ A.is_real) ↔
     ∃ (U : submodule ℂ ℍ),
       (orthogonal_projection' U : l(ℍ))
-      = (hφ.elim.to_matrix.symm ((tensor_product.map id (transpose_alg_equiv n ℂ ℂ).symm.to_linear_map)
+      = (hφ.elim.to_matrix.symm ((tensor_product.map id (transpose_alg_equiv p ℂ ℂ).symm.to_linear_map)
       ((hφ.elim.Psi 0 (1/2)) A)).to_kronecker) :=
 begin
   rw [qam.is_real_and_idempotent_iff_Psi_orthogonal_projection,
@@ -265,7 +370,7 @@ end
 lemma qam.orthogonal_projection'_eq {A : l(ℍ)} (hA1 : qam.refl_idempotent hφ.elim A A = A)
   (hA2 : A.is_real) :
   (orthogonal_projection' (qam.submodule_of_idempotent_and_real hA1 hA2) : l(ℍ))
-  = (hφ.elim.to_matrix.symm ((tensor_product.map id (transpose_alg_equiv n ℂ ℂ).symm.to_linear_map)
+  = (hφ.elim.to_matrix.symm ((tensor_product.map id (transpose_alg_equiv p ℂ ℂ).symm.to_linear_map)
     ((hφ.elim.Psi 0 (1/2)) A)).to_kronecker) :=
 (qam.submodule_of_idempotent_and_real._proof_8 hA1 hA2)
 
@@ -378,15 +483,15 @@ begin
 end
 
 lemma complete_graph_real_qam :
-  real_qam hφ.elim (qam.complete_graph hφ.elim) :=
+  real_qam hφ.elim (qam.complete_graph ℍ) :=
 ⟨qam.nontracial.complete_graph.qam, qam.nontracial.complete_graph.is_real⟩
 
 lemma qam.complete_graph_edges :
-  (@complete_graph_real_qam n _ _ φ hφ).edges = finite_dimensional.finrank ℂ (⊤ : submodule ℂ ℍ) :=
+  (@complete_graph_real_qam p _ _ φ hφ).edges = finite_dimensional.finrank ℂ (⊤ : submodule ℂ ℍ) :=
 begin
   have := calc
     (real_qam.edges complete_graph_real_qam : ℂ)
-    = (qam.complete_graph hφ.elim φ.matrix⁻¹).trace : real_qam.edges_eq _,
+    = (qam.complete_graph ℍ φ.matrix⁻¹).trace : real_qam.edges_eq _,
   haveI ig := hφ.elim.matrix_is_pos_def.invertible,
   simp_rw [qam.complete_graph, continuous_linear_map.coe_coe,
     rank_one_apply, module.dual.is_faithful_pos_map.inner_eq',
@@ -396,14 +501,14 @@ begin
   simp_rw [qam.complete_graph, this, finrank_top, finite_dimensional.finrank_matrix],
 end
 
-lemma qam.trivial_graph_real_qam [nontrivial n] :
-  real_qam hφ.elim (qam.trivial_graph hφ.elim) :=
-⟨qam.nontracial.trivial_graph.qam, qam.nontracial.trivial_graph.is_real⟩
+lemma qam.trivial_graph_real_qam [nontrivial p] :
+  real_qam hφ.elim (qam.trivial_graph hφ rfl) :=
+⟨qam.nontracial.trivial_graph.qam rfl, qam.nontracial.trivial_graph.is_real rfl⟩
 
-lemma qam.trivial_graph_edges [nontrivial n] :
-  (@qam.trivial_graph_real_qam n _ _ φ hφ _).edges = 1 :=
+lemma qam.trivial_graph_edges [nontrivial p] :
+  (@qam.trivial_graph_real_qam p _ _ φ hφ _).edges = 1 :=
 begin
-  have := real_qam.edges_eq (@qam.trivial_graph_real_qam n _ _ φ _ _),
+  have := real_qam.edges_eq (@qam.trivial_graph_real_qam p _ _ φ _ _),
   haveI ig := hφ.elim.matrix_is_pos_def.invertible,
   simp_rw [qam.trivial_graph_eq, linear_map.smul_apply, linear_map.one_apply,
     trace_smul, smul_eq_mul, inv_mul_cancel (hφ.elim.matrix_is_pos_def.inv.trace_ne_zero)] at this,
@@ -431,8 +536,8 @@ begin
   simp_rw [matrix.zero_mul, linear_map.mul_left_zero_eq_zero, zero_mul],
 end
 
-private lemma orthogonal_projection_of_top {𝕜 E : Type*} [is_R_or_C 𝕜] [normed_add_comm_group E]
-  [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
+lemma orthogonal_projection_of_top {𝕜 E : Type*} [is_R_or_C 𝕜] [normed_add_comm_group E]
+  [inner_product_space 𝕜 E] [complete_space ↥(⊤ : submodule 𝕜 E)] :
   orthogonal_projection' (⊤ : submodule 𝕜 E) = 1 :=
 begin
   ext1,
@@ -453,7 +558,7 @@ lemma real_qam.edges_eq_dim_iff {A : l(ℍ)} (hA : real_qam hφ.elim A) :
   hA.edges = finite_dimensional.finrank ℂ (⊤ : submodule ℂ ℍ)
     ↔ A = (|(1 : ℍ)⟩⟨(1 : ℍ)|) :=
 begin
-  refine ⟨λ h, _, λ h, by { rw [← @qam.complete_graph_edges n _ _ φ],
+  refine ⟨λ h, _, λ h, by { rw [← @qam.complete_graph_edges p _ _ φ],
     simp only [h] at hA,
     simp only [h, hA],
     refl, }⟩,
@@ -467,7 +572,7 @@ begin
   { rw [hU, orthogonal_projection_of_top],
     refl, },
   rw this at t1,
-  apply_fun (one_map_transpose : ℍ ⊗[ℂ] ℍᵐᵒᵖ ≃⋆ₐ[ℂ] matrix (n × n) (n × n) ℂ)
+  apply_fun (one_map_transpose : ℍ ⊗[ℂ] ℍᵐᵒᵖ ≃⋆ₐ[ℂ] matrix (p × p) (p × p) ℂ)
     using (star_alg_equiv.injective _),
   simp_rw [Psi_apply_complete_graph, _root_.map_one, one_map_transpose_eq],
   rw [← function.injective.eq_iff hφ.elim.to_matrix.symm.injective,