OAI/RepresentationTheory/FoulkesHowe/SymmetricLift.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.SymmetricLift.tupleExponent line 14
2. lemma OAI.Problem346.SymmetricLift.tupleExponent_apply line 17
3. lemma OAI.Problem346.SymmetricLift.exists_perm_of_exponent_eq line 23
4. def OAI.Problem346.SymmetricLift.liftValues line 36
5. lemma OAI.Problem346.SymmetricLift.liftValues_tuple line 41
6. def OAI.Problem346.SymmetricLift.liftOnAlgebra line 53
7. lemma OAI.Problem346.SymmetricLift.liftOnAlgebra_basis line 59
8. lemma OAI.Problem346.SymmetricLift.liftOnAlgebra_monomial line 76
9. theorem OAI.Problem346.exists_symPow_lift line 93

   Source documentation

   A symmetric multilinear map descends to the homogeneous symmetric-power submodule.

   theorem exists_symPow_lift {n : ℕ} {V W : Type*}
       [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
       (T : MultilinearMap ℂ (fun _ : Fin n => V) W)
       (hT : ∀ (σ : Equiv.Perm (Fin n)) (v : Fin n → V), T (fun i => v (σ i)) = T v) :
       ∃ L : SymPow n V →ₗ[ℂ] W, ∀ v, L (symMonomial n V v) = T v := by
   …

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

10. def OAI.Problem346.symPowLift line 104

    Source documentation

    A chosen linear descent of a symmetric multilinear map.

    def symPowLift {n : ℕ} {V W : Type*}
        [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
        (T : MultilinearMap ℂ (fun _ : Fin n => V) W)
        (hT : ∀ (σ : Equiv.Perm (Fin n)) (v : Fin n → V), T (fun i => v (σ i)) = T v) :
        SymPow n V →ₗ[ℂ] W :=
    …

    Mentions: OAI.Problem346.SymPow

11. theorem OAI.Problem346.symPowLift_symMonomial line 111
12. theorem OAI.Problem346.SymmetricLift.linearMap_ext line 121

    Source documentation

    Linear maps out of a symmetric power are determined by products.

    theorem linearMap_ext {n : ℕ} {V W : Type*}
        [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
        {f g : SymPow n V →ₗ[ℂ] W}
        (h : ∀ v, f (symMonomial n V v) = g (symMonomial n V v)) : f = g := by
    …

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

13. def OAI.Problem346.symmetricMultilinearSubmodule line 132

    Source documentation

    The submodule of multilinear maps invariant under permutations of their arguments.

    def symmetricMultilinearSubmodule (n : ℕ) (V W : Type*)
        [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W] :
        Submodule ℂ (MultilinearMap ℂ (fun _ : Fin n => V) W) where
    …

14. def OAI.Problem346.symPowLiftLinear line 146

    Source documentation

    Descent from symmetric multilinear maps is linear in the map being descended.

    def symPowLiftLinear (n : ℕ) (V W : Type*)
        [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W] :
        symmetricMultilinearSubmodule n V W →ₗ[ℂ] (SymPow n V →ₗ[ℂ] W) where
    …

    Mentions: OAI.Problem346.symmetricMultilinearSubmodule, OAI.Problem346.SymPow

15. theorem OAI.Problem346.symPowLiftLinear_symMonomial line 163