OrdinaryTensorExactness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BalancedTensor.mapRightTo line 16
Source documentation
The actual covariant map in the left-module factor of a balanced tensor.
```
def mapRightTo (f : N →ₗ[A] N') : Tensor k A M N →ₗ[k] Tensor k A M N' :=
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor
theorem OAI.LittleFinitistic.BalancedTensor.mapRightTo_mk line 22
def OAI.LittleFinitistic.IdempotentTensor.spaceMap line 35
theorem OAI.LittleFinitistic.IdempotentTensor.tensorEval_naturality line 42
theorem OAI.LittleFinitistic.IdempotentTensor.spaceMap_exact line 53
Source documentation
Taking an idempotent part preserves exactness, with an explicit projected preimage.
```
theorem spaceMap_exact (he : e*e=e) (f : N →ₗ[A] N') (g : N' →ₗ[A] N'')
    (h : Function.Exact f g) : Function.Exact (spaceMap (k := k) e f) (spaceMap (k := k) e g) := by
…
```
Mentions: OAI.LittleFinitistic.IdempotentTensor.spaceMap
theorem OAI.LittleFinitistic.IdempotentTensor.tensor_exact line 69
Source documentation
Tensor with the actual projective eA preserves every exact module sequence.
```
theorem tensor_exact (he : e*e=e) (f : N →ₗ[A] N') (g : N' →ₗ[A] N'')
    (h : Function.Exact f g) :
    Function.Exact (BalancedTensor.mapRightTo (k := k) (M := rightIdeal e) f)
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.mapRightTo, OAI.LittleFinitistic.IdempotentTensor.rightIdeal