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
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
have : IsScalarTower k (MonoidAlgebra k G) p := p.isScalarTower'
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
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
rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
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
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
refine ⟨LinearMap.ker f, LinearMap.isCompl_of_proj ?_⟩
no goals
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
exact FunLike.congr_fun hf