OAI/RepresentationTheory/FoulkesHowe/PairingConstruction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.PairingConstruction.leftMultilinear line 20

   Source documentation

   Descend the right-hand family of the normalized permanent.

   def leftMultilinear (n : ℕ) (B : X →ₗ[ℂ] Y →ₗ[ℂ] ℂ) :
       MultilinearMap ℂ (fun _ : Fin n => X) (Module.Dual ℂ (SymPow n Y)) :=
   …

   Mentions: OAI.Problem346.SymPow

2. theorem OAI.Problem346.PairingConstruction.leftMultilinear_apply_monomial line 28
3. theorem OAI.Problem346.PairingConstruction.leftMultilinear_symmetric line 36
4. def OAI.Problem346.PairingConstruction.pairing line 45

   Source documentation

   The canonical bilinear pairing induced on homogeneous symmetric powers.

   def pairing (n : ℕ) (B : X →ₗ[ℂ] Y →ₗ[ℂ] ℂ) :
       SymPow n X →ₗ[ℂ] Module.Dual ℂ (SymPow n Y) :=
   …

   Mentions: OAI.Problem346.SymPow

5. theorem OAI.Problem346.PairingConstruction.pairing_monomials line 49
6. def OAI.Problem346.PairingConstruction.dualMap line 58

   Source documentation

   The evaluation pairing of a symmetric power and the symmetric power of its dual.

   def dualMap (n : ℕ) :
       SymPow n (Module.Dual ℂ V) →ₗ[ℂ] Module.Dual ℂ (SymPow n V) :=
   …

   Mentions: OAI.Problem346.SymPow

7. theorem OAI.Problem346.PairingConstruction.dualMap_monomials line 62
8. theorem OAI.Problem346.PairingConstruction.dualMap_pure line 68
9. theorem OAI.Problem346.PairingConstruction.dualMap_injective line 82
10. theorem OAI.Problem346.PairingConstruction.dual_finrank line 86
11. def OAI.Problem346.PairingConstruction.dualEquiv line 95

    Source documentation

    Perfect duality for homogeneous symmetric powers in finite dimension.

    def dualEquiv [FiniteDimensional ℂ V] (n : ℕ) :
        SymPow n (Module.Dual ℂ V) ≃ₗ[ℂ] Module.Dual ℂ (SymPow n V) :=
    …

    Mentions: OAI.Problem346.SymPow

12. theorem OAI.Problem346.PairingConstruction.dualEquiv_apply line 99
13. theorem OAI.Problem346.PairingConstruction.dualMap_natural line 102
14. theorem OAI.Problem346.PairingConstruction.dualEquiv_natural line 117
15. theorem OAI.Problem346.PairingConstruction.comparison_of_surjection line 124

    Source documentation

    Canonical surjectivity on the dual space gives the equivariant comparison.

    theorem comparison_of_surjection [FiniteDimensional ℂ V] (a b : ℕ)
        (hsurj : ∃ μ : SymPow b (SymPow a (Module.Dual ℂ V)) →ₗ[ℂ]
          SymPow a (SymPow b (Module.Dual ℂ V)),
          IsFoulkesMap a b (Module.Dual ℂ V) μ ∧ Function.Surjective μ) :
        ∃ ι : SymPow a (SymPow b V) →ₗ[ℂ] SymPow b (SymPow a V),
          IsGLEquivariantEmbedding a b V ι := by
    …

    Mentions: OAI.Problem346.SymPow, OAI.Problem346.IsFoulkesMap, OAI.Problem346.IsGLEquivariantEmbedding