SelectedMinimalResolution.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.SelectedMinimalResolution.finiteModule line 10
def OAI.LittleFinitistic.SelectedMinimalResolution.resolution line 14
Source documentation
A genuine minimal projective resolution of each actual constructed A-module.
```
def resolution (Y : FiniteSelectionFamily.S.{0}) : ProjectiveResolution (SelectedOrdinaryModules.module Y) :=
…
```
Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.module
theorem OAI.LittleFinitistic.SelectedMinimalResolution.dimension_iff line 19
Source documentation
The constructed A-module has projective dimension at most n precisely when its actual minimal projective resolution has zero term n+1.
```
theorem dimension_iff (Y : FiniteSelectionFamily.S.{0}) (n : ℕ) :
    HasProjectiveDimensionLE (SelectedOrdinaryModules.module Y) n ↔
      Subsingleton (PDMinimal.term (finiteModule Y) (n+1)) :=
…
```
Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.module, OAI.LittleFinitistic.PDMinimal.term, OAI.LittleFinitistic.SelectedMinimalResolution.finiteModule
theorem OAI.LittleFinitistic.SelectedMinimalResolution.projective line 25
Source documentation
The actual minimal-resolution terms are projective.
```
theorem projective (Y : FiniteSelectionFamily.S.{0}) (n : ℕ) :
    Projective ((resolution Y).complex.X n) := inferInstance
…
```
Mentions: OAI.LittleFinitistic.SelectedMinimalResolution.resolution