OAI/Algebra/Finitistic/Selected/SelectedBaseIterates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedBaseIterates.input line 11

   Source documentation

   The actual first-block D-module underlying the inflated A-module.

   abbrev input (Y : FiniteSelectionFamily.S.{0}) := ModuleCat.of D (Inflated Y)
   …

2. instance OAI.LittleFinitistic.SelectedBaseIterates.input_finiteD line 21
3. instance OAI.LittleFinitistic.SelectedBaseIterates.input_finite line 24
4. abbrev OAI.LittleFinitistic.SelectedBaseIterates.object line 31

   Source documentation

   Genuine bar-derived iteration of the actual X over the actual D.

   abbrev object (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :=
   …

5. theorem OAI.LittleFinitistic.SelectedBaseIterates.cohomology_finite line 34
6. theorem OAI.LittleFinitistic.SelectedBaseIterates.bounded line 47

   Source documentation

   A global-dimension bound on D bounds the amplitude of every derived iterate.

   theorem bounded (g : ℕ) (hg : ∀ M : ModuleCat.{0} D, HasProjectiveDimensionLE M g)
       (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :
       (object Y r).IsGE (-((r*(g+2) : ℕ) : ℤ)) ∧ (object Y r).IsLE 0 :=
   …

   Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object