OrdinaryFreeTensorExactness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BalancedTensor.Free.evaluation_naturality line 15

theorem OAI.LittleFinitistic.BalancedTensor.Free.finsupp_exact line 32

Source documentation

Direct sums preserve exactness, with a preimage supported on the given finite support.

theorem finsupp_exact (f : N →ₗ[A] N') (g : N' →ₗ[A] N'') (h : Function.Exact f g) :
    Function.Exact (Finsupp.mapRange.linearMap (f.restrictScalars k) : (I →₀ N) →ₗ[k] (I →₀ N'))
      (Finsupp.mapRange.linearMap (g.restrictScalars k)) := by
…

theorem OAI.LittleFinitistic.BalancedTensor.Free.tensor_exact line 57
Source documentation
Tensor by an arbitrary free right module preserves every exact module sequence.
```
theorem tensor_exact (f : N →ₗ[A] N') (g : N' →ₗ[A] N'') (h : Function.Exact f g) :
    Function.Exact (mapRightTo (k := k) (M := I →₀ Aᵐᵒᵖ) f)
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.mapRightTo