Basic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.littleFinitisticDimension line 15
Source documentation
The little finitistic dimension: the supremum of the actual projective dimensions of finitely generated modules whose projective dimension is finite. The value of the zero module follows mathlib's -∞ convention.
Distinct definitions of this name: ComparatorChallenges/FinitisticAsymmetry.lean:13 (same declaration text), ComparatorChallenges/LittleFinitistic.lean:17 (different declaration text). Qualify references as OAI.LittleFinitistic.littleFinitisticDimension@path.
```
def littleFinitisticDimension : WithBot ℕ∞ :=
…
```
theorem OAI.LittleFinitistic.le_littleFinitisticDimension line 19

theorem OAI.LittleFinitistic.littleFinitisticDimension_eq_top_of_unbounded line 27

Source documentation

Unbounded finite projective dimensions of actual finitely generated modules force the little finitistic dimension to be infinite.

theorem littleFinitisticDimension_eq_top_of_unbounded
    (h : ∀ n : ℕ, ∃ M : ModuleCat.{u} A, Module.Finite A M ∧
      projectiveDimension M < ⊤ ∧ (n : WithBot ℕ∞) ≤ projectiveDimension M) :
    littleFinitisticDimension A = ⊤ := by
…

theorem OAI.LittleFinitistic.littleFinitisticDimension_eq_top_of_two_mul_bounds line 39

Source documentation

The manuscript's concrete lower-bound pattern is sufficient; all finite projective-dimension premises must still be supplied by the constructed modules.

theorem littleFinitisticDimension_eq_top_of_two_mul_bounds
    (h : ∀ m : ℕ, 0 < m → ∃ M : ModuleCat.{u} A, Module.Finite A M ∧
      projectiveDimension M < ⊤ ∧ ((2*m-2 : ℕ) : WithBot ℕ∞) ≤ projectiveDimension M) :
    littleFinitisticDimension A = ⊤ := by
…