[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ Finsupp.single g 1 * average k G = average k G
[PROOFSTEP]
simp only [mul_one, Finset.mul_sum, Algebra.mul_smul_comm, average, MonoidAlgebra.of_apply, Finset.sum_congr,
  MonoidAlgebra.single_mul_single]
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
[PROOFSTEP]
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • Finset.sum Finset.univ f
[PROOFSTEP]
show ⅟(Fintype.card G : k) • ∑ x : G, f (g * x) = ⅟(Fintype.card G : k) • ∑ x : G, f x
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (g * x) = ⅟↑(Fintype.card G) • ∑ x : G, f x
[PROOFSTEP]
rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) _]
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ average k G * Finsupp.single g 1 = average k G
[PROOFSTEP]
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply, Finset.sum_congr,
  MonoidAlgebra.single_mul_single]
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
[PROOFSTEP]
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • Finset.sum Finset.univ f
[PROOFSTEP]
show ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (x * g) = ⅟↑(Fintype.card G) • ∑ x : G, f x
[PROOFSTEP]
rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
a✝ b✝ : V
hv : a✝ ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v}
hw : b✝ ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v}
g : G
⊢ ↑(↑ρ g) (a✝ + b✝) = a✝ + b✝
[PROOFSTEP]
simp only [hv g, hw g, map_add]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(↑ρ g) 0 = 0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
v : V
hv :
  v ∈
    {
          toAddSubsemigroup :=
            { carrier := {v | ∀ (g : G), ↑(↑ρ g) v = v},
              add_mem' :=
                (_ :
                  ∀ {a b : V},
                    a ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v} →
                      b ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v} → ∀ (g : G), ↑(↑ρ g) (a + b) = a + b) },
          zero_mem' := (_ : ∀ (g : G), ↑(↑ρ g) 0 = 0) }.toAddSubsemigroup.carrier
g : G
⊢ ↑(↑ρ g) (r • v) = r • v
[PROOFSTEP]
simp only [hv g, LinearMap.map_smulₛₗ, RingHom.id_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
v : V
⊢ v ∈ invariants ρ ↔ ∀ (g : G), ↑(↑ρ g) v = v
[PROOFSTEP]
rfl
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
⊢ (invariants ρ).toAddSubmonoid.toAddSubsemigroup.carrier = ⋂ (g : G), Function.fixedPoints ↑(↑ρ g)
[PROOFSTEP]
ext
[GOAL]
case h
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ x✝ ∈ (invariants ρ).toAddSubmonoid.toAddSubsemigroup.carrier ↔ x✝ ∈ ⋂ (g : G), Function.fixedPoints ↑(↑ρ g)
[PROOFSTEP]
simp [Function.IsFixedPt]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ ↑(↑ρ g) (↑(averageMap ρ) v) = ↑(averageMap ρ) v
[PROOFSTEP]
rw [averageMap, ← asAlgebraHom_single_one, ← LinearMap.mul_apply, ← map_mul (asAlgebraHom ρ), mul_average_left]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : v ∈ invariants ρ
⊢ ↑(averageMap ρ) v = v
[PROOFSTEP]
rw [mem_invariants] at hv 
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : ∀ (g : G), ↑(↑ρ g) v = v
⊢ ↑(averageMap ρ) v = v
[PROOFSTEP]
simp [average, map_sum, hv, Finset.card_univ, nsmul_eq_smul_cast k _ v, smul_smul]
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f = f ↔ LinearMap.comp f (↑(Rep.ρ X) g) = LinearMap.comp (↑(Rep.ρ Y) g) f
[PROOFSTEP]
dsimp
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ LinearMap.comp (↑(Rep.ρ Y) g) (LinearMap.comp f (↑(Rep.ρ X) g⁻¹)) = f ↔
    LinearMap.comp f (↑(Rep.ρ X) g) = LinearMap.comp (↑(Rep.ρ Y) g) f
[PROOFSTEP]
erw [← ρAut_apply_inv]
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ LinearMap.comp (↑(Rep.ρ Y) g) (LinearMap.comp f (↑(ρAut X) g).inv) = f ↔
    LinearMap.comp f (↑(Rep.ρ X) g) = LinearMap.comp (↑(Rep.ρ Y) g) f
[PROOFSTEP]
rw [← LinearMap.comp_assoc, ← ModuleCat.comp_def, ← ModuleCat.comp_def, Iso.inv_comp_eq, ρAut_apply_hom]
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ f ≫ ↑(Rep.ρ Y) g = ↑X.ρ g ≫ f ↔ LinearMap.comp f (↑(Rep.ρ X) g) = f ≫ ↑(Rep.ρ Y) g
[PROOFSTEP]
exact comm
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝ : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }
⊢ (fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => Hom.mk ↑f,
                map_add' :=
                  (_ :
                    ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                      (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
            map_smul' :=
              (_ :
                ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                  AddHom.toFun
                      { toFun := fun f => Hom.mk ↑f,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                              (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                      (x • x_1) =
                    AddHom.toFun
                      { toFun := fun f => Hom.mk ↑f,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                              (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                      (x • x_1)) }.toAddHom
        x✝) =
    x✝
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝ : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }
⊢ ↑((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
        (AddHom.toFun
          {
              toAddHom :=
                { toFun := fun f => Hom.mk ↑f,
                  map_add' :=
                    (_ :
                      ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                        (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
              map_smul' :=
                (_ :
                  ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                    AddHom.toFun
                        { toFun := fun f => Hom.mk ↑f,
                          map_add' :=
                            (_ :
                              ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                        (x • x_1) =
                      AddHom.toFun
                        { toFun := fun f => Hom.mk ↑f,
                          map_add' :=
                            (_ :
                              ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                        (x • x_1)) }.toAddHom
          x✝)) =
    ↑x✝
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝¹ : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }
x✝ : CoeSort.coe X
⊢ ↑↑((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => Hom.mk ↑f,
                      map_add' :=
                        (_ :
                          ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                            (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
                  map_smul' :=
                    (_ :
                      ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                        AddHom.toFun
                            { toFun := fun f => Hom.mk ↑f,
                              map_add' :=
                                (_ :
                                  ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                    (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                            (x • x_1) =
                          AddHom.toFun
                            { toFun := fun f => Hom.mk ↑f,
                              map_add' :=
                                (_ :
                                  ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                    (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                            (x • x_1)) }.toAddHom
              x✝¹))
      x✝ =
    ↑↑x✝¹ x✝
[PROOFSTEP]
rfl
  -- Porting note: Added `apply Subtype.ext`
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝ : X ⟶ Y
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => Hom.mk ↑f,
              map_add' :=
                (_ :
                  ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                    (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
          map_smul' :=
            (_ :
              ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                AddHom.toFun
                    { toFun := fun f => Hom.mk ↑f,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                            (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                    (x • x_1) =
                  AddHom.toFun
                    { toFun := fun f => Hom.mk ↑f,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                            (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                    (x • x_1)) }.toAddHom
      ((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) }) x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝¹ : X ⟶ Y
x✝ : ↑X.V
⊢ ↑(AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => Hom.mk ↑f,
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                          (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                      AddHom.toFun
                          { toFun := fun f => Hom.mk ↑f,
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                  (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => Hom.mk ↑f,
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                  (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            ((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
              x✝¹)).hom
      x✝ =
    ↑x✝¹.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k : Type u
inst✝ : Field k
G : GroupCat
X Y : FdRep k ↑G
⊢ { x // x ∈ invariants (linHom (FdRep.ρ X) (FdRep.ρ Y)) } ≃ₗ[k] X ⟶ Y
[PROOFSTEP]
rw [← FdRep.forget₂_ρ, ← FdRep.forget₂_ρ]
  -- Porting note: The original version used `linHom.invariantsEquivRepHom _ _ ≪≫ₗ`
[GOAL]
k : Type u
inst✝ : Field k
G : GroupCat
X Y : FdRep k ↑G
⊢ { x //
      x ∈
        invariants
          (linHom (Rep.ρ ((forget₂ (FdRep k ↑G) (Rep k ↑G)).obj X))
            (Rep.ρ ((forget₂ (FdRep k ↑G) (Rep k ↑G)).obj Y))) } ≃ₗ[k]
    X ⟶ Y
[PROOFSTEP]
exact
  linHom.invariantsEquivRepHom ((forget₂ (FdRep k G) (Rep k G)).obj X) ((forget₂ (FdRep k G) (Rep k G)).obj Y) ≪≫ₗ
    FdRep.forget₂HomLinearEquiv X Y
