OrdinaryResolutionModels.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex line 12
Source documentation
A finite model for tensoring a genuine bimodule complex, with its support and right projectivity proved.
```
structure FiniteProjectiveBimoduleComplex (k S A : Type u) [Field k] [Ring S] [Ring A]
    [Algebra k S] [Algebra k A] where
…
```
instance OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex.rightTerm_projective line 25
abbrev OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex.tensorFunctor line 28
theorem OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex.tensorFunctor_quasiIso line 31
Source documentation
The certified model inverts every input quasi-isomorphism; no condition is placed on the input complex.
```
theorem tensorFunctor_quasiIso {Z Z' : CochainComplex (ModuleCat.{u} A) ℤ} (f : Z ⟶ Z') [QuasiIso f] :
    QuasiIso (Q.tensorFunctor.map f) :=
…
```
def OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex.derivedTensor line 37
def OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex.comparison line 40
structure OAI.LittleFinitistic.BoundedBimoduleResolution line 45
Source documentation
A genuine ordinary bimodule supplied with an actual bounded right-projective resolution.
```
structure BoundedBimoduleResolution (k S A : Type u) [Field k] [Ring S] [Ring A]
    [Algebra k S] [Algebra k A] (M : ModuleCat.{u} (S ⊗[k] Aᵐᵒᵖ)) extends FiniteProjectiveBimoduleComplex k S A where
…
```
Mentions: OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex
def OAI.LittleFinitistic.BoundedBimoduleResolution.tensorOrdinary line 61
Source documentation
The resolved ordinary tensor object, in the native derived category retaining both outside actions. The resolution, its quasi-isomorphism, finite support and right projectivity are fields of Q.
```
def tensorOrdinary : DerivedCategory (ModuleCat.{u} (S ⊗[k] Bᵐᵒᵖ)) :=
…
```