OAI/RepresentationTheory/FoulkesHowe/GeneratorLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.exists_symPow_lift_on_spanning line 12

   Source documentation

   A separately linearly extendible symmetric formula on spanning generators induces a linear map out of the homogeneous symmetric power.

   theorem exists_symPow_lift_on_spanning
       {n : ℕ} {X V W : Type*} [AddCommGroup V] [Module ℂ V]
       [AddCommGroup W] [Module ℂ W]
       (s : X → V) (hs : Submodule.span ℂ (Set.range s) = ⊤)
       (F : (Fin n → X) → W)
       (hlinear : ∀ x : Fin n → X, ∀ i : Fin n,
         ∃ L : V →ₗ[ℂ] W, ∀ y, L (s y) = F (Function.update x i y))
       (hsym : ∀ (σ : Equiv.Perm (Fin n)) (x : Fin n → X),
         F (fun i => x (σ i)) = F x) :
       ∃ L : SymPow n V →ₗ[ℂ] W, ∀ x : Fin n → X,
         L (symMonomial n V (fun i => s (x i))) = F x := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.symMonomial