Concrete tensor characters and the tensor semiring

The coefficient-level character interface and monotone real-valued semiring homomorphisms on mutual-restriction classes describe the same valuations. The map classOf uses finite natural-number coordinate presentations, so the construction applies to all finite coordinate types in the character interface.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass {K : Type} [Field K] (χ : Character K) : TensorSemiring.TensorClass K → ℝ

A character has a well-defined value on mutual-restriction classes.

Equations

• χ.valueOnTensorClass = Quotient.lift (fun (T : MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor K) => χ.value T.coeff) ⋯

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_tensorClass {K : Type} [Field K] (χ : Character K) (T : TensorSemiring.FiniteTensor K) : χ.valueOnTensorClass (TensorSemiring.tensorClass T) = χ.value T.coeff

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_classOf {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : χ.valueOnTensorClass (TensorSemiring.classOf T) = χ.value T

Passing to a finite natural-coordinate presentation preserves the value.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_monotone {K : Type} [Field K] (χ : Character K) : Monotone χ.valueOnTensorClass

Restriction monotonicity descends to the quotient order.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_zero {K : Type} [Field K] (χ : Character K) : χ.valueOnTensorClass 0 = 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_one {K : Type} [Field K] (χ : Character K) : χ.valueOnTensorClass 1 = 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_mul {K : Type} [Field K] (χ : Character K) (T S : TensorSemiring.TensorClass K) : χ.valueOnTensorClass (T * S) = χ.valueOnTensorClass T * χ.valueOnTensorClass S

Multiplicativity is unchanged on passing to tensor classes.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_add {K : Type} [Field K] (χ : Character K) (T S : TensorSemiring.TensorClass K) : χ.valueOnTensorClass (T + S) = χ.valueOnTensorClass T + χ.valueOnTensorClass S

Additivity is unchanged on passing to tensor classes.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom {K : Type} [Field K] (χ : Character K) : TensorSemiring.TensorClass K →+* ℝ

A coefficient-level character descends to a normalized semiring homomorphism.

Equations

• χ.toTensorClassHom = { toFun := χ.valueOnTensorClass, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom_monotone {K : Type} [Field K] (χ : Character K) : Monotone ⇑χ.toTensorClassHom

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom_classOf {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : χ.toTensorClassHom (TensorSemiring.classOf T) = χ.value T

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom {K : Type} [Field K] (φ : TensorSemiring.TensorClass K →+* ℝ) (hφ : Monotone ⇑φ) : Character K

A monotone semiring homomorphism on tensor classes gives a character on all finite coefficient tensors. Normalization follows from preservation of 0 and 1.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom_value {K : Type} [Field K] (φ : TensorSemiring.TensorClass K →+* ℝ) (hφ : Monotone ⇑φ) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : (ofTensorClassHom φ hφ).value T = φ (TensorSemiring.classOf T)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.ext {K : Type} [Field K] {χ ψ : Character K} (h : ∀ {X Y Z : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype Z] (T : Foundation.Tensor K X Y Z), χ.value T = ψ.value T) : χ = ψ

Equality of all coefficient-level values determines a character.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.ext_iff {K : Type} [Field K] {χ ψ : Character K} : χ = ψ ↔ ∀ {X Y Z : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype Z] (T : Foundation.Tensor K X Y Z), χ.value T = ψ.value T

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom_toTensorClassHom {K : Type} [Field K] (χ : Character K) : ofTensorClassHom χ.toTensorClassHom ⋯ = χ

Descending and then lifting recovers the original coefficient-level character.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom_ofTensorClassHom {K : Type} [Field K] (φ : TensorSemiring.TensorClass K →+* ℝ) (hφ : Monotone ⇑φ) : (ofTensorClassHom φ hφ).toTensorClassHom = φ

Lifting and then descending recovers the original semiring homomorphism.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.tensorClassHomEquiv {K : Type} [Field K] : Character K ≃ { φ : TensorSemiring.TensorClass K →+* ℝ // Monotone ⇑φ }

Concrete characters are exactly monotone real-valued tensor semiring homomorphisms.

Equations

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