OAI/Algebra/Finitistic/Selected/SelectedOrdinaryDimension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedOrdinaryDimension.bound line 11

   Source documentation

   A fixed numerical bound determined solely by the fixed selecting bimodule.

   abbrev bound : ℕ := 3 * length + 2

2. theorem OAI.LittleFinitistic.SelectedOrdinaryDimension.both_sides line 14

   Source documentation

   The actual D has the manuscript's global dimension bound on both sides.

   theorem both_sides :
       (⨆ M : ModuleCat.{0} D, projectiveDimension M) ≤ bound ∧
       (⨆ M : ModuleCat.{0} Dᵐᵒᵖ, projectiveDimension M) ≤ bound :=
   …

   Mentions: OAI.LittleFinitistic.SelectedOrdinaryDimension.bound

3. theorem OAI.LittleFinitistic.SelectedOrdinaryDimension.left_module line 19
4. theorem OAI.LittleFinitistic.SelectedOrdinaryDimension.right_module line 23