Universal root complexes

Orthogonal root kernels and the universal BGG complex used in the all-rank argument.

inductive MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot (r n : ℕ) : Type

Data encoding the orthogonal positive root construction.

• difference {r n : ℕ} (p q : Fin (r + 1)) : p < q → OrthogonalPositiveRoot r n
• sum {r n : ℕ} (p q : Fin (r + 1)) : p < q → OrthogonalPositiveRoot r n
• short {r n : ℕ} (p : Fin (r + 1)) (t : Fin n) : 2 * (r + 1) ≤ ↑t → OrthogonalPositiveRoot r n

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation {r n : ℕ} (h : 2 * (r + 1) ≤ n) : OrthogonalPositiveRoot r n → Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The orthogonal positive root derivation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) = ↑p

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) = 2 * (r + 1) - ↑p

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight_unused {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ (HigherHarmonicYoung.variableIndex a t) = r + 1

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight_le {r n : ℕ} (v : Fin ((r + 1) * n)) : MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ v ≤ 2 * (r + 1)

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation {σ : Type u_1} (e : MvPolynomial σ ℂ ≃ₐ[ℂ] MvPolynomial σ ℂ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)

The conjugated polynomial derivation used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation e D = MvPolynomial.mkDerivation ℂ fun (i : σ) => e.symm (D (e (MvPolynomial.X i)))

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation_X {σ : Type u_1} (e : MvPolynomial σ ℂ ≃ₐ[ℂ] MvPolynomial σ ℂ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (i : σ) : (conjugatedPolynomialDerivation e D) (MvPolynomial.X i) = e.symm (D (e (MvPolynomial.X i)))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation_intertwine {σ : Type u_1} (e : MvPolynomial σ ℂ ≃ₐ[ℂ] MvPolynomial σ ℂ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (p : MvPolynomial σ ℂ) : e ((conjugatedPolynomialDerivation e D) p) = D (e p)

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The isotropic orthogonal positive root derivation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation_intertwine {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) ((isotropicOrthogonalPositiveRootDerivation h α) p) = (orthogonalPositiveRootDerivation h α) ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.weighted_coefficient_smul_X_lt {σ : Type u_1} (weight : σ → ℕ) (u v : σ) (c : ℂ) (huv : weight u < weight v) (d : σ →₀ ℕ) (hd : MvPolynomial.coeff d (c • MvPolynomial.X u) ≠ 0) : (Finsupp.weight weight) d + 1 ≤ weight v

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootWord_intertwine {r n : ℕ} (h : 2 * (r + 1) ≤ n) (word : List (OrthogonalPositiveRoot r n)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) ((HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(isotropicOrthogonalPositiveRootDerivation h α)) word) p) = (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(orthogonalPositiveRootDerivation h α)) word) ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedDifferenceRoot_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.difference p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))) = if q = j then 2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedDifferenceRoot_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.difference p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j))) = if p = j then -2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedSumRoot_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.sum p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedSumRoot_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.sum p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j))) = (if q = j then 2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) else 0) - if p = j then 2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedDifferenceRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.difference p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedSumRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.sum p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedShortRoot_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (a j : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.short p t ht)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedShortRoot_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (a j : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.short p t ht)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j))) = if p = j then -2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedShortRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t u : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (hu : 2 * (r + 1) ≤ ↑u) (a : Fin (r + 1)) : (isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.short p t ht)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a u)) = if t = u then MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (a j : Fin (r + 1)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : MvPolynomial.coeff d ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j)))) ≠ 0) : (Finsupp.weight MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝) d + 1 ≤ MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (a j : Fin (r + 1)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : MvPolynomial.coeff d ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j)))) ≠ 0) : (Finsupp.weight MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝) d + 1 ≤ MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : MvPolynomial.coeff d ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t))) ≠ 0) : (Finsupp.weight MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝) d + 1 ≤ MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ (HigherHarmonicYoung.variableIndex a t)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (v : Fin ((r + 1) * n)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : MvPolynomial.coeff d ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X v)) ≠ 0) : (Finsupp.weight MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝) d + 1 ≤ MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight✝ v

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootWord_eq_zero_of_isHomogeneous {r n m : ℕ} (h : 2 * (r + 1) ≤ n) {p : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hp : p.IsHomogeneous m) (word : List (OrthogonalPositiveRoot r n)) (hlen : m * (2 * (r + 1)) < word.length) : (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(isotropicOrthogonalPositiveRootDerivation h α)) word) p = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootWord_eq_zero_of_isHomogeneous {r n m : ℕ} (h : 2 * (r + 1) ≤ n) {p : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hp : p.IsHomogeneous m) (word : List (OrthogonalPositiveRoot r n)) (hlen : m * (2 * (r + 1)) < word.length) : (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(orthogonalPositiveRootDerivation h α)) word) p = 0

theorem MetricCodes.Spherical.HigherYoungIsotropicAdjoinRange.adjoin_isotropicVariable_eq_nullSubstitution_range {r n : ℕ} (h : 2 * (r + 1) ≤ n) : Algebra.adjoin ℂ (Set.range fun (ap : Fin (r + 1) × Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h ap.1 ap.2) = (HigherHarmonicYoung.nullSubstitution h).range

theorem MetricCodes.Spherical.HigherYoungIsotropicAdjoinRange.exists_nullSubstitution_of_mem_adjoin_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ Algebra.adjoin ℂ (Set.range fun (ap : Fin (r + 1) × Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h ap.1 ap.2)) : ∃ (q : MvPolynomial (Fin (r + 1) × Fin (r + 1)) ℂ), (HigherHarmonicYoung.nullSubstitution h) q = f

theorem MetricCodes.Spherical.HigherYoungEvenCoordinateHolomorphicAdjoin.isotropicCoordinateEquiv_mem_adjoin_of_even_vars {r n : ℕ} (h : 2 * (r + 1) ≤ n) (g : MvPolynomial (Fin ((r + 1) * n)) ℂ) (heven : ∀ v ∈ g.vars, ∃ (a : Fin (r + 1)) (p : Fin (r + 1)), v = HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) : (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) g ∈ Algebra.adjoin ℂ (Set.range fun (ap : Fin (r + 1) × Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h ap.1 ap.2)

@[simp]

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) = 0

@[simp]

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) = 2

@[simp]

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect_unused {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ (HigherHarmonicYoung.variableIndex a t) = 1

@[simp]

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_X {ι : Type u_1} (w : ι → ℕ) (i : ι) : (MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ w) (MvPolynomial.X i) = ↑(w i) • MvPolynomial.X i

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.coeff_X_mul_pderiv {ι : Type u_1} (p : MvPolynomial ι ℂ) (i : ι) (d : ι →₀ ℕ) : MvPolynomial.coeff d (MvPolynomial.X i * (MvPolynomial.pderiv i) p) = ↑(d i) * MvPolynomial.coeff d p

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_eq_sum {ι : Type u_1} [Fintype ι] (w : ι → ℕ) : MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ w = ∑ i : ι, ↑(w i) • MvPolynomial.X i • MvPolynomial.pderiv i

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_apply {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (p : MvPolynomial ι ℂ) : (MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ w) p = ∑ i : ι, ↑(w i) • (MvPolynomial.X i * (MvPolynomial.pderiv i) p)

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_coeff {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (p : MvPolynomial ι ℂ) (d : ι →₀ ℕ) : MvPolynomial.coeff d ((MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ w) p) = ↑(∑ i : ι, w i * d i) * MvPolynomial.coeff d p

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.conjugatedTotalAmbientCartan_X {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) : (HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h)) (MvPolynomial.X v) = 2 • MvPolynomial.X v - ↑(2 * MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ v) • MvPolynomial.X v

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.conjugatedTotalAmbientCartan_eq_euler_sub_defect {r n : ℕ} (h : 2 * (r + 1) ≤ n) : HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) = (2 • MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ fun (x : Fin ((r + 1) * n)) => 1) - MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ fun (i : Fin ((r + 1) * n)) => 2 * MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ i

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_one_of_homogeneous {ι : Type u_1} [Finite ι] {d : ℕ} (p : MvPolynomial ι ℂ) (hp : p.IsHomogeneous d) : (MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ fun (x : ι) => 1) p = ↑d • p

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.exists_evenCoordinate_of_defect_eq_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) (hv : MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ v = 0) : ∃ (a : Fin (r + 1)) (p : Fin (r + 1)), v = HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefectDerivation_eq_zero_of_maximalCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ) (hfhom : f.IsHomogeneous d) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * d) • f) : (MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation✝ fun (i : Fin ((r + 1) * n)) => 2 * MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ i) ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f) = 0

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect_eq_zero_of_mem_vars_of_maximalCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ) (hfhom : f.IsHomogeneous d) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * d) • f) (v : Fin ((r + 1) * n)) (hv : v ∈ ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f).vars) : MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect✝ v = 0

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.maximalTotalAmbientCartan_mem_nullSubstitution_range {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ) (hfhom : f.IsHomogeneous d) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * d) • f) : ∃ (q : MvPolynomial (Fin (r + 1) × Fin (r + 1)) ℂ), (HigherHarmonicYoung.nullSubstitution h) q = f

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The young complex pair used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.polynomialRealPart_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : HigherHarmonicYoung.polynomialRealPart (youngComplexPair lam p q) = ↑p

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.polynomialImaginaryPart_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : HigherHarmonicYoung.polynomialImaginaryPart (youngComplexPair lam p q) = ↑q

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexPolynomial_eq_of_real_imaginary {r n : ℕ} (p q : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hreal : HigherHarmonicYoung.polynomialRealPart p = HigherHarmonicYoung.polynomialRealPart q) (himag : HigherHarmonicYoung.polynomialImaginaryPart p = HigherHarmonicYoung.polynomialImaginaryPart q) : p = q

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_eq_zero_iff {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : youngComplexPair lam p q = 0 ↔ p = 0 ∧ q = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexAmbientRotation_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (youngComplexPair lam p q) = youngComplexPair lam ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b) p) ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b) q)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complex_smul_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (c : ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : c • youngComplexPair lam p q = youngComplexPair lam (c.re • p - c.im • q) (c.im • p + c.re • q)

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_add {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q p' q' : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : youngComplexPair lam (p + p') (q + q') = youngComplexPair lam p q + youngComplexPair lam p' q'

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexRotationCombination_youngComplexPair {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin k → Fin n) (c : Fin k → ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : ∑ i : Fin k, c i • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (a i) (b i)) (youngComplexPair lam p q) = youngComplexPair lam (∑ i : Fin k, ((c i).re • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) p - (c i).im • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) q)) (∑ i : Fin k, ((c i).im • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) p + (c i).re • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) q))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rowDerivation_self_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (i : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation i i) (youngComplexPair lam p q) = ↑(lam i) • youngComplexPair lam p q

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rowDerivation_upper_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (i j : Fin (r + 1)) (hij : i < j) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) (youngComplexPair lam p q) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_dominantHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : youngComplexPair lam (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn lam hdom) (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn lam hdom) = (HigherHarmonicYoung.DeterminantVectors.dominantHighestWeightWitness hn lam hdom).polynomial

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_endomorphism_dominantHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : youngComplexPair lam (A (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn lam hdom)) (A (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn lam hdom)) = HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_isHomogeneous {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : (youngComplexPair lam p q).IsHomogeneous (∑ i : Fin (r + 1), lam i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngEndomorphismHighestPolynomial_isHomogeneous {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : (HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A).IsHomogeneous (∑ i : Fin (r + 1), lam i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_complexCombination_eigen {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (a b : Fin k → Fin n) (c : Fin k → ℂ) (z : ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (heigen : ∑ i : Fin k, c i • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (a i) (b i)) (youngComplexPair lam p q) = z • youngComplexPair lam p q) : ∑ i : Fin k, c i • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (a i) (b i)) (youngComplexPair lam (A p) (A q)) = z • youngComplexPair lam (A p) (A q)

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexAmbientRotation_self {r n : ℕ} (a : Fin n) : HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a a = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.ambientCartan_eq_twice_I_complexRotation {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (i : Fin (r + 1)) : HigherHarmonicYoung.DeterminantVectors.ambientCartan hn i = (2 * Complex.I) • HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn i) (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_complexRotation_eigen {r n : ℕ} (lam : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (a b : Fin n) (c z : ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (heigen : c • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (youngComplexPair lam p q) = z • youngComplexPair lam p q) : c • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (youngComplexPair lam (A p) (A q)) = z • youngComplexPair lam (A p) (A q)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_ambientCartan_dominantHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (i : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn i) (HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A) = ↑(2 * lam i) • HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_totalAmbientCartan_dominantHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) (HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A) = ↑(2 * ∑ i : Fin (r + 1), lam i) • HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_dominantHighest_mem_ambientIsotropic_of_maximalCartan_range {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (hrange : ∀ (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ), f.IsHomogeneous d → (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) f = ↑(2 * d) • f → ∃ (q : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (HigherHarmonicYoung.nullSubstitution hn) q = f) : HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_dominantHighest_mem_ambientIsotropic {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) : HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.arbitraryRowRaisingGramScalar_eq_tensorGramScalar {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : ArbitraryRowRaisingSchurTraceGram.arbitraryRowRaisingGramScalar high row = ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar high row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.youngClebschRaise_arbitrary_inner_of_highestLine_and_cyclic {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (ha : 0 < high row) (hn : 2 * (r + 1) ≤ n) (hdomhigh : Antitone high) (hdomlow : Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hhighest : HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) hdomlow (LinearMap.adjoint (youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) ∘ₗ youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) ∈ IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) hdomlow = ⊤) (p q : ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row))) : inner ℝ ((youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) p) ((youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) q) = ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar high row * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.arbitraryRowRaiseTensorGram_pos {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hn : 2 * (r + 1) ≤ n) (ha : 0 < high row) (hdomhigh : Antitone high) (hdomlow : Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hstrict : ∀ (j : Fin (r + 1)), ↑j = ↑row + 1 → high j < high row) : 0 < ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar high row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.youngClebschRaise_arbitrary_inner_of_cyclic {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (ha : 0 < high row) (hn : 2 * (r + 1) ≤ n) (hdomhigh : Antitone high) (hdomlow : Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) hdomlow = ⊤) (p q : ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row))) : inner ℝ ((youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) p) ((youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) q) = ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar high row * inner ℝ p q

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot (r : ℕ) : Type

The positive root used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot r = { z : Fin (r + 1) × Fin (r + 1) // z.1 < z.2 }

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator {r : ℕ} (n : ℕ) (α : PositiveRoot r) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The positive root operator used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator n α = MetricCodes.Spherical.HigherHarmonicYoung.polarization r n (↑α).2 (↑α).1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator_apply {r n : ℕ} (α : PositiveRoot r) (p : PolynomialSpace r n) : (positiveRootOperator n α) p = (polarization r n (↑α).2 (↑α).1) p

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign {α : Type u_1} [LinearOrder α] (s : Finset α) (a : α) : ℤ

The exterior root sign used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign s a = (-1) ^ {x ∈ s | x < a}.card

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRoot_predecessorCard_erase_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (ha : a ∈ s) (hab : a < b) : {x ∈ s | x < b}.card = {x ∈ s.erase a | x < b}.card + 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRoot_predecessors_erase_not_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (hab : ¬a < b) : {x ∈ s.erase a | x < b} = {x ∈ s | x < b}

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign_erase_of_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (ha : a ∈ s) (hab : a < b) : exteriorRootSign s b = -exteriorRootSign (s.erase a) b

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign_erase_of_not_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (hab : ¬a < b) : exteriorRootSign (s.erase a) b = exteriorRootSign s b

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign_erase_anticommute {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b) : exteriorRootSign s a * exteriorRootSign (s.erase a) b = -(exteriorRootSign s b * exteriorRootSign (s.erase b) a)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootWedge (r k : ℕ) : Type

The root wedge used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootWedge r k = { S : Finset (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot r) // S.card = k }

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFirst {r : ℕ} (α : PositiveRoot r) : Fin (r + 1)

The positive root first used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFirst α = (↑α).1

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootSecond {r : ℕ} (α : PositiveRoot r) : Fin (r + 1)

The positive root second used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootSecond α = (↑α).2

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFirst_lt_second {r : ℕ} (α : PositiveRoot r) : positiveRootFirst α < positiveRootSecond α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFirst_ne_second {r : ℕ} (α : PositiveRoot r) : positiveRootFirst α ≠ positiveRootSecond α

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge {r : ℕ} (α : PositiveRoot r) (i : Fin (r + 1)) : ℤ

The root charge used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge_first {r : ℕ} (α : PositiveRoot r) : rootCharge α (positiveRootFirst α) = 1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge_second {r : ℕ} (α : PositiveRoot r) : rootCharge α (positiveRootSecond α) = -1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge_eq_zero_of_ne {r : ℕ} (α : PositiveRoot r) (i : Fin (r + 1)) (hfirst : i ≠ positiveRootFirst α) (hsecond : i ≠ positiveRootSecond α) : rootCharge α i = 0

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge {r : ℕ} (S : Finset (PositiveRoot r)) (i : Fin (r + 1)) : ℤ

The root family charge used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge S i = ∑ α ∈ S, MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge α i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_empty {r : ℕ} (i : Fin (r + 1)) : rootFamilyCharge ∅ i = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_singleton {r : ℕ} (α : PositiveRoot r) (i : Fin (r + 1)) : rootFamilyCharge {α} i = rootCharge α i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_insert {r : ℕ} (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∉ S) (i : Fin (r + 1)) : rootFamilyCharge (insert α S) i = rootCharge α i + rootFamilyCharge S i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_erase {r : ℕ} (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∈ S) (i : Fin (r + 1)) : rootFamilyCharge (S.erase α) i = rootFamilyCharge S i - rootCharge α i

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) (i : Fin (r + 1)) : ℤ

The signed root weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight lam S i = ↑(lam i) + MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge S i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_insert {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∉ S) (i : Fin (r + 1)) : signedRootWeight lam (insert α S) i = signedRootWeight lam S i + rootCharge α i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_erase {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∈ S) (i : Fin (r + 1)) : signedRootWeight lam (S.erase α) i = signedRootWeight lam S i - rootCharge α i

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.AdmissibleRootWedge {r : ℕ} (lam : Fin (r + 1) → ℕ) (k : ℕ) : Type

The admissible root wedge used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (i : Fin (r + 1)) : ℕ

The root wedge weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight lam S i = (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight lam (↑↑S) i).toNat

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight_cast {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (i : Fin (r + 1)) : ↑(rootWedgeWeight lam S i) = signedRootWeight lam (↑↑S) i

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootJointHarmonicChain {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : Type

The root joint harmonic chain used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootPolynomialChain (r n k : ℕ) : Type

The root polynomial chain used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootVector (r : ℕ) : Type

The root vector used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootVector r = (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot r →₀ ℝ)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant {r : ℕ} (α β γ : PositiveRoot r) : ℝ

The root structure constant used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracket {r : ℕ} (α β : PositiveRoot r) : RootVector r

The root bracket used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracket_apply {r : ℕ} (α β γ : PositiveRoot r) : (rootBracket α β) γ = rootStructureConstant α β γ

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_single {r n : ℕ} (α : PositiveRoot r) (c : ℝ) : ((MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) fun₀ | α => c) = c • positiveRootOperator n α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator_commutator {r n : ℕ} (α β : PositiveRoot r) : positiveRootOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootOperator n α = ∑ γ : PositiveRoot r, rootStructureConstant α β γ • positiveRootOperator n γ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_rootBracket {r n : ℕ} (α β : PositiveRoot r) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) (rootBracket α β) = positiveRootOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootOperator n α

@[instance_reducible]

instance MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootLinearOrder (r : ℕ) : LinearOrder (PositiveRoot r)

Equations

• One or more equations did not get rendered due to their size.

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeInsert {r k : ℕ} (T : RootWedge r k) (α : PositiveRoot r) (hα : α ∉ ↑T) : RootWedge r (k + 1)

The root wedge insert used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeInsert T α hα = ⟨insert α ↑T, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeInsert_val {r k : ℕ} (T : RootWedge r k) (α : PositiveRoot r) (hα : α ∉ ↑T) : ↑(rootWedgeInsert T α hα) = insert α ↑T

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign {α : Type u_1} [LinearOrder α] (S : Finset α) (a : α) : ℝ

The real exterior root sign used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign S a = ↑(MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign S a)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBoundary (r n k : ℕ) : RootPolynomialChain r n (k + 1) →ₗ[ℝ] RootPolynomialChain r n k

The root action boundary used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBoundary_apply (r n k : ℕ) (f : RootPolynomialChain r n (k + 1)) (T : RootWedge r k) : (rootActionBoundary r n k) f T = ∑ α : PositiveRoot r, if hα : α ∈ ↑T then 0 else realExteriorRootSign (insert α ↑T) α • (positiveRootOperator n α) (f (rootWedgeInsert T α hα))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign_erase_anticommute {α : Type u_1} [LinearOrder α] (S : Finset α) {a b : α} (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) : realExteriorRootSign S a * realExteriorRootSign (S.erase a) b = -(realExteriorRootSign S b * realExteriorRootSign (S.erase b) a)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (i : Fin (r + 1)) : ℕ

The lower root weight used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_first {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) : lowerRootWeight μ α (positiveRootFirst α) = μ (positiveRootFirst α) - 1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_second {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) : lowerRootWeight μ α (positiveRootSecond α) = μ (positiveRootSecond α) + 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_other {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (i : Fin (r + 1)) (hfirst : i ≠ positiveRootFirst α) (hsecond : i ≠ positiveRootSecond α) : lowerRootWeight μ α i = μ i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferSource_eq {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) : μ = Function.update (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferBase✝ μ α) (positiveRootFirst α) (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferBase✝ μ α (positiveRootFirst α) + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferTarget_eq {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) : lowerRootWeight μ α = Function.update (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferBase✝ μ α) (positiveRootSecond α) (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferBase✝ μ α (positiveRootSecond α) + 1)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperator {r : ℕ} (n : ℕ) (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) : JointHarmonicWeightSpace n μ →ₗ[ℝ] JointHarmonicWeightSpace n (lowerRootWeight μ α)

The weighted positive root operator used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperatorStar {r : ℕ} (n : ℕ) (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) : JointHarmonicWeightSpace n (lowerRootWeight μ α) →ₗ[ℝ] JointHarmonicWeightSpace n μ

The weighted positive root operator star used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperator_coe {r n : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (p : JointHarmonicWeightSpace n μ) : ↑↑((weightedPositiveRootOperator n μ α hμ) p) = (positiveRootOperator n α) ↑↑p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperatorStar_coe {r n : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (q : JointHarmonicWeightSpace n (lowerRootWeight μ α)) : ↑↑((weightedPositiveRootOperatorStar n μ α hμ) q) = (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_cast {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (i : Fin (r + 1)) : ↑(lowerRootWeight μ α i) = ↑(μ i) - rootCharge α i

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) : AdmissibleRootWedge lam (k + 1)

The root admissible insert used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_val {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) : ↑↑(rootAdmissibleInsert lam T α hα hadm) = insert α ↑↑T

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_weight_charge {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (i : Fin (r + 1)) : ↑(rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm) i) = ↑(rootWedgeWeight lam T i) + rootCharge α i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_first_pos {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) : 0 < rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm) (positiveRootFirst α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_lowerRootWeight {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) : lowerRootWeight (rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm)) α = rootWedgeWeight lam T

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.jointHarmonicWeightCast {r : ℕ} (n : ℕ) (μ ν : Fin (r + 1) → ℕ) (h : μ = ν) : JointHarmonicWeightSpace n μ ≃ₗ[ℝ] JointHarmonicWeightSpace n ν

The joint harmonic weight cast used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.jointHarmonicWeightCast n μ ν h = h ▸ LinearEquiv.refl ℝ (MetricCodes.Spherical.HigherHarmonicYoung.JointHarmonicWeightSpace n μ)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.jointHarmonicWeightCast_coe {r n : ℕ} (μ ν : Fin (r + 1) → ℕ) (h : μ = ν) (p : JointHarmonicWeightSpace n μ) : ↑↑((jointHarmonicWeightCast n μ ν h) p) = ↑↑p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdge {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm)) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam T)

The weighted exterior root edge used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k

The weighted exterior action differential used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (T : AdmissibleRootWedge lam k) : (weightedExteriorActionDifferential n lam k) f T = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑T then 0 else if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i then realExteriorRootSign (insert α ↑↑T) α • (weightedExteriorRootEdge n lam T α hα hadm) (f (rootAdmissibleInsert lam T α hα hadm)) else 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_youngGramPrefixWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) : p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam k ↔ ↑p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_zero (r n : ℕ) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n 0 = ⊥

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam 0 = ⊥

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight_variableIndex {r n : ℕ} (i : Fin (r + 1)) (k : Fin n) : MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n (variableIndex i k) = Pi.single i 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight_weight {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) : (Finsupp.weight (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n)) d = fun (i : Fin (r + 1)) => Finsupp.degree (rowExponent d i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousSubmodule_eq_weightedHomogeneousSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) : youngMultihomogeneousSubmodule n lam = MvPolynomial.weightedHomogeneousSubmodule ℝ (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngWeightedComponent_mem_youngMultihomogeneousSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : (MvPolynomial.weightedHomogeneousComponent (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) lam) p ∈ youngMultihomogeneousSubmodule n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial_isWeightedHomogeneous {r n : ℕ} (i j : Fin (r + 1)) : MvPolynomial.IsWeightedHomogeneous (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) (rowPairingPolynomial i j) (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial_isHomogeneousElem {r n : ℕ} (i j : Fin (r + 1)) : SetLike.IsHomogeneousElem (MvPolynomial.weightedHomogeneousSubmodule ℝ (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n)) (rowPairingPolynomial i j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_isHomogeneous (r n k : ℕ) : Ideal.IsHomogeneous (MvPolynomial.weightedHomogeneousSubmodule ℝ (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n)) (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_weightedHomogeneousComponent_mem {r n k : ℕ} {p : PolynomialSpace r n} (hp : p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k) (lam : Fin (r + 1) → ℕ) : (MvPolynomial.weightedHomogeneousComponent (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) lam) p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_add_finrank {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : ℕ) : Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam k) + Module.finrank ℝ ↥(MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam k) = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngWeightedComponent_gram_mul {r n : ℕ} (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : (MvPolynomial.weightedHomogeneousComponent (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j + mu)) (rowPairingPolynomial i j * p) = rowPairingPolynomial i j * (MvPolynomial.weightedHomogeneousComponent (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) mu) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_succ {r n k : ℕ} (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n (k + 1) = MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k ⊔ Ideal.span {(ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k]}

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_le_succ {r n k : ℕ} (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k ≤ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule_le_succ {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam k ≤ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixQuotientNext_surjective {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) : Function.Surjective ⇑(MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixQuotientNext✝ n lam k hk)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotientMultiplication_injective {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) (hreg : ∀ (p : PolynomialSpace r n), rowPairingPolynomial i j * p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k → p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k) : Function.Injective ⇑(MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotientMultiplication✝ n i j mu k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotient_exact {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) : (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotientMultiplication✝ n i j mu k).range = (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixQuotientNext✝ n (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j + mu) k hk).ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_succ_of_fits {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) (hreg : ∀ (p : PolynomialSpace r n), rowPairingPolynomial i j * p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k → p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n k) : Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j + mu) (k + 1)) + Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n mu k) = Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j + mu) k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngWeightedComponent_gram_mul_eq_zero_of_overweight {r n : ℕ} (i j : Fin (r + 1)) (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hover : lam a < MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j a) (p : PolynomialSpace r n) : (MvPolynomial.weightedHomogeneousComponent (MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight✝ r n) lam) (rowPairingPolynomial i j * p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule_succ_eq_of_overweight {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) (hover : lam a < MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j a) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam (k + 1) = MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam k

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_succ_of_overweight {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) (hover : lam a < MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ i j a) : Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (k + 1)) = Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam k)

def MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree {r : ℕ} (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) (i : Fin (r + 1)) : ℕ

The gram pair row degree used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree z i = (if (↑z).1 = i then 1 else 0) + if (↑z).2 = i then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree_eq_youngGramPairDegree {r : ℕ} (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) : gramPairRowDegree z = MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ (↑z).1 (↑z).2

def MetricCodes.Spherical.HigherHarmonicYoung.gramFamilyRowDegree {r : ℕ} (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (i : Fin (r + 1)) : ℕ

The gram family row degree used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.gramFamilyRowDegree s i = ∑ z ∈ s, MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree z i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramFamilyRowDegree_insert {r : ℕ} (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) (hz : z ∉ s) (i : Fin (r + 1)) : gramFamilyRowDegree (insert z s) i = gramPairRowDegree z i + gramFamilyRowDegree s i

def MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient {r : ℕ} (n : ℕ) (lam delta : Fin (r + 1) → ℕ) : ℕ

The shifted young ambient coefficient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient n lam delta = ∏ i : Fin (r + 1), if delta i ≤ lam i then (n + (lam i - delta i) - 1).choose (lam i - delta i) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient_eq_zero_of_not_le {r n : ℕ} (lam delta : Fin (r + 1) → ℕ) (i : Fin (r + 1)) (hi : lam i < delta i) : shiftedYoungAmbientCoefficient n lam delta = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient_add {r n : ℕ} (lam delta epsilon : Fin (r + 1) → ℕ) (hdelta : ∀ (i : Fin (r + 1)), delta i ≤ lam i) : (shiftedYoungAmbientCoefficient n lam fun (i : Fin (r + 1)) => delta i + epsilon i) = shiftedYoungAmbientCoefficient n (fun (i : Fin (r + 1)) => lam i - delta i) epsilon

def MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) : ℤ

The gram koszul coefficient used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient_empty {r n : ℕ} (lam : Fin (r + 1) → ℕ) : gramKoszulCoefficient n lam ∅ = ↑(∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i))

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient_insert {r n : ℕ} (lam : Fin (r + 1) → ℕ) (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) (hz : z ∉ s) : gramKoszulCoefficient n lam (insert z s) = gramKoszulCoefficient n lam s - if ∀ (i : Fin (r + 1)), gramPairRowDegree z i ≤ lam i then gramKoszulCoefficient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree z i) s else 0

def MetricCodes.Spherical.HigherHarmonicYoung.fullGramKoszulCoefficient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℤ

The full gram koszul coefficient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.fullGramKoszulCoefficient n lam = MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient n lam Finset.univ

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset_zero (r : ℕ) : MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r 0 = ∅

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset_length (r n : ℕ) : MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = Finset.univ

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset_succ {r : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) : MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r (↑k + 1) = insert (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) (MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r ↑k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt_not_mem_gramPrefixPairFinset {r : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) : MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k ∉ MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r ↑k

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient_prefix_succ {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) : gramKoszulCoefficient n lam (MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r (↑k + 1)) = gramKoszulCoefficient n lam (MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r ↑k) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i ≤ lam i then gramKoszulCoefficient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i) (MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r ↑k) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam 0) = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_eq_gramKoszulCoefficient_of_recurrence {r n : ℕ} (hstep : ∀ (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))), ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (↑k + 1))) = ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i ≤ lam i then ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i) ↑k)) else 0) (k : ℕ) (hk : k ≤ Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (lam : Fin (r + 1) → ℕ) : ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam k)) = gramKoszulCoefficient n lam (MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset✝ r k)

def MetricCodes.Spherical.HigherHarmonicYoung.weylShift {r : ℕ} (lam : Fin (r + 1) → ℕ) (σ : Equiv.Perm (Fin (r + 1))) (i : Fin (r + 1)) : ℤ

The weyl shift used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.weylShift lam σ i = ↑(lam i) - ↑↑i + ↑↑(σ i)

def MetricCodes.Spherical.HigherHarmonicYoung.signedFullGramKoszulCoefficient {r : ℕ} (n : ℕ) (mu : Fin (r + 1) → ℤ) : ℤ

The signed full gram koszul coefficient used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

def MetricCodes.Spherical.HigherHarmonicYoung.alternatingGramKoszulCoefficient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℤ

The alternating gram koszul coefficient used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_length (r n : ℕ) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule_length {r n : ℕ} (lam : Fin (r + 1) → ℕ) : MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule✝ n lam (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = youngGramRadialWeightSubmodule n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_length_eq_upperGramPair_card (r n : ℕ) : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_getElem_gramPairAt {r n : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).get ⟨↑k, ⋯⟩ = ArbitraryRankMixedTraceRegularity.gramPairPolynomial n (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt_mul_mem_prefix_of_weaklyRegular {r n : ℕ} (hregular : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) (p : PolynomialSpace r n) (hp : ArbitraryRankMixedTraceRegularity.gramPairPolynomial n (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) * p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n ↑k) : p ∈ MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal✝ r n ↑k

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightQuotient_signed_recurrence_of_fits_and_overweight {r n : ℕ} (hfits : ∀ (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) (mu : Fin (r + 1) → ℕ), Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ (↑(MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)).1 (↑(MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)).2 + mu) (↑k + 1)) + Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n mu ↑k) = Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ (↑(MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)).1 (↑(MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)).2 + mu) ↑k)) (hoverweight : ∀ (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)), lam i < MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree✝ (↑(MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)).1 (↑(MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k)).2 i → Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (↑k + 1)) = Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam ↑k)) (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) : ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (↑k + 1))) = ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i ≤ lam i then ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i) ↑k)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightQuotient_signed_recurrence_of_weaklyRegular {r n : ℕ} (hregular : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)) (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) : ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (↑k + 1))) = ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i ≤ lam i then ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i) ↑k)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramRadialWeightQuotient_eq_fullGramKoszulCoefficient_of_recurrence {r n : ℕ} (hstep : ∀ (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))), ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (↑k + 1))) = ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i ≤ lam i then ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i) ↑k)) else 0) (lam : Fin (r + 1) → ℕ) : ↑(Module.finrank ℝ (YoungGramRadialWeightQuotient n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_fullGramKoszulCoefficient_of_recurrence {r n : ℕ} (hstep : ∀ (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))), ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam (↑k + 1))) = ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i ≤ lam i then ↑(Module.finrank ℝ (MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient✝ n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt✝ k) i) ↑k)) else 0) (lam : Fin (r + 1) → ℕ) : ↑(Module.finrank ℝ (JointHarmonicWeightSpace n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_fullGramKoszulCoefficient {r n : ℕ} (hregular : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)) (lam : Fin (r + 1) → ℕ) : ↑(Module.finrank ℝ (JointHarmonicWeightSpace n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_fullGramKoszulCoefficient_of_stable {r n : ℕ} (hn : 2 * r < n) (lam : Fin (r + 1) → ℕ) : ↑(Module.finrank ℝ (JointHarmonicWeightSpace n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.bgg_range_eq_ker_of_hodgeLaplacian_injective {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ G] (d : F →ₗ[ℝ] E) (e : G →ₗ[ℝ] F) (hchain : d ∘ₗ e = 0) (hinj : Function.Injective ⇑(LinearMap.adjoint d ∘ₗ d + e ∘ₗ LinearMap.adjoint e)) : e.range = d.ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.bgg_range_eq_ker_of_fischerCore_hodgeLaplacian_injective {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ G] (cE : InnerProductSpace.Core ℝ E) (cF : InnerProductSpace.Core ℝ F) (cG : InnerProductSpace.Core ℝ G) (d : F →ₗ[ℝ] E) (dStar : E →ₗ[ℝ] F) (e : G →ₗ[ℝ] F) (eStar : F →ₗ[ℝ] G) (hdStar : ∀ (x : E) (y : F), inner ℝ (dStar x) y = inner ℝ x (d y)) (heStar : ∀ (x : F) (y : G), inner ℝ (eStar x) y = inner ℝ x (e y)) (hchain : d ∘ₗ e = 0) (hinj : Function.Injective ⇑(dStar ∘ₗ d + e ∘ₗ eStar)) : e.range = d.ker

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.signedJointHarmonicWeightDimension {r : ℕ} (n : ℕ) (mu : Fin (r + 1) → ℤ) : ℤ

The signed joint harmonic weight dimension used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.alternatingJointHarmonicWeightDimension {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℤ

The alternating joint harmonic weight dimension used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.alternatingJointHarmonicWeightDimension_eq_alternatingGramKoszul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hgram : ∀ (mu : Fin (r + 1) → ℕ), ↑(Module.finrank ℝ (JointHarmonicWeightSpace n mu)) = fullGramKoszulCoefficient n mu) : alternatingJointHarmonicWeightDimension n lam = alternatingGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.alternatingJointHarmonicWeightDimension_eq_alternatingGramKoszul_of_stable {r n : ℕ} (hn : 2 * r < n) (lam : Fin (r + 1) → ℕ) : alternatingJointHarmonicWeightDimension n lam = alternatingGramKoszulCoefficient n lam

def MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (W : ι → Type u_3) [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℝ (W i)] (A : (i : ι) → V →ₗ[ℝ] W i) (Astar : (i : ι) → W i →ₗ[ℝ] V) : V →ₗ[ℝ] V

The finite fischer root laplacian used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian W A Astar = ∑ i : ι, Astar i ∘ₗ A i

theorem MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian_energy {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (cV : InnerProductSpace.Core ℝ V) (W : ι → Type u_3) [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℝ (W i)] (cW : (i : ι) → InnerProductSpace.Core ℝ (W i)) (A : (i : ι) → V →ₗ[ℝ] W i) (Astar : (i : ι) → W i →ₗ[ℝ] V) (hadjoint : ∀ (i : ι) (x : W i) (y : V), inner ℝ ((Astar i) x) y = inner ℝ x ((A i) y)) (x : V) : inner ℝ x ((finiteFischerRootLaplacian W A Astar) x) = ∑ i : ι, inner ℝ ((A i) x) ((A i) x)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian_eq_zero_iff {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (cV : InnerProductSpace.Core ℝ V) (W : ι → Type u_3) [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℝ (W i)] (cW : (i : ι) → InnerProductSpace.Core ℝ (W i)) (A : (i : ι) → V →ₗ[ℝ] W i) (Astar : (i : ι) → W i →ₗ[ℝ] V) (hadjoint : ∀ (i : ι) (x : W i) (y : V), inner ℝ ((Astar i) x) y = inner ℝ x ((A i) y)) (x : V) : (finiteFischerRootLaplacian W A Astar) x = 0 ↔ ∀ (i : ι), (A i) x = 0

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.ActivePositiveRoot {r : ℕ} (lam : Fin (r + 1) → ℕ) : Type

The active positive root used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeRootBaseWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : Fin (r + 1) → ℕ

The active root base weight used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeRootBaseWeight_update_second {r : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : Function.update (activeRootBaseWeight lam α) (positiveRootSecond ↑α) (activeRootBaseWeight lam α (positiveRootSecond ↑α) + 1) = lam

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeRootRaisedWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : Fin (r + 1) → ℕ

The active root raised weight used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activePositiveRootRaise {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : JointHarmonicWeightSpace n lam →ₗ[ℝ] JointHarmonicWeightSpace n (activeRootRaisedWeight lam α)

The active positive root raise used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activePositiveRootLower {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : JointHarmonicWeightSpace n (activeRootRaisedWeight lam α) →ₗ[ℝ] JointHarmonicWeightSpace n lam

The active positive root lower used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activePositiveRootRaise_coe {r n : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) (p : JointHarmonicWeightSpace n lam) : ↑↑((activePositiveRootRaise n lam α) p) = (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ↑↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activePositiveRoot_fischer_adjoint {r n : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) (p : JointHarmonicWeightSpace n (activeRootRaisedWeight lam α)) (q : JointHarmonicWeightSpace n lam) : inner ℝ ((activePositiveRootLower n lam α) p) q = inner ℝ p ((activePositiveRootRaise n lam α) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian_eq_zero_iff {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : JointHarmonicWeightSpace n lam) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian✝ n lam) p = 0 ↔ ∀ (α : ActivePositiveRoot lam), (activePositiveRootRaise n lam α) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian_eq_zero_iff_harmonicYoung {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : JointHarmonicWeightSpace n lam) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian✝ n lam) p = 0 ↔ ↑↑p ∈ harmonicYoungSubmodule lam

@[implicit_reducible]

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicChainFischerCore {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : InnerProductSpace.Core ℝ (RootJointHarmonicChain n lam k)

The root joint harmonic chain fischer core component.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicChainFischerCore_inner {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (p q : RootJointHarmonicChain n lam k) : inner ℝ p q = ∑ S : AdmissibleRootWedge lam k, inner ℝ (p S) (q S)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.emptyAdmissibleRootWedge {r : ℕ} (lam : Fin (r + 1) → ℕ) : AdmissibleRootWedge lam 0

The empty admissible root wedge used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.admissibleRootWedge_zero_eq_empty {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam 0) : S = emptyAdmissibleRootWedge lam

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.admissibleRootWedgeZeroUnique {r : ℕ} (lam : Fin (r + 1) → ℕ) : Unique (AdmissibleRootWedge lam 0)

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight_degree_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam 0) : rootWedgeWeight lam S = lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicDegreeZeroEquiv {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : RootJointHarmonicChain n lam 0 ≃ₗ[ℝ] JointHarmonicWeightSpace n lam

The root joint harmonic degree zero equiv used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : RootJointHarmonicChain n lam 0 →ₗ[ℝ] (α : ActivePositiveRoot lam) → JointHarmonicWeightSpace n (activeRootRaisedWeight lam α)

The root degree zero positive cochain used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) (α : ActivePositiveRoot lam) : (rootDegreeZeroPositiveCochain n lam) p α = (activePositiveRootRaise n lam α) ((rootJointHarmonicDegreeZeroEquiv n lam) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain_eq_zero_iff_harmonicYoung {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) : (rootDegreeZeroPositiveCochain n lam) p = 0 ↔ ↑↑((rootJointHarmonicDegreeZeroEquiv n lam) p) ∈ harmonicYoungSubmodule lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroFischerLaplacian_eq_zero_iff_harmonicYoung {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroFischerLaplacian✝ n lam) p = 0 ↔ ↑↑((rootJointHarmonicDegreeZeroEquiv n lam) p) ∈ harmonicYoungSubmodule lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain_eq_zero_iff_hodge {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) : (rootDegreeZeroPositiveCochain n lam) p = 0 ↔ (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroFischerLaplacian✝ n lam) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.finrank_rootDegreeZeroPositiveCochain_kernel {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ ↥(rootDegreeZeroPositiveCochain n lam).ker = Module.finrank ℝ ↥(HarmonicYoungSpace lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finiteChain_eulerCharacteristic_eq_degreeZero_sub_boundary_add_top (V : ℕ → Type u_1) [(k : ℕ) → AddCommGroup (V k)] [(k : ℕ) → Module ℝ (V k)] [∀ (k : ℕ), FiniteDimensional ℝ (V k)] (d : (k : ℕ) → V (k + 1) →ₗ[ℝ] V k) (N : ℕ) (hexact : ∀ k < N, (d (k + 1)).range = (d k).ker) : ∑ k ∈ Finset.range (N + 1), (-1) ^ k * ↑(Module.finrank ℝ (V k)) = ↑(Module.finrank ℝ (V 0)) - ↑(Module.finrank ℝ ↥(d 0).range) + (-1) ^ N * ↑(Module.finrank ℝ ↥(d N).range)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_reversed_vandermonde {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) : (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j)) = ∏ i : Fin (r + 1), ∏ j > i, (x i - x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_quadratic_projective_vandermonde {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) : (Matrix.projVandermonde (fun (i : Fin (r + 1)) => 1 + x i ^ 2) x).det = (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j)) * ∏ i : Fin (r + 1), ∏ j > i, (1 - x i * x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.upper_gram_pair_product {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) : (∏ i : Fin (r + 1), (1 - x i ^ 2)) * ∏ i : Fin (r + 1), ∏ j > i, (1 - x i * x j) = ∏ i : Fin (r + 1), ∏ j ≥ i, (1 - x i * x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.orthogonal_denominator_entry {R : Type u_1} [CommRing R] (x : R) (r j : ℕ) (hj : j ≤ r) : x ^ (r - j) - x ^ (r + j + 2) = (1 - x ^ 2) * x ^ (r - j) * ∑ k ∈ Finset.range (j + 1), x ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_isMonicOfDegree (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) : (Polynomial.Chebyshev.S R ↑j).IsMonicOfDegree j

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_monic (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) : (Polynomial.Chebyshev.S R ↑j).Monic

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_natDegree (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) : (Polynomial.Chebyshev.S R ↑j).natDegree = j

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.homogenize_shift {R : Type u_1} [CommSemiring R] (p : Polynomial R) (n k : ℕ) (hp : p.natDegree ≤ n) : p.homogenize (n + k) = p.homogenize n * MvPolynomial.X 1 ^ k

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_homogenize_add_two (R : Type u_1) [CommRing R] [Nontrivial R] (n : ℕ) : (Polynomial.Chebyshev.S R ↑(n + 2)).homogenize (n + 2) = MvPolynomial.X 0 * (Polynomial.Chebyshev.S R ↑(n + 1)).homogenize (n + 1) - MvPolynomial.X 1 ^ 2 * (Polynomial.Chebyshev.S R ↑n).homogenize n

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.even_geometric_sum_add_two {R : Type u_1} [CommRing R] (x : R) (n : ℕ) : ∑ k ∈ Finset.range (n + 3), x ^ (2 * k) = (1 + x ^ 2) * ∑ k ∈ Finset.range (n + 2), x ^ (2 * k) - x ^ 2 * ∑ k ∈ Finset.range (n + 1), x ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_homogenize_eval_one_add_sq (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) (x : R) : (MvPolynomial.eval ![1 + x ^ 2, x]) ((Polynomial.Chebyshev.S R ↑j).homogenize j) = ∑ k ∈ Finset.range (j + 1), x ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_homogenized_monic_evaluation {R : Type u_1} [CommRing R] {r : ℕ} (p : Fin (r + 1) → Polynomial R) (hdegree : ∀ (j : Fin (r + 1)), (p j).natDegree = ↑j) (hmonic : ∀ (j : Fin (r + 1)), (p j).Monic) (v w : Fin (r + 1) → R) : (Matrix.det fun (i j : Fin (r + 1)) => ∑ k ∈ Finset.range (↑j + 1), (p j).coeff k * v i ^ k * w i ^ (r - k)) = (Matrix.projVandermonde v w).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.homogenize_eval_eq_sum_coeff {R : Type u_1} [CommSemiring R] (p : Polynomial R) (j : ℕ) (v w : R) : (MvPolynomial.eval ![v, w]) (p.homogenize j) = ∑ k ∈ Finset.range (j + 1), p.coeff k * v ^ k * w ^ (j - k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_orthogonal_denominator_row_factor {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) : (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) - x i ^ (r + ↑j + 2)) = (∏ i : Fin (r + 1), (1 - x i ^ 2)) * Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) * ∑ k ∈ Finset.range (↑j + 1), x i ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_chebyshev_geometric_sum {R : Type u_1} [CommRing R] [Nontrivial R] {r : ℕ} (x : Fin (r + 1) → R) : (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) * ∑ k ∈ Finset.range (↑j + 1), x i ^ (2 * k)) = (Matrix.projVandermonde (fun (i : Fin (r + 1)) => 1 + x i ^ 2) x).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_orthogonal_denominator {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) : (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) - x i ^ (r + ↑j + 2)) = (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j)) * ∏ i : Fin (r + 1), ∏ j ≥ i, (1 - x i * x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRoot_prod_eq {R : Type u_1} [CommMonoid R] {r : ℕ} (f : Fin (r + 1) → Fin (r + 1) → R) : ∏ α : PositiveRoot r, f (positiveRootFirst α) (positiveRootSecond α) = ∏ i : Fin (r + 1), ∏ j > i, f i j

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRoot_vandermonde {r : ℕ} : ∏ α : PositiveRoot r, (MvPolynomial.X (positiveRootSecond α) - MvPolynomial.X (positiveRootFirst α)) = ∑ σ : Equiv.Perm (Fin (r + 1)), ↑(Equiv.Perm.sign σ) • ∏ i : Fin (r + 1), MvPolynomial.X i ^ ↑(σ i)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.shiftedPolynomialWeightFunctional_monomial {r : ℕ} (lam : Fin (r + 1) → ℕ) (F : (Fin (r + 1) → ℤ) → ℤ) (m : Fin (r + 1) →₀ ℕ) (c : ℤ) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.shiftedPolynomialWeightFunctional✝ lam F) ((MvPolynomial.monomial m) c) = (F fun (i : Fin (r + 1)) => ↑(lam i) + ↑(m i) - ↑↑i) * c

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSelectedExponent_apply {r : ℕ} (S : Finset (PositiveRoot r)) (i : Fin (r + 1)) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSelectedExponent✝ S) i = (∑ α ∈ Finset.univ \ S, if positiveRootSecond α = i then 1 else 0) + ∑ α ∈ S, if positiveRootFirst α = i then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootSecond_card {r : ℕ} (i : Fin (r + 1)) : {α : PositiveRoot r | positiveRootSecond α = i}.card = ↑i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSelectedExponent_sub_baseline {r : ℕ} (S : Finset (PositiveRoot r)) (i : Fin (r + 1)) : ↑((MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSelectedExponent✝ S) i) - ↑↑i = rootFamilyCharge S i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamily_selectedMonomial {r : ℕ} (S : Finset (PositiveRoot r)) : (∏ α ∈ Finset.univ \ S, MvPolynomial.X (positiveRootSecond α)) * ∏ α ∈ S, MvPolynomial.X (positiveRootFirst α) = (MvPolynomial.monomial (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSelectedExponent✝ S)) 1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPermutationExponent_apply {r : ℕ} (σ : Equiv.Perm (Fin (r + 1))) (i : Fin (r + 1)) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPermutationExponent✝ σ) i = ↑(σ i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPermutationMonomial {r : ℕ} (σ : Equiv.Perm (Fin (r + 1))) : ∏ i : Fin (r + 1), MvPolynomial.X i ^ ↑(σ i) = (MvPolynomial.monomial (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPermutationExponent✝ σ)) 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootFamily_vandermonde_expansion {r : ℕ} : ∏ α : PositiveRoot r, (MvPolynomial.X (positiveRootSecond α) - MvPolynomial.X (positiveRootFirst α)) = ∑ S : Finset (PositiveRoot r), (MvPolynomial.monomial (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSelectedExponent✝ S)) ((-1) ^ S.card)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_alternating_eq_weylShift {r : ℕ} (lam : Fin (r + 1) → ℕ) (F : (Fin (r + 1) → ℤ) → ℤ) : ∑ S : Finset (PositiveRoot r), (-1) ^ S.card * F (signedRootWeight lam S) = ∑ σ : Equiv.Perm (Fin (r + 1)), ↑(Equiv.Perm.sign σ) * F (weylShift lam σ)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.finrank_rootJointHarmonicChain {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ (RootJointHarmonicChain n lam k) = ∑ S : AdmissibleRootWedge lam k, Module.finrank ℝ (JointHarmonicWeightSpace n (rootWedgeWeight lam S))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedJointHarmonicWeightDimension_signedRootWeight {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : signedJointHarmonicWeightDimension n (signedRootWeight lam ↑↑S) = ↑(Module.finrank ℝ (JointHarmonicWeightSpace n (rootWedgeWeight lam S)))

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootExteriorEulerCharacteristic {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℤ

The root exterior euler characteristic used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyEulerCharacteristic {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℤ

The root family euler characteristic used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyEulerCharacteristic_eq_alternatingJointHarmonicWeightDimension {r n : ℕ} (lam : Fin (r + 1) → ℕ) : rootFamilyEulerCharacteristic n lam = alternatingJointHarmonicWeightDimension n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_swap {r : ℕ} (α β γ : PositiveRoot r) : rootStructureConstant β α γ = -rootStructureConstant α β γ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_apply_X {r n : ℕ} (x : RootVector r) (j : Fin (r + 1)) (k : Fin n) : ((MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) x) (MvPolynomial.X (variableIndex j k)) = ∑ α ∈ x.support, x α • if (↑α).1 = j then MvPolynomial.X (variableIndex (↑α).2 k) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_X_coefficient {r n : ℕ} (x : RootVector r) (α : PositiveRoot r) (k : Fin n) : MvPolynomial.coeff (fun₀ | variableIndex (↑α).2 k => 1) (((MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) x) (MvPolynomial.X (variableIndex (↑α).1 k))) = x α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_injective {r n : ℕ} (hn : 0 < n) : Function.Injective ⇑(MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket {r : ℕ} (x y : RootVector r) : RootVector r

The root vector bracket used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_zero_left {r : ℕ} (y : RootVector r) : rootVectorBracket 0 y = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_zero_right {r : ℕ} (x : RootVector r) : rootVectorBracket x 0 = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_single_single {r : ℕ} (α β : PositiveRoot r) (a b : ℝ) : (rootVectorBracket (fun₀ | α => a) fun₀ | β => b) = (a * b) • rootBracket α β

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_add_left {r : ℕ} (x y z : RootVector r) : rootVectorBracket (x + y) z = rootVectorBracket x z + rootVectorBracket y z

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_add_right {r : ℕ} (x y z : RootVector r) : rootVectorBracket x (y + z) = rootVectorBracket x y + rootVectorBracket x z

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_rootVectorBracket {r n : ℕ} (x y : RootVector r) : (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) (rootVectorBracket x y) = (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) x ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) y - (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) y ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction✝ n) x

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_jacobi {r : ℕ} (x y z : RootVector r) : rootVectorBracket x (rootVectorBracket y z) + rootVectorBracket y (rootVectorBracket z x) + rootVectorBracket z (rootVectorBracket x y) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundaryCoefficient {r k : ℕ} (S : RootWedge r (k + 1)) (T : RootWedge r k) : ℝ

The root bracket boundary coefficient used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeSingleton {r : ℕ} (α : PositiveRoot r) : RootWedge r 1

The root wedge singleton used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeSingleton α = ⟨{α}, ⋯⟩

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundary (r n k : ℕ) : RootPolynomialChain r n (k + 1) →ₗ[ℝ] RootPolynomialChain r n k

The root bracket boundary used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundary_apply {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (T : RootWedge r k) : (rootBracketBoundary r n k) f T = ∑ S : RootWedge r (k + 1), rootBracketBoundaryCoefficient S T • f S

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundaryCoefficient_degree_zero {r : ℕ} (S : RootWedge r 1) (T : RootWedge r 0) : rootBracketBoundaryCoefficient S T = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootChevalleyEilenbergBoundary (r n k : ℕ) : RootPolynomialChain r n (k + 1) →ₗ[ℝ] RootPolynomialChain r n k

The root chevalley eilenberg boundary used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_cases_disjoint {r : ℕ} (α β γ : PositiveRoot r) (hfirst : (↑α).1 = (↑β).2 ∧ ↑γ = ((↑β).1, (↑α).2)) (hsecond : (↑β).1 = (↑α).2 ∧ ↑γ = ((↑α).1, (↑β).2)) : False

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_ne_zero_iff {r : ℕ} (α β γ : PositiveRoot r) : rootStructureConstant α β γ ≠ 0 ↔ (↑α).1 = (↑β).2 ∧ ↑γ = ((↑β).1, (↑α).2) ∨ (↑β).1 = (↑α).2 ∧ ↑γ = ((↑α).1, (↑β).2)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge_eq_add_of_structureConstant_ne_zero {r : ℕ} (α β γ : PositiveRoot r) (h : rootStructureConstant α β γ ≠ 0) (i : Fin (r + 1)) : rootCharge γ i = rootCharge α i + rootCharge β i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exists_rootBracketWitness_of_coefficient_ne_zero {r k : ℕ} (S : RootWedge r (k + 1)) (T : RootWedge r k) (h : rootBracketBoundaryCoefficient S T ≠ 0) : ∃ (α : PositiveRoot r) (β : PositiveRoot r) (γ : PositiveRoot r), α ∈ ↑S ∧ β ∈ (↑S).erase α ∧ α < β ∧ γ ∉ ((↑S).erase α).erase β ∧ ↑T = insert γ (((↑S).erase α).erase β) ∧ rootStructureConstant α β γ ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_eq_of_bracketWitness {r : ℕ} (lam : Fin (r + 1) → ℕ) (S T : Finset (PositiveRoot r)) (α β γ : PositiveRoot r) (hα : α ∈ S) (hβ : β ∈ S.erase α) (hγ : γ ∉ (S.erase α).erase β) (hT : T = insert γ ((S.erase α).erase β)) (hconstant : rootStructureConstant α β γ ≠ 0) (i : Fin (r + 1)) : signedRootWeight lam S i = signedRootWeight lam T i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_eq_of_bracketBoundaryCoefficient_ne_zero {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : RootWedge r (k + 1)) (T : RootWedge r k) (h : rootBracketBoundaryCoefficient S T ≠ 0) (i : Fin (r + 1)) : signedRootWeight lam (↑S) i = signedRootWeight lam (↑T) i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight_eq_of_bracketBoundaryCoefficient_ne_zero {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (T : AdmissibleRootWedge lam k) (h : rootBracketBoundaryCoefficient ↑S ↑T ≠ 0) : rootWedgeWeight lam S = rootWedgeWeight lam T

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketEdge {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (T : AdmissibleRootWedge lam k) (h : rootBracketBoundaryCoefficient ↑S ↑T ≠ 0) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam T)

The weighted root bracket edge used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketEdge_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (T : AdmissibleRootWedge lam k) (h : rootBracketBoundaryCoefficient ↑S ↑T ≠ 0) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : ↑↑((weightedRootBracketEdge n lam S T h) p) = ↑↑p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketBoundary {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k

The weighted root bracket boundary used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketBoundary_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (T : AdmissibleRootWedge lam k) : (weightedRootBracketBoundary n lam k) f T = ∑ S : AdmissibleRootWedge lam (k + 1), if h : rootBracketBoundaryCoefficient ↑S ↑T = 0 then 0 else rootBracketBoundaryCoefficient ↑S ↑T • (weightedRootBracketEdge n lam S T h) (f S)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k

The weighted chevalley eilenberg differential used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

instance MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicChain_finiteDimensional {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : FiniteDimensional ℝ (RootJointHarmonicChain n lam k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.admissibleRootWedge_above_card_isEmpty {r k : ℕ} (lam : Fin (r + 1) → ℕ) (hk : Fintype.card (PositiveRoot r) < k) : IsEmpty (AdmissibleRootWedge lam k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.admissibleRootWedge_one_exists_active {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam 1) : ∃ (α : PositiveRoot r), ↑↑S = {α} ∧ 0 < lam (positiveRootSecond α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicChainDifferential_top_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (d : (k : ℕ) → RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k) : d (Fintype.card (PositiveRoot r)) = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketBoundary_degree_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) : weightedRootBracketBoundary n lam 0 = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential_degree_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) : weightedChevalleyEilenbergDifferential n lam 0 = weightedExteriorActionDifferential n lam 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.finrank_harmonicYoung_eq_rootExteriorEulerCharacteristic_of_rootExact {r n : ℕ} (lam : Fin (r + 1) → ℕ) (d : (k : ℕ) → RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k) (hexact : ∀ k < Fintype.card (PositiveRoot r), (d (k + 1)).range = (d k).ker) (hzero : Module.finrank ℝ ↥(rootDegreeZeroPositiveCochain n lam).ker + Module.finrank ℝ ↥(d 0).range = Module.finrank ℝ (RootJointHarmonicChain n lam 0)) : ↑(Module.finrank ℝ ↥(HarmonicYoungSpace lam)) = rootExteriorEulerCharacteristic n lam