OAI/RepresentationTheory/FoulkesHowe/DualComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.canonicalSymPowDualMap_adjoint line 10

   Source documentation

   The canonical symmetric-power pairing is natural for arbitrary linear maps.

   theorem canonicalSymPowDualMap_adjoint (n : ℕ) {V W : Type*}
       [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
       (A : V →ₗ[ℂ] W) (p : SymPow n (Module.Dual ℂ W)) (q : SymPow n V) :
       symPowDualMap n V (symPowMap n A.dualMap p) q =
         symPowDualMap n W p (symPowMap n A q) := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.symPowDualMap, OAI.Problem346.symPowMap

2. theorem OAI.Problem346.canonicalSymPowDualEquiv_adjoint line 28

   Source documentation

   The perfect-pairing equivalence has the same adjointness identity.

   theorem canonicalSymPowDualEquiv_adjoint (n : ℕ) {V W : Type*}
       [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
       [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
       (A : V →ₗ[ℂ] W) (p : SymPow n (Module.Dual ℂ W)) (q : SymPow n V) :
       symPowDualEquiv n V (symPowMap n A.dualMap p) q =
         symPowDualEquiv n W p (symPowMap n A q) :=
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.symPowDualEquiv, OAI.Problem346.symPowMap

3. def OAI.Problem346.concretePlethysmDualEquiv line 37

   Source documentation

   Canonical duality on a nested symmetric power.

   def concretePlethysmDualEquiv (outer inner : ℕ) (V : Type*)
       [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] :
       SymPow outer (SymPow inner (Module.Dual ℂ V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow outer (SymPow inner V)) :=
   …

   Mentions: OAI.Problem346.SymPow

4. theorem OAI.Problem346.concretePlethysmDualEquiv_adjoint line 44
5. theorem OAI.Problem346.comparison_embedding_of_dual_foulkes_surjection line 60

   Source documentation

   A canonical surjection at the dual vector space supplies the required GL-equivariant comparison embedding, using the concrete perfect pairings.

   theorem comparison_embedding_of_dual_foulkes_surjection (a b : ℕ) (V : Type*)
       [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
       (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 ι :=
   …

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