OAI/RepresentationTheory/FoulkesHowe/Functoriality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.symAlgMap line 15

   Source documentation

   The algebra map induced by a complex-linear map.

   def symAlgMap (f : V →ₗ[ℂ] W) : SymmetricAlgebra ℂ V →ₐ[ℂ] SymmetricAlgebra ℂ W :=
   …

2. theorem OAI.Problem346.symAlgMap_ι line 18
3. theorem OAI.Problem346.symAlgMap_symMonomialRaw line 22
4. def OAI.Problem346.symPowMap line 27

   Source documentation

   Symmetric powers act covariantly on linear maps.

   def symPowMap (n : ℕ) (f : V →ₗ[ℂ] W) : SymPow n V →ₗ[ℂ] SymPow n W :=
   …

   Mentions: OAI.Problem346.SymPow

5. theorem OAI.Problem346.symPowMap_symMonomial line 40
6. theorem OAI.Problem346.symAlgMap_id line 45
7. theorem OAI.Problem346.symAlgMap_comp line 50
8. theorem OAI.Problem346.symPowMap_coe line 55
9. theorem OAI.Problem346.symPowMap_id line 58
10. theorem OAI.Problem346.symPowMap_comp line 65
11. def OAI.Problem346.symPowEquiv line 73

    Source documentation

    A linear equivalence induces an equivalence on each symmetric power.

    def symPowEquiv (n : ℕ) (e : V ≃ₗ[ℂ] W) : SymPow n V ≃ₗ[ℂ] SymPow n W where
    …

    Mentions: OAI.Problem346.SymPow

12. theorem OAI.Problem346.symPowEquiv_symMonomial line 85
13. theorem OAI.Problem346.symPowEquiv_toLinearMap line 89
14. theorem OAI.Problem346.symPowEquiv_refl line 92
15. theorem OAI.Problem346.symPowEquiv_trans line 97
16. theorem OAI.Problem346.symPowEquiv_symm line 102
17. theorem OAI.Problem346.symPowMap_injective line 106
18. theorem OAI.Problem346.symPowMap_surjective line 115