Character values on powers and varying-dimension direct sums

These are consequences of the normalized restriction-monotone character interface. Coordinate changes preserve values; permuting the three tensor legs need not preserve an individual character.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_extendByZero {K : Type} [Field K] (χ : Character K) {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] [DecidableEq X'] [DecidableEq Y'] [DecidableEq Z'] (T : Foundation.Tensor K X Y Z) (fx : X → X') (fy : Y → Y') (fz : Z → Z') (hx : Function.Injective fx) (hy : Function.Injective fy) (hz : Function.Injective fz) : χ.value (Foundation.Tensor.restrict (fun (x' : X') (x : X) => if fx x = x' then 1 else 0) (fun (y' : Y') (y : Y) => if fy y = y' then 1 else 0) (fun (z' : Z') (z : Z) => if fz z = z' then 1 else 0) T) = χ.value T

Extending finite coordinates by zero does not change a character value.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_power {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) (n : ℕ) : χ.value (T.power n) = χ.value T ^ n

Tensor powers turn a character value into an ordinary natural power.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_copies {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) (r : ℕ) : χ.value (Foundation.Tensor.directSum fun (x : Fin r) => T) = ↑r * χ.value T

Full independent copies contribute their exact multiplicity.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_power_copies {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) (r n : ℕ) : χ.value (Foundation.Tensor.directSum fun (x : Fin r) => T.power n) = ↑r * χ.value T ^ n

The character cost of an exact number of full copies of a tensor power.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch {K : Type} [Field K] {ι : Type} [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) (i : ι) : Foundation.Tensor K ((i : ι) × X i) ((i : ι) × Y i) ((i : ι) × Z i)

A branch extended to the common ambient sigma coordinate spaces.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_paddedBranch {K : Type} [Field K] (χ : Character K) {ι : Type} [Fintype ι] [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) (i : ι) : χ.value (paddedBranch T i) = χ.value (T i)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_matching {K : Type} [Field K] {ι : Type} [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) (i : ι) (x : X i) (y : Y i) (z : Z i) : paddedBranch T i ⟨i, x⟩ ⟨i, y⟩ ⟨i, z⟩ = T i x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_zero_left {K : Type} [Field K] {ι : Type} [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) (i : ι) (x : (i : ι) × X i) (y : (i : ι) × Y i) (z : (i : ι) × Z i) (hx : x.fst ≠ i) : paddedBranch T i x y z = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_zero_middle {K : Type} [Field K] {ι : Type} [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) (i : ι) (x : (i : ι) × X i) (y : (i : ι) × Y i) (z : (i : ι) × Z i) (hy : y.fst ≠ i) : paddedBranch T i x y z = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_zero_right {K : Type} [Field K] {ι : Type} [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) (i : ι) (x : (i : ι) × X i) (y : (i : ι) × Y i) (z : (i : ι) × Z i) (hz : z.fst ≠ i) : paddedBranch T i x y z = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.directSum_paddedBranch {K : Type} [Field K] {ι : Type} [Fintype ι] [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) : Foundation.Tensor.directSum (paddedBranch T) = Foundation.Tensor.restrict (fun (x' : ι × (i : ι) × X i) (x : (i : ι) × X i) => if (x.fst, x) = x' then 1 else 0) (fun (y' : ι × (i : ι) × Y i) (y : (i : ι) × Y i) => if (y.fst, y) = y' then 1 else 0) (fun (z' : ι × (i : ι) × Z i) (z : (i : ι) × Z i) => if (z.fst, z) = z' then 1 else 0) (Foundation.Tensor.dependentDirectSum T)

Redundant outer labels give a zero extension of the varying-dimension sum.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_dependentDirectSum {K : Type} [Field K] (χ : Character K) {ι : Type} [Fintype ι] [DecidableEq ι] {X Y Z : ι → Type} [(i : ι) → Fintype (X i)] [(i : ι) → Fintype (Y i)] [(i : ι) → Fintype (Z i)] (T : (i : ι) → Foundation.Tensor K (X i) (Y i) (Z i)) : χ.value (Foundation.Tensor.dependentDirectSum T) = ∑ i : ι, χ.value (T i)

Additivity holds even when each summand has different coordinate types.