OrdinaryResolutionExact.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.supportedIdealEquiv line 13
Source documentation
In the supported range, the extended ideal is the source's actual right projective.
```
def supportedIdealEquiv (n : ℕ) (h : n ≤ l) :
    resolutionIdeal k l n ≃ₗ[(ChainAlgebra k l)ᵐᵒᵖ] rightTerm (k := k) (⟨n,by omega⟩ : Fin (l+1)) where
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionIdeal, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.supportedIdealEquiv_d line 29
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.supported_complex_exact line 37
Source documentation
The actual bundled complex is exact at every interior degree.
```
theorem supported_complex_exact (n : ℕ) (h : n+1 < l) :
    (ShortComplex.mk (resolutionDifferential k l n) (resolutionDifferential k l (n+1))
      (resolutionDifferential_square k l n)).Exact := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionDifferential, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionDifferential_square
def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionAugmentation line 50
Source documentation
The actual augmentation of the bundled complex in its last degree.
```
def resolutionAugmentation : resolutionTerm k l l ⟶ ModuleCat.of (ChainAlgebra k l)ᵐᵒᵖ (TerminalSimple k) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionTerm, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple
def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalAugmentationMap line 54
Source documentation
A genuine chain map to the terminal simple placed in degree l.
```
def terminalAugmentationMap : terminalProjectiveComplex k l ⟶
    (HomologicalComplex.single _ (.up ℕ) l).obj (ModuleCat.of (ChainAlgebra k l)ᵐᵒᵖ (TerminalSimple k)) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalProjectiveComplex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple