The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.
Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.
abbreviation OAI.CubeShuffle.Specht.Cell line 9
abbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}
definition OAI.CubeShuffle.Specht.row line 10
def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1
definition OAI.CubeShuffle.Specht.col line 11
def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2
definition OAI.CubeShuffle.Specht.rowIndex line 15
noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) := ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩
abbreviation OAI.CubeShuffle.Specht.Tabloid line 18
abbrev Tabloid (μ : YoungDiagram) := {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}
definition OAI.CubeShuffle.Specht.baseTabloid line 23
noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩
definition OAI.CubeShuffle.Specht.tabloidAct line 25
noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) : Equiv.Perm (Tabloid μ) where
Show the remaining 12 lines
toFun f := ⟨fun x => f.1 (p⁻¹ x), by obtain ⟨q,hq⟩ := f.2 refine ⟨q*p⁻¹, ?_⟩ funext x simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩ invFun f := ⟨fun x => f.1 (p x), by obtain ⟨q,hq⟩ := f.2 refine ⟨q*p, ?_⟩ funext x simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩ left_inv f := by apply Subtype.ext; funext x; simp right_inv f := by apply Subtype.ext; funext x; simp
definition OAI.CubeShuffle.Specht.tabloidRep line 57
noncomputable def tabloidRep (μ : YoungDiagram) : Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where
Show the remaining 9 lines
toFun p := { toFun := fun v f => v (tabloidAct p⁻¹ f) map_add' := by intros; rfl map_smul' := by intros; rfl } map_one' := by ext v f; simp map_mul' p q := by ext v f simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply] rfl
definition OAI.CubeShuffle.Specht.delta line 72
noncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ := fun g => if g=f then 1 else 0
definition OAI.CubeShuffle.Specht.colGroup line 75
noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where carrier := {p | ∀ x, col (p x) = col x} one_mem' := by intro x; rfl mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x) inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symm
definition OAI.CubeShuffle.Specht.permSign line 81
noncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ := ((Equiv.Perm.sign p : ℤ) : ℂ)
definition OAI.CubeShuffle.Specht.alternator line 86
noncomputable def alternator (C : Subgroup (Equiv.Perm α)) (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by classical exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ c
definition OAI.CubeShuffle.Specht.polytabloid line 93
noncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ := alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))
definition OAI.CubeShuffle.Specht.space line 96
noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) := Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))
definition OAI.CubeShuffle.Specht.subrepresentation line 114
noncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) := ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩
definition OAI.CubeShuffle.Specht.representation line 117
noncomputable def representation (μ : YoungDiagram) : Representation ℂ (Equiv.Perm (Cell μ)) (space μ) := (subrepresentation μ).toRepresentation
abbreviation OAI.CubeShuffle.PermutationHilbert.H line 130
abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ X
definition OAI.CubeShuffle.Specht.hilbertEquiv line 138
noncomputable def hilbertEquiv (μ : YoungDiagram) : (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) := (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symm
definition OAI.CubeShuffle.Specht.hilbertSpace line 142
noncomputable def hilbertSpace (μ : YoungDiagram) : Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMap
definition OAI.CubeShuffle.Specht.spaceHilbertEquiv line 145
noncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ := (hilbertEquiv μ).submoduleMap (space μ)
definition OAI.CubeShuffle.Specht.unitaryRepresentation line 148
noncomputable def unitaryRepresentation (μ : YoungDiagram) : Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) := ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)
definition OAI.CubeShuffle.Specht.relabelledUnitary line 154
noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) : Representation ℂ (Equiv.Perm α) (hilbertSpace μ) := (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHom
definition OAI.CubeShuffle.UnitaryFinite.IsUnitary line 169
def IsUnitary (ρ : Representation ℂ G V) : Prop := ∀ g v w, inner ℂ (ρ g v) (ρ g w) = inner ℂ v w
definition OAI.RowColumn.lineGroup line 182
def lineGroup {α β : Type*} (f : α → β) : Subgroup (Equiv.Perm α) where carrier := {g | ∀ x, f (g x) = f x} one_mem' := by intro x; rfl mul_mem' := by intro a b ha hb x exact (ha (b x)).trans (hb x) inv_mem' := by intro a ha x simpa using (ha (a⁻¹ x)).symm
7 more definitions are reached the same way; the full file lists them.
Comparator compares only the name and type of each definition listed here. When a theorem is configured, its proof uses the definition in OpenAI’s solution library. Read that definition as well as the one in this file when comparing the statement with the paper.