[GOAL]
k : Type u
inst✝⁹ : CommRing k
G : Type u
inst✝⁸ : Group G
V : Type v
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
g : G
v : V
⊢ ↑(conjugate π g) (↑i v) = v
[PROOFSTEP]
rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, mul_left_inv, ← one_def, one_smul]
[GOAL]
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝ : Fintype G
g : G
v : W
⊢ ↑(sumOfConjugates G π) (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • ↑(sumOfConjugates G π) v
[PROOFSTEP]
simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
[GOAL]
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝ : Fintype G
g : G
v : W
⊢ ∑ x : G, MonoidAlgebra.single x⁻¹ 1 • ↑π (MonoidAlgebra.single x 1 • MonoidAlgebra.single g 1 • v) =
    ∑ x : G, MonoidAlgebra.single g 1 • MonoidAlgebra.single x⁻¹ 1 • ↑π (MonoidAlgebra.single x 1 • v)
[PROOFSTEP]
refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
[GOAL]
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i✝ : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i✝ v) = v
inst✝ : Fintype G
g : G
v : W
i : G
⊢ MonoidAlgebra.single i⁻¹ 1 • ↑π (MonoidAlgebra.single i 1 • MonoidAlgebra.single g 1 • v) =
    MonoidAlgebra.single g 1 •
      MonoidAlgebra.single ((fun x => x * g) i)⁻¹ 1 • ↑π (MonoidAlgebra.single ((fun x => x * g) i) 1 • v)
[PROOFSTEP]
simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : W
⊢ ↑(equivariantProjection G π) v = ⅟↑(Fintype.card G) • ∑ g : G, ↑(conjugate π g) v
[PROOFSTEP]
simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
⊢ ↑(equivariantProjection G π) (↑i v) = v
[PROOFSTEP]
rw [equivariantProjection_apply]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
⊢ ⅟↑(Fintype.card G) • ∑ g : G, ↑(conjugate π g) (↑i v) = v
[PROOFSTEP]
simp only [conjugate_i π i h]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
⊢ ⅟↑(Fintype.card G) • ∑ x : G, v = v
[PROOFSTEP]
rw [Finset.sum_const, Finset.card_univ, nsmul_eq_smul_cast k, smul_smul, Invertible.invOf_mul_self, one_smul]
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
⊢ ∃ g, LinearMap.comp g f = LinearMap.id
[PROOFSTEP]
obtain ⟨φ, hφ⟩ :=
  (f.restrictScalars k).exists_leftInverse_of_injective <| by
    simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
⊢ LinearMap.ker (↑k f) = ⊥
[PROOFSTEP]
simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
φ : W →ₗ[k] V
hφ : LinearMap.comp φ (↑k f) = LinearMap.id
⊢ ∃ g, LinearMap.comp g f = LinearMap.id
[PROOFSTEP]
refine ⟨φ.equivariantProjection G, FunLike.ext _ _ ?_⟩
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
φ : W →ₗ[k] V
hφ : LinearMap.comp φ (↑k f) = LinearMap.id
⊢ ∀ (x : V), ↑(LinearMap.comp (LinearMap.equivariantProjection G φ) f) x = ↑LinearMap.id x
[PROOFSTEP]
exact φ.equivariantProjection_condition G _ <| FunLike.congr_fun hφ
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
⊢ ∃ q, IsCompl p q
[PROOFSTEP]
have : IsScalarTower k (MonoidAlgebra k G) p := p.isScalarTower'
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
this : IsScalarTower k (MonoidAlgebra k G) { x // x ∈ p }
⊢ ∃ q, IsCompl p q
[PROOFSTEP]
rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
this : IsScalarTower k (MonoidAlgebra k G) { x // x ∈ p }
f : V →ₗ[MonoidAlgebra k G] { x // x ∈ p }
hf : LinearMap.comp f (Submodule.subtype p) = LinearMap.id
⊢ ∃ q, IsCompl p q
[PROOFSTEP]
refine ⟨LinearMap.ker f, LinearMap.isCompl_of_proj ?_⟩
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
this : IsScalarTower k (MonoidAlgebra k G) { x // x ∈ p }
f : V →ₗ[MonoidAlgebra k G] { x // x ∈ p }
hf : LinearMap.comp f (Submodule.subtype p) = LinearMap.id
⊢ ∀ (x : { x // x ∈ p }), ↑f ↑x = x
[PROOFSTEP]
exact FunLike.congr_fun hf
