Spanning.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.span_symMonomial line 11
Source documentation
Monomials span the symmetric power, in its subtype realization.
```
theorem span_symMonomial (n : ℕ) (V : Type u) [AddCommGroup V] [Module ℂ V] :
    Submodule.span ℂ (Set.range (symMonomial n V)) = ⊤ := by
…
```
Mentions: OAI.Problem346.symMonomial

theorem OAI.Problem346.symPow_linearMap_ext line 18

Source documentation

Maps out of a symmetric power are determined by monomials.

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

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

theorem OAI.Problem346.multilinear_eq_zero_of_span line 27

Source documentation

A multilinear map vanishing on tuples from a spanning set is zero.

theorem multilinear_eq_zero_of_span
    {M : Type u} [AddCommGroup M] [Module ℂ M]
    {N : Type v} [AddCommGroup N] [Module ℂ N]
    {s : Set M} (hs : Submodule.span ℂ s = ⊤) (n : ℕ) :
    ∀ F : MultilinearMap ℂ (fun _ : Fin n => M) N,
      (∀ x, (∀ i, x i ∈ s) → F x = 0) → F = 0 := by
…

theorem OAI.Problem346.multilinear_ext_of_span line 53

Source documentation

Multilinear maps agree if they agree on tuples from a spanning set.

theorem multilinear_ext_of_span
    {M : Type u} [AddCommGroup M] [Module ℂ M]
    {N : Type v} [AddCommGroup N] [Module ℂ N]
    {s : Set M} (hs : Submodule.span ℂ s = ⊤) (n : ℕ)
    (F G : MultilinearMap ℂ (fun _ : Fin n => M) N)
    (h : ∀ x, (∀ i, x i ∈ s) → F x = G x) : F = G := by
…

theorem OAI.Problem346.plethysm_linearMap_ext line 65

Source documentation

Linear maps out of a plethysm are determined by double monomials.

theorem plethysm_linearMap_ext (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V]
    {W : Type v} [AddCommGroup W] [Module ℂ W]
    (f g : SymPow b (SymPow a V) →ₗ[ℂ] W)
    (h : ∀ x : Fin b → Fin a → V,
      f (symMonomial b (SymPow a V) (fun j => symMonomial a V (x j))) =
      g (symMonomial b (SymPow a V) (fun j => symMonomial a V (x j)))) : f = g := by
…

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

theorem OAI.Problem346.span_plethysmMonomial line 86

Source documentation

Double monomials span the plethysm.

theorem span_plethysmMonomial (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V] :
    Submodule.span ℂ (Set.range (fun x : Fin b → Fin a → V =>
      symMonomial b (SymPow a V) (fun j => symMonomial a V (x j)))) = ⊤ := by
…

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

theorem OAI.Problem346.IsFoulkesMap.unique line 101

Source documentation

The defining formula determines a Foulkes map uniquely.

theorem IsFoulkesMap.unique (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V]
    {f g : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V)}
    (hf : IsFoulkesMap a b V f) (hg : IsFoulkesMap a b V g) : f = g := by
…

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