BalancedProjectiveLeft.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BalancedTensor.mapRightTo_split line 18
theorem OAI.LittleFinitistic.BalancedTensor.leftTensor_exact_of_split line 28
theorem OAI.LittleFinitistic.BalancedTensor.projectiveLeftTensor_exact line 48
Source documentation
Projectivity of the left input preserves every exact sequence in the right variable.
```
theorem projectiveLeftTensor_exact [Module.Projective A N]
    (f : M →ₗ[Aᵐᵒᵖ] M') (g : M' →ₗ[Aᵐᵒᵖ] M'') (h : Function.Exact f g) :
    Function.Exact (mapLeft (k := k) N f) (mapLeft (k := k) N g) := by
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.mapLeft
theorem OAI.LittleFinitistic.BimoduleBalancedTensor.projectiveInput_mapsExact line 65
Source documentation
Exactness of tensoring genuine bimodules with a projective left module, with the result still in B-Mod.
```
theorem projectiveInput_mapsExact
    (S : ShortComplex (ModuleCat.{u} (Enveloping k B))) (hS : S.Exact) :
    (S.map (functor k B N)).Exact := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor
theorem OAI.LittleFinitistic.BimoduleBalancedTensor.projectiveInput_preservesHomology line 82
theorem OAI.LittleFinitistic.BimoduleBalancedTensor.projectiveInput_quasiIso line 86
Source documentation
An actual bimodule augmentation quasi-isomorphism remains one on each projective input row.
```
theorem projectiveInput_quasiIso {P Q : BiComplex k B} (ε : P ⟶ Q) [QuasiIso ε] :
    QuasiIso (((functor k B N).mapHomologicalComplex (.up ℤ)).map ε) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BimoduleBalancedTensor.map