OAI/RepresentationTheory/FoulkesHowe/PlethysmDual.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.PlethysmDual.liftDualEquiv line 26

   Source documentation

   Lift a perfect-duality chart through a symmetric power using the canonical duality chart for that symmetric power.

   def liftDualEquiv (n : ℕ) (e : W ≃ₗ[ℂ] Module.Dual ℂ V)
       (d : SymPow n (Module.Dual ℂ V) ≃ₗ[ℂ] Module.Dual ℂ (SymPow n V)) :
       SymPow n W ≃ₗ[ℂ] Module.Dual ℂ (SymPow n V) :=
   …

   Mentions: OAI.Problem346.SymPow

2. theorem OAI.Problem346.PlethysmDual.liftDualEquiv_adjoint line 33

   Source documentation

   Adjointness is preserved when a perfect pairing is lifted through a symmetric power whose duality chart is natural for the given map.

   theorem liftDualEquiv_adjoint (n : ℕ) (e : W ≃ₗ[ℂ] Module.Dual ℂ V)
       (d : SymPow n (Module.Dual ℂ V) ≃ₗ[ℂ] Module.Dual ℂ (SymPow n V))
       (A : V →ₗ[ℂ] V) (A' : W →ₗ[ℂ] W)
       (he : ∀ x y, e (A' x) y = e x (A y))
       (hd : ∀ x y, d (symPowMap n A.dualMap x) y = d x (symPowMap n A y))
       (x : SymPow n W) (y : SymPow n V) :
       liftDualEquiv n e d (symPowMap n A' x) y =
         liftDualEquiv n e d x (symPowMap n A y) := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.symPowMap, OAI.Problem346.PlethysmDual.liftDualEquiv

3. def OAI.Problem346.PlethysmDual.plethysmDualEquivOf line 56

   Source documentation

   The duality chart for a plethysm is the composite of its inner and outer one-level duality charts.

   def plethysmDualEquivOf (outer inner : ℕ)
       (e : SymPow inner (Module.Dual ℂ V) ≃ₗ[ℂ] Module.Dual ℂ (SymPow inner V))
       (d : SymPow outer (Module.Dual ℂ (SymPow inner V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow outer (SymPow inner V))) :
       SymPow outer (SymPow inner (Module.Dual ℂ V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow outer (SymPow inner V)) :=
   …

   Mentions: OAI.Problem346.SymPow

4. theorem OAI.Problem346.PlethysmDual.plethysmDualEquivOf_adjoint line 67

   Source documentation

   Naturality of each level gives the adjoint-action identity for the plethysm pairing. The dual automorphism here is the ordinary dual map, not the inverse contragredient; this is precisely the adjoint identity.

   theorem plethysmDualEquivOf_adjoint (outer inner : ℕ)
       (e : SymPow inner (Module.Dual ℂ V) ≃ₗ[ℂ] Module.Dual ℂ (SymPow inner V))
       (d : SymPow outer (Module.Dual ℂ (SymPow inner V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow outer (SymPow inner V)))
       (g : V ≃ₗ[ℂ] V)
       (he : ∀ x y, e (symPowMap inner g.dualMap.toLinearMap x) y =
         e x (symPowMap inner g.toLinearMap y))
       (hd : ∀ x y,
         d (symPowMap outer (symPowMap inner g.toLinearMap).dualMap x) y =
         d x (symPowMap outer (symPowMap inner g.toLinearMap) y))
       (x : SymPow outer (SymPow inner (Module.Dual ℂ V)))
       (y : SymPow outer (SymPow inner V)) :
   …

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

5. theorem OAI.Problem346.PlethysmDual.exists_embedding_of_dual_surjection line 88

   Source documentation

   The comparison embedding follows formally from a surjection on the dual vector space and compatible perfect pairings on the two plethysms.

   theorem exists_embedding_of_dual_surjection (a b : ℕ)
       [Module.IsReflexive ℂ (SymPow b (SymPow a V))]
       [Module.IsReflexive ℂ (SymPow a (SymPow b V))]
       (e : SymPow b (SymPow a (Module.Dual ℂ V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow b (SymPow a V)))
       (f : SymPow a (SymPow b (Module.Dual ℂ V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow a (SymPow b V)))
       (he : ∀ (g : V ≃ₗ[ℂ] V) x y,
         e (plethysmAction b a g.dualMap x) y = e x (plethysmAction b a g y))
       (hf : ∀ (g : V ≃ₗ[ℂ] V) x y,
         f (plethysmAction a b g.dualMap x) y = f x (plethysmAction a b g y))
       (μ : SymPow b (SymPow a (Module.Dual ℂ V)) →ₗ[ℂ]
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.plethysmAction

6. theorem OAI.Problem346.PlethysmDual.comparison_of_dual_charts line 125

   Source documentation

   With finite-dimensionality and canonical-map naturality available, only the two perfect-duality charts and their adjointness remain to construct the comparison embedding from canonical surjectivity on the dual space.

   theorem comparison_of_dual_charts (a b : ℕ) [FiniteDimensional ℂ V]
       (e : SymPow b (SymPow a (Module.Dual ℂ V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow b (SymPow a V)))
       (f : SymPow a (SymPow b (Module.Dual ℂ V)) ≃ₗ[ℂ]
         Module.Dual ℂ (SymPow a (SymPow b V)))
       (he : ∀ (g : V ≃ₗ[ℂ] V) x y,
         e (plethysmAction b a g.dualMap x) y = e x (plethysmAction b a g y))
       (hf : ∀ (g : V ≃ₗ[ℂ] V) x y,
         f (plethysmAction a b g.dualMap x) y = f x (plethysmAction a b g y))
       (hsurj : ∃ μ : SymPow b (SymPow a (Module.Dual ℂ V)) →ₗ[ℂ]
         SymPow a (SymPow b (Module.Dual ℂ V)),
         IsFoulkesMap a b (Module.Dual ℂ V) μ ∧ Function.Surjective μ) :
   …

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