exists_isCompl — Mathlib

English

For v ∈ W, applying the equivariant projection yields the average-conjugate expression: (π.equivariantProjection G) v = |G|^{-1} ∑_{g∈G} (π.conjugate g) v.

Русский

Для v ∈ W применение эквиаривантной проекции даёт усреднённое выражение конъюгатов: (π.equivariantProjection G) v = |G|^{-1} ∑_{g∈G} (π^g) v.

LaTeX

$$$\text{equivariantProjection_apply } G π v = \mathrm{Ring.inverse} (Fintype.card G : k) \cdot \sum_{g : G} π.conjugate g v$$$

Lean4

theorem exists_isCompl (p : Submodule (MonoidAlgebra k G) V) : ∃ q : Submodule (MonoidAlgebra k G) V, IsCompl p q :=
  by
  rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
  exact ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩

Похожие утверждения