[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V : FdRep k G
g h : G
⊢ character V (h * g) = character V (g * h)
[PROOFSTEP]
simp only [trace_mul_comm, character, map_mul]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V : FdRep k G
⊢ character V 1 = ↑(finrank k (CoeSort.coe V))
[PROOFSTEP]
simp only [character, map_one, trace_one]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
⊢ character (V ⊗ W) = character V * character W
[PROOFSTEP]
ext g
[GOAL]
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
g : G
⊢ character (V ⊗ W) g = (character V * character W) g
[PROOFSTEP]
convert trace_tensorProduct' (V.ρ g) (W.ρ g)
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
⊢ character
      (Action.FunctorCategoryEquivalence.inverse.obj
        (Action.FunctorCategoryEquivalence.functor.obj V ⊗ Action.FunctorCategoryEquivalence.functor.obj W)) =
    character V * character W
[PROOFSTEP]
simp [← char_tensor]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
⊢ character V = character W
[PROOFSTEP]
ext g
[GOAL]
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ character V g = character W g
[PROOFSTEP]
simp only [character, FdRep.Iso.conj_ρ i]
[GOAL]
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ↑(trace k (CoeSort.coe V)) (↑(ρ V) g) =
    ↑(trace k (CoeSort.coe W)) (↑(LinearEquiv.conj (isoToLinearEquiv i)) (↑(ρ V) g))
[PROOFSTEP]
exact (trace_conj' (V.ρ g) _).symm
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Group G
V : FdRep k G
g h : G
⊢ character V (h * g * h⁻¹) = character V g
[PROOFSTEP]
rw [char_mul_comm, inv_mul_cancel_left]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Group G
V W : FdRep k G
g : G
⊢ character (of (linHom (ρ V) (ρ W))) g = character V g⁻¹ * character W g
[PROOFSTEP]
rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]
[GOAL]
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FdRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, character V g = ↑(finrank k { x // x ∈ invariants (ρ V) })
[PROOFSTEP]
erw [← (isProj_averageMap V.ρ).trace]
  -- Porting note: Changed `rw` to `erw`
[GOAL]
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FdRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, character V g = ↑(trace k (CoeSort.coe V)) (averageMap (ρ V))
[PROOFSTEP]
simp [character, GroupAlgebra.average, _root_.map_sum]
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹ = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
conv_lhs =>
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
    -- The average over the group of the character of a representation equals the dimension of the
      -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
| ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹
[PROOFSTEP]
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
    -- The average over the group of the character of a representation equals the dimension of the
      -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
| ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹
[PROOFSTEP]
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
    -- The average over the group of the character of a representation equals the dimension of the
      -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
| ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹
[PROOFSTEP]
enter [2, 2, g]
[GOAL]
case h
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
g : ↑G
| character V g * character W g⁻¹
[PROOFSTEP]
rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
[GOAL]
case h
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
g : ↑G
| character (of (dual (ρ W)) ⊗ V) g
[PROOFSTEP]
rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
  -- The average over the group of the character of a representation equals the dimension of the
    -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character (of (linHom (ρ W) (ρ V))) g = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
rw [average_char_eq_finrank_invariants]
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k { x // x ∈ invariants (ρ (of (linHom (ρ W) (ρ V)))) }) = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
rw [show (of (linHom W.ρ V.ρ)).ρ = linHom W.ρ V.ρ from FdRep.of_ρ (linHom W.ρ V.ρ)]
  -- The space of invariants of `Hom(W, V)` is the subspace of `G`-equivariant linear maps,
    -- `Hom_G(W, V)`.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k { x // x ∈ invariants (linHom (ρ W) (ρ V)) }) = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
erw [(linHom.invariantsEquivFdRepHom W V).finrank_eq]
  -- Porting note: Changed `rw` to `erw`
    -- By Schur's Lemma, the dimension of `Hom_G(W, V)` is `1` is `V ≅ W` and `0` otherwise.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k (W ⟶ V)) = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]
