[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix b b) f) = trace (↑(toMatrix b b) (comp (comp id f) id))
[PROOFSTEP]
rw [LinearMap.id_comp, LinearMap.comp_id]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix b b) (comp (comp id f) id)) = trace (↑(toMatrix c b) id * ↑(toMatrix c c) f * ↑(toMatrix b c) id)
[PROOFSTEP]
rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c b) id * ↑(toMatrix c c) f * ↑(toMatrix b c) id) =
    trace (↑(toMatrix c c) f * ↑(toMatrix b c) id * ↑(toMatrix c b) id)
[PROOFSTEP]
rw [Matrix.mul_assoc, Matrix.trace_mul_comm]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c c) f * ↑(toMatrix b c) id * ↑(toMatrix c b) id) = trace (↑(toMatrix c c) (comp (comp f id) id))
[PROOFSTEP]
rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c c) (comp (comp f id) id)) = trace (↑(toMatrix c c) f)
[PROOFSTEP]
rw [LinearMap.comp_id, LinearMap.comp_id]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
⊢ ↑(trace R M) f = Matrix.trace (↑(toMatrix b b) f)
[PROOFSTEP]
have : ∃ s : Finset M, Nonempty (Basis s R M) := ⟨s, ⟨b⟩⟩
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) f = Matrix.trace (↑(toMatrix b b) f)
[PROOFSTEP]
rw [trace, dif_pos this, ← traceAux_def]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(traceAux R (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose this } R M)))) f = ↑(traceAux R b) f
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ traceAux R (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose this } R M))) = traceAux R b
[PROOFSTEP]
apply traceAux_eq
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ↑(trace R M) f = Matrix.trace (↑(toMatrix b b) f)
[PROOFSTEP]
rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
  traceAux_eq R b b.reindexFinsetRange]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
[PROOFSTEP]
let ⟨s, ⟨b⟩⟩ := H
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
[PROOFSTEP]
simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ Matrix.trace (↑(toMatrix b b) f * ↑(toMatrix b b) g) = Matrix.trace (↑(toMatrix b b) g * ↑(toMatrix b b) f)
[PROOFSTEP]
apply Matrix.trace_mul_comm
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
[PROOFSTEP]
rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g h : M →ₗ[R] M
⊢ ↑(trace R M) (f * g * h) = ↑(trace R M) (h * f * g)
[PROOFSTEP]
rw [LinearMap.trace_mul_comm, ← mul_assoc]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g h : M →ₗ[R] M
⊢ ↑(trace R M) (f * (g * h)) = ↑(trace R M) (h * (f * g))
[PROOFSTEP]
rw [← mul_assoc, LinearMap.trace_mul_comm]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ ↑(trace R M) (↑f * g * ↑f⁻¹) = ↑(trace R M) g
[PROOFSTEP]
rw [trace_mul_comm]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ ↑(trace R M) (↑f⁻¹ * (↑f * g)) = ↑(trace R M) g
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
[PROOFSTEP]
classical
cases nonempty_fintype ι
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
rintro ⟨i, j⟩
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
by_cases hij : i = j
· rw [hij]
  simp
rw [Matrix.StdBasisMatrix.trace_zero j i (1 : R) hij]
simp [Finsupp.single_eq_pi_single, hij]
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
[PROOFSTEP]
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
[GOAL]
case intro
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i) =
      ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i)
[PROOFSTEP]
rintro ⟨i, j⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j)) =
    ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j))
[PROOFSTEP]
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
[GOAL]
case intro.mk
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(trace R M) (↑(dualTensorHom R M M) (Basis.coord b i ⊗ₜ[R] ↑b j)) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
[GOAL]
case intro.mk
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
rw [hij]
[GOAL]
case pos
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j j 1) = ↑(contractLeft R M) (Basis.coord b j ⊗ₜ[R] ↑b j)
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
rw [Matrix.StdBasisMatrix.trace_zero j i (1 : R) hij]
[GOAL]
case neg
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ 0 = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
simp [Finsupp.single_eq_pi_single, hij]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R M
⊢ trace R M = comp (contractLeft R M) ↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b))
[PROOFSTEP]
simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
x : Module.Dual R M ⊗[R] M
⊢ ↑(trace R M) (↑(dualTensorHom R M M) x) = ↑(contractLeft R M) x
[PROOFSTEP]
rw [← comp_apply, trace_eq_contract]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Subsingleton R
⊢ ↑(trace R M) 1 = ↑(finrank R M)
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
have b := Module.Free.chooseBasis R M
[GOAL]
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R M) R M
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]
[GOAL]
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(Fintype.card (Module.Free.ChooseBasisIndex R M))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ ↑(trace R M) id = ↑(finrank R M)
[PROOFSTEP]
rw [← one_eq_id, trace_one]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
[PROOFSTEP]
let e := dualTensorHomEquiv R M M
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
[PROOFSTEP]
have h : Function.Surjective e.toLinearMap := e.surjective
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
[PROOFSTEP]
refine' (cancel_right h).1 _
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e = comp (trace R M) ↑e
[PROOFSTEP]
ext f m
[GOAL]
case a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
f : Module.Dual R M
m : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e)) f) m =
    ↑(↑(AlgebraTensorModule.curry (comp (trace R M) ↑e)) f) m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ comp (trace R (M × N)) (prodMapLinear R M N M N R) = comp (coprod id id) (prodMap (trace R M) (trace R N))
[PROOFSTEP]
let e := (dualTensorHomEquiv R M M).prod (dualTensorHomEquiv R N N)
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
⊢ comp (trace R (M × N)) (prodMapLinear R M N M N R) = comp (coprod id id) (prodMap (trace R M) (trace R N))
[PROOFSTEP]
have h : Function.Surjective e.toLinearMap := e.surjective
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
⊢ comp (trace R (M × N)) (prodMapLinear R M N M N R) = comp (coprod id id) (prodMap (trace R M) (trace R N))
[PROOFSTEP]
refine' (cancel_right h).1 _
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
⊢ comp (comp (trace R (M × N)) (prodMapLinear R M N M N R)) ↑e =
    comp (comp (coprod id id) (prodMap (trace R M) (trace R N))) ↑e
[PROOFSTEP]
ext
[GOAL]
case hl.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
x✝¹ : Module.Dual R M
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (trace R (M × N)) (prodMapLinear R M N M N R)) ↑e)
                (inl R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝ =
    ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (coprod id id) (prodMap (trace R M) (trace R N))) ↑e)
                (inl R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [dualTensorHomEquiv, LinearEquiv.coe_prod, dualTensorHomEquivOfBasis_toLinearMap,
  AlgebraTensorModule.curry_apply, curry_apply, coe_restrictScalars, coe_comp, coe_inl, Function.comp_apply,
  prodMap_apply, map_zero, prodMapLinear_apply, dualTensorHom_prodMap_zero, trace_eq_contract_apply, contractLeft_apply,
  fst_apply, coprod_apply, id_coe, id_eq, add_zero]
[GOAL]
case hr.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
x✝¹ : Module.Dual R N
x✝ : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (trace R (M × N)) (prodMapLinear R M N M N R)) ↑e)
                (inr R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝ =
    ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (coprod id id) (prodMap (trace R M) (trace R N))) ↑e)
                (inr R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [dualTensorHomEquiv, LinearEquiv.coe_prod, dualTensorHomEquivOfBasis_toLinearMap,
  AlgebraTensorModule.curry_apply, curry_apply, coe_restrictScalars, coe_comp, coe_inr, Function.comp_apply,
  prodMap_apply, map_zero, prodMapLinear_apply, zero_prodMap_dualTensorHom, trace_eq_contract_apply, contractLeft_apply,
  snd_apply, coprod_apply, id_coe, id_eq, zero_add]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
[PROOFSTEP]
have h := ext_iff.1 (trace_prodMap R M N) (f, g)
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  ↑(comp (trace R (M × N)) (prodMapLinear R M N M N R)) (f, g) =
    ↑(comp (coprod id id) (prodMap (trace R M) (trace R N))) (f, g)
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, prodMap_apply, coprod_apply, id_coe, id.def, prodMapLinear_apply] at h 
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h : ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N)) = compl₁₂ (lsmul R R) (trace R M) (trace R N)
[PROOFSTEP]
apply
  (compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective)
      (show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).1
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compl₁₂ (compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M) (dualTensorHom R N N) =
    compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N)
[PROOFSTEP]
ext f m g n
[GOAL]
case a.h.h.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : Module.Dual R M
m : M
g : Module.Dual R N
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n
[PROOFSTEP]
simp only [AlgebraTensorModule.curry_apply, toFun_eq_coe, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply,
  compr₂_apply, mapBilinear_apply, trace_eq_contract_apply, contractLeft_apply, lsmul_apply, Algebra.id.smul_eq_mul,
  map_dualTensorHom, dualDistrib_apply]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compr₂ (llcomp R M N M) (trace R M) = compr₂ (flip (llcomp R N M N)) (trace R N)
[PROOFSTEP]
apply
  (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
      (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N) =
    compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N)
[PROOFSTEP]
ext g m f n
[GOAL]
case a.h.h.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
g : Module.Dual R N
m : M
f : Module.Dual R M
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N)))
                    g)
                m))
          f)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                          (dualTensorHom R M N)))
                    g)
                m))
          f)
      n
[PROOFSTEP]
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply, compr₂_apply,
  llcomp_apply', comp_dualTensorHom, map_smulₛₗ, RingHom.id_apply, trace_eq_contract_apply, contractLeft_apply,
  smul_eq_mul, mul_comm, flip_apply]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
⊢ ↑(trace R (Module.Dual R M)) (↑Module.Dual.transpose f) = ↑(trace R M) f
[PROOFSTEP]
rw [← comp_apply, trace_transpose]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
[PROOFSTEP]
have h := ext_iff.1 (ext_iff.1 (trace_tensorProduct R M N) f) g
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  ↑(↑(compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) f) g = ↑(↑(compl₁₂ (lsmul R R) (trace R M) (trace R N)) f) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
[PROOFSTEP]
simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply, Algebra.id.smul_eq_mul] at h 
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h : ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
[PROOFSTEP]
have h := ext_iff.1 (ext_iff.1 (trace_comp_comm R M N) g) f
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(↑(compr₂ (llcomp R M N M) (trace R M)) g) f = ↑(↑(compr₂ (flip (llcomp R N M N)) (trace R N)) g) f
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
[PROOFSTEP]
simp only [llcomp_apply', compr₂_apply, flip_apply] at h 
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ ↑(trace R P) (comp g (comp f h)) = ↑(trace R N) (comp f (comp h g))
[PROOFSTEP]
rw [trace_comp_comm', comp_assoc]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ ↑(trace R P) (comp (comp g f) h) = ↑(trace R M) (comp (comp h g) f)
[PROOFSTEP]
rw [trace_comp_comm', ← comp_assoc]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ ↑(trace R N) (↑(LinearEquiv.conj e) f) = ↑(trace R M) f
[PROOFSTEP]
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm,
  LinearEquiv.refl_toLinearMap, id_comp]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
M : Type u_2
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
inst✝¹¹ : AddCommGroup P
inst✝¹⁰ : Module R P
ι : Type u_5
inst✝⁹ : Module.Free R M
inst✝⁸ : Module.Finite R M
inst✝⁷ : Module.Free R N
inst✝⁶ : Module.Finite R N
inst✝⁵ : Module.Free R P
inst✝⁴ : Module.Finite R P
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Module.Free R { x // x ∈ p }
inst✝² : Module.Finite R { x // x ∈ p }
inst✝¹ : Module.Free R { x // x ∈ ker f }
inst✝ : Module.Finite R { x // x ∈ ker f }
⊢ ↑(LinearMap.trace R M) f = ↑(finrank R { x // x ∈ p })
[PROOFSTEP]
rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
