OAI/Algebra/Finitistic/Ordinary/OrdinaryGlobalDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.OrdinarySimulation.ordinary_globalDimension_bound line 13

   Source documentation

   The manuscript's exact bound for D, on both sides and for arbitrary modules.

   theorem ordinary_globalDimension_bound (DB : DirectedBound.DirectedSystem k B 3) (l : ℕ) :
       (⨆ M : ModuleCat.{max u v} (AlgebraD k l B), projectiveDimension M) ≤ (3*l+2 : ℕ) ∧
       (⨆ M : ModuleCat.{max u v} (AlgebraD k l B)ᵐᵒᵖ, projectiveDimension M) ≤ (3*l+2 : ℕ) := by
   …

   Mentions: OAI.LittleFinitistic.DirectedBound.DirectedSystem, OAI.LittleFinitistic.OrdinarySimulation.AlgebraD

2. theorem OAI.LittleFinitistic.OrdinarySimulation.source_ordinary_globalDimension_bound line 33

   Source documentation

   The bound for the actual three-vertex coefficient algebra and the actual Section 5 product D.

   theorem source_ordinary_globalDimension_bound (μ : W →ₗ[k] V →ₗ[k] U) (l : ℕ) :
       (⨆ M : ModuleCat.{max u v} (AlgebraD k l (ThreeVertexAlgebra μ)), projectiveDimension M) ≤ (3*l+2 : ℕ) ∧
       (⨆ M : ModuleCat.{max u v} (AlgebraD k l (ThreeVertexAlgebra μ))ᵐᵒᵖ, projectiveDimension M) ≤ (3*l+2 : ℕ) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.AlgebraD, OAI.LittleFinitistic.ThreeVertexAlgebra