BandGlue.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.bandGlue line 15

Source comment

Apply a band intertwiner to every scalar high-coordinate of a colored strip orbit map. This is the concrete tensor product of the two maps.

def bandGlue {n a b k d : ℕ} {X : Type uX} [AddCommGroup X] [Module ℂ X]
    (e : Fin n ≃ Fin a ⊕ Fin b)
    (T : X →ₗ[ℂ] ((Fin b → Fin k) → WordSpace a d))
    (L : WordSpace b k →ₗ[ℂ] WordSpace b d) : X →ₗ[ℂ] WordSpace n d where
…

Mentions: OAI.Saxl.WordSpace

lemma OAI.Saxl.bandGlue_sum line 33
lemma OAI.Saxl.bandGlue_equivariant line 48
lemma OAI.Saxl.bandGlue_mem line 76

theorem OAI.Saxl.bandGlue_exists line 90

Source comment

A module containing every band Specht type of the relevant height detects any nonzero high-valued colored-band vector. No multiplicity hypothesis is needed.

theorem bandGlue_exists {n a b k d : ℕ} {X : Type uX} [AddCommGroup X] [Module ℂ X]
    (e : Fin n ≃ Fin a ⊕ Fin b) (ρ : Representation ℂ (Equiv.Perm (Fin n)) X)
    (v : WordSpace a d) (u : WordSpace b d)
    (hband : ∀ (μ : YoungDiagram) (t : Tableau b μ), μ.colLen 0 ≤ k →
      ∃ f : Representation.IntertwiningMap (spechtRep t) (cyclic (wordRep b d) u).toRepresentation, f ≠ 0)
    (T : X →ₗ[ℂ] ((Fin b → Fin k) → WordSpace a d)) (hT0 : T ≠ 0)
    (hT : ∀ h q x w, T (ρ (sumPerm e h q) x) w = wordRep a d h (T x (w ∘ q)))
    (hTm : ∀ x c, T x c ∈ cyclic (wordRep a d) v) :
    ∃ f : X →ₗ[ℂ] WordSpace n d, f ≠ 0 ∧
      (∀ h q x, f (ρ (sumPerm e h q) x) = wordRep n d (sumPerm e h q) (f x)) ∧
      (∀ x, f x ∈ cyclic (wordRep n d) (positionProduct e v u)) := by
…

Mentions: OAI.Saxl.WordSpace, OAI.Saxl.Tableau, OAI.Saxl.spechtRep, OAI.Saxl.cyclic, OAI.Saxl.wordRep, OAI.Saxl.sumPerm, OAI.Saxl.positionProduct

def OAI.Saxl.coordinateSub line 130
lemma OAI.Saxl.positionProduct_sector line 136
lemma OAI.Saxl.bandGlue_sector line 154
theorem OAI.Saxl.bandGlue_sector_exists line 170