Recovering tensors from their supported coordinate subspaces

If a tensor has support inside three injectively embedded coordinate sets, it is exactly the extension by zero of its pullback to those sets. Characters therefore have the same value on the ambient tensor and this smaller tensor.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensor_eq_extendByZero_pullback {K : Type} [Field K] {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype 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) (hs : ∀ (x' : X') (y' : Y') (z' : Z'), T x' y' z' ≠ 0 → x' ∈ Set.range fx ∧ y' ∈ Set.range fy ∧ z' ∈ Set.range fz) : T = 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) (Foundation.Tensor.pullback fx fy fz T)

Support in embedded coordinate sets reconstructs the tensor by zero extension.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_eq_pullback_of_support {K : Type} [Field K] {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (χ : Character K) (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) (hs : ∀ (x' : X') (y' : Y') (z' : Z'), T x' y' z' ≠ 0 → x' ∈ Set.range fx ∧ y' ∈ Set.range fy ∧ z' ∈ Set.range fz) : χ.value T = χ.value (Foundation.Tensor.pullback fx fy fz T)

A character ignores ambient coordinates outside a tensor's support.