OrdinaryAssociativityNaturality.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.RightTensor.mapFirst line 17
Source documentation
A map of the first right module retains the middle bimodule's right B-action.
```
def RightTensor.mapFirst (f : M →ₗ[Aᵐᵒᵖ] M') : RightTensor k A B M N →ₗ[Bᵐᵒᵖ] RightTensor k A B M' N where
…
```
Mentions: OAI.LittleFinitistic.RightTensor
def OAI.LittleFinitistic.LeftTensor.mapLast line 30
Source documentation
A map of the last left module retains the middle bimodule's left A-action.
```
def LeftTensor.mapLast (g : Z →ₗ[B] Z') : LeftTensor k B A N Z →ₗ[A] LeftTensor k B A N Z' where
…
```
Mentions: OAI.LittleFinitistic.LeftTensor
theorem OAI.LittleFinitistic.BalancedAssociativity.natural_first line 46
Source documentation
Actual associativity is natural in the complex's right-module term.
```
theorem natural_first (f : M →ₗ[Aᵐᵒᵖ] M') :
    (forward k A B M' N Z).comp
      (BalancedTensor.mapLeft (k := k) Z (RightTensor.mapFirst (k := k) (B := B) (N := N) f)) =
…
```
Mentions: OAI.LittleFinitistic.BalancedAssociativity.forward, OAI.LittleFinitistic.BalancedTensor.mapLeft, OAI.LittleFinitistic.RightTensor.mapFirst
theorem OAI.LittleFinitistic.BalancedAssociativity.natural_last line 64
Source documentation
Actual associativity is natural in the arbitrary input module.
```
theorem natural_last (g : Z →ₗ[B] Z') :
    (forward k A B M N Z').comp (BalancedTensor.mapRightTo (k := k) (M := RightTensor k A B M N) g) =
…
```
Mentions: OAI.LittleFinitistic.BalancedAssociativity.forward, OAI.LittleFinitistic.BalancedTensor.mapRightTo, OAI.LittleFinitistic.RightTensor