Characters.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass line 30
Source documentation
A character has a well-defined value on mutual-restriction classes.
```
def valueOnTensorClass (χ : Character) : TensorClass → ℝ :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_tensorClass line 41
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_classOf line 45
Source documentation
Passing to a finite natural-coordinate presentation preserves the value.
```
@[simp] theorem valueOnTensorClass_classOf (χ : Character)
    {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) : χ.valueOnTensorClass (classOf T) = χ.value T :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_monotone line 51
Source documentation
Restriction monotonicity descends to the quotient order.
```
theorem valueOnTensorClass_monotone (χ : Character) : Monotone χ.valueOnTensorClass := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_zero line 61
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_one line 66
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_mul line 72
Source documentation
Multiplicativity is unchanged on passing to tensor classes.
```
theorem valueOnTensorClass_mul (χ : Character) (T S : TensorClass) :
    χ.valueOnTensorClass (T * S) = χ.valueOnTensorClass T * χ.valueOnTensorClass S := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.valueOnTensorClass_add line 83
Source documentation
Additivity is unchanged on passing to tensor classes.
```
theorem valueOnTensorClass_add (χ : Character) (T S : TensorClass) :
    χ.valueOnTensorClass (T + S) = χ.valueOnTensorClass T + χ.valueOnTensorClass S := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom line 94
Source documentation
A coefficient-level character descends to a normalized semiring homomorphism.
```
def toTensorClassHom (χ : Character) : TensorClass →+* ℝ where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom_monotone line 101
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom_classOf line 104
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom line 111
Source documentation
A monotone semiring homomorphism on tensor classes gives a character on all finite coefficient tensors. Normalization follows from preservation of 0 and 1.
```
def ofTensorClassHom (φ : TensorClass →+* ℝ) (hφ : Monotone φ) : Character where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom_value line 134
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.ext line 139
Source documentation
Equality of all coefficient-level values determines a character.
```
@[ext] theorem ext {χ ψ : Character}
    (h : ∀ {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z]
      (T : Tensor ℂ X Y Z), χ.value T = ψ.value T) : χ = ψ := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom_toTensorClassHom line 149
Source documentation
Descending and then lifting recovers the original coefficient-level character.
```
@[simp] theorem ofTensorClassHom_toTensorClassHom (χ : Character) :
    ofTensorClassHom χ.toTensorClassHom χ.toTensorClassHom_monotone = χ := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom_ofTensorClassHom line 156
Source documentation
Lifting and then descending recovers the original semiring homomorphism.
```
@[simp] theorem toTensorClassHom_ofTensorClassHom
    (φ : TensorClass →+* ℝ) (hφ : Monotone φ) :
    (ofTensorClassHom φ hφ).toTensorClassHom = φ := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character.ofTensorClassHom, OAI.MatrixMultiplication.AuxiliarySeparation.Character.toTensorClassHom
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.tensorClassHomEquiv line 166
Source documentation
Concrete characters are exactly monotone real-valued tensor semiring homomorphisms.
```
def tensorClassHomEquiv : Character ≃ {φ : TensorClass →+* ℝ // Monotone φ} where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character