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.SignedSweeps.Partition line 11
abbrev Partition (n : ℕ) := {lam : YoungDiagram // lam.card = n}
abbreviation OAI.SignedSweeps.SymmetricGroup line 13
abbrev SymmetricGroup (n : ℕ) := Equiv.Perm (Fin n)
definition OAI.SignedSweeps.Partition.transpose line 17
def transpose {n : ℕ} (lam : Partition n) : Partition n := ⟨lam.1.transpose, by simpa [YoungDiagram.card, YoungDiagram.transpose] using lam.2⟩
definition OAI.SignedSweeps.Partition.tableau line 20
def tableau {n : ℕ} (lam : Partition n) : {c // c ∈ lam.1.cells} ≃ Fin n := Fintype.equivFinOfCardEq (by simpa using lam.2)
definition OAI.SignedSweeps.Partition.rowOf line 23
def rowOf {n : ℕ} (lam : Partition n) (x : Fin n) : ℕ := ((tableau lam).symm x).1.1
definition OAI.SignedSweeps.Partition.colOf line 26
def colOf {n : ℕ} (lam : Partition n) (x : Fin n) : ℕ := ((tableau lam).symm x).1.2
definition OAI.SignedSweeps.fiberSubgroup line 31
def fiberSubgroup {A C : Type*} (f : A → C) : Subgroup (Equiv.Perm A) where carrier := {g | ∀ x, f (g x) = f x} one_mem' := by intro x; rfl mul_mem' := by intro g h hg hh x exact (hg (h x)).trans (hh x) inv_mem' := by intro g hg x simpa using (hg (g⁻¹ x)).symm
definition OAI.SignedSweeps.rowSubgroup line 41
def rowSubgroup {n : ℕ} (lam : Partition n) : Subgroup (SymmetricGroup n) := fiberSubgroup lam.rowOf
definition OAI.SignedSweeps.colSubgroup line 44
def colSubgroup {n : ℕ} (lam : Partition n) : Subgroup (SymmetricGroup n) := fiberSubgroup lam.colOf
abbreviation OAI.SignedSweeps.RegularSpace line 47
abbrev RegularSpace (n : ℕ) := EuclideanSpace ℂ (SymmetricGroup n)
definition OAI.SignedSweeps.regularIsometry line 49
def regularIsometry {n : ℕ} (g : SymmetricGroup n) : RegularSpace n ≃ₗᵢ[ℂ] RegularSpace n := LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (Equiv.mulLeft g)@[simp]
definition OAI.SignedSweeps.regularRepresentation line 58
def regularRepresentation (n : ℕ) : Representation ℂ (SymmetricGroup n) (RegularSpace n) where toFun g := (regularIsometry g).toLinearEquiv.toLinearMap map_one' := by ext f h; simp map_mul' := by intro g h ext f k simp [mul_assoc]@[simp]
definition OAI.SignedSweeps.polytabloid line 71
def polytabloid {n : ℕ} (lam : Partition n) : RegularSpace n := by classical exact ∑ c : colSubgroup lam, ∑ a : rowSubgroup lam, (((Equiv.Perm.sign (c : SymmetricGroup n) : ℤˣ) : ℤ) : ℂ) • EuclideanSpace.single ((c : SymmetricGroup n) * (a : SymmetricGroup n)) 1
definition OAI.SignedSweeps.spechtSubrepresentation line 77
def spechtSubrepresentation {n : ℕ} (lam : Partition n) : Subrepresentation (regularRepresentation n) where
Show the remaining 14 lines
toSubmodule := Submodule.span ℂ (Set.range (fun g => regularRepresentation n g (polytabloid lam))) apply_mem_toSubmodule := by intro g f hf induction hf using Submodule.span_induction with | mem v hv => obtain ⟨h, rfl⟩ := hv apply Submodule.subset_span refine ⟨g * h, ?_⟩ simp [map_mul, Module.End.mul_apply] | zero => simp | add x y hx hy ihx ihy => simpa only [map_add] using Submodule.add_mem _ ihx ihy | smul a x hx ih => simpa only [map_smul] using Submodule.smul_mem _ a ih
definition OAI.SignedSweeps.Specht line 94
def Specht {n : ℕ} (lam : Partition n) : Type := (spechtSubrepresentation lam).toSubmodule
definition OAI.SignedSweeps.spechtRepresentation line 105
def spechtRepresentation {n : ℕ} (lam : Partition n) : Representation ℂ (SymmetricGroup n) (Specht lam) := (spechtSubrepresentation lam).toRepresentation
definition OAI.SignedSweeps.spechtDimension line 109
def spechtDimension {n : ℕ} (lam : Partition n) : ℕ := finrank ℂ (Specht lam)
definition OAI.SignedSweeps.blockEmbedding line 111
def blockEmbedding {u v l n : ℕ} (h : u + v + l = n) (a : SymmetricGroup u) (b : SymmetricGroup v) (c : SymmetricGroup l) : SymmetricGroup n := let e : (Fin u ⊕ Fin v) ⊕ Fin l ≃ Fin n := ((Equiv.sumCongr finSumFinEquiv (Equiv.refl (Fin l))).trans finSumFinEquiv).trans (finCongr h) e.permCongr ((a.sumCongr b).sumCongr c)
definition OAI.SignedSweeps.SignedOccurrence line 119
def SignedOccurrence {u v l n : ℕ} (h : u + v + l = n) (α : Partition u) (β : Partition v) (γ : Partition l) (lam : Partition n) : Prop := ∃ f : ((Specht α ⊗[ℂ] Specht β.transpose) ⊗[ℂ] Specht γ) →ₗ[ℂ] Specht lam, Function.Injective f ∧ ∀ (a : SymmetricGroup u) (b : SymmetricGroup v) (c : SymmetricGroup l) x, f (TensorProduct.map (TensorProduct.map (spechtRepresentation α a) (spechtRepresentation β.transpose b)) (spechtRepresentation γ c) x) = spechtRepresentation lam (blockEmbedding h a b c) (f x)
abbreviation OAI.SignedSweeps.BinaryPositions line 129
abbrev BinaryPositions (d : ℕ) := Fin d → Fin 2
definition OAI.SignedSweeps.positionsEquiv line 131
def positionsEquiv (d : ℕ) : BinaryPositions d ≃ Fin (2 ^ d) := Fintype.equivFinOfCardEq (by simp [BinaryPositions])
definition OAI.SignedSweeps.coordinateSubgroup line 134
def coordinateSubgroup (d : ℕ) (i : Fin d) : Subgroup (SymmetricGroup (2 ^ d)) := fiberSubgroup (fun x : Fin (2 ^ d) => fun j : {j : Fin d // j ≠ i} => (positionsEquiv d).symm x j.1)
definition OAI.SignedSweeps.layerOperator line 138
def layerOperator {d : ℕ} (lam : Partition (2 ^ d)) (i : Fin d) : Specht lam →ₗ[ℂ] Specht lam := by classical exact (Fintype.card (coordinateSubgroup d i) : ℂ)⁻¹ • ∑ g : coordinateSubgroup d i, spechtRepresentation lam g.1
definition OAI.SignedSweeps.sweepOperator line 144
def sweepOperator {d : ℕ} (lam : Partition (2 ^ d)) : Specht lam →ₗ[ℂ] Specht lam := ((List.ofFn (layerOperator lam)).reverse).prod
7 more definitions are reached the same way; the full file lists them.