OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorGlobalDimension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The source tensor algebra bound uses exactly 3(l+1) directed vertices, on both sides.

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

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

2. theorem OAI.LittleFinitistic.OrdinarySimulation.tensor_projectiveDimension_bound line 22

   Source documentation

   The corresponding bound holds for each arbitrary left or right module.

   theorem tensor_projectiveDimension_bound (DB : DirectedBound.DirectedSystem k B 3) (l : ℕ) :
       (∀ M : ModuleCat.{max u v} (B ⊗[k] ChainAlgebra k l), projectiveDimension M ≤ (3*l+2 : ℕ)) ∧
       (∀ M : ModuleCat.{max u v} (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ, projectiveDimension M ≤ (3*l+2 : ℕ)) := by
   …

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

3. theorem OAI.LittleFinitistic.OrdinarySimulation.source_tensor_globalDimension_bound line 34

   Source documentation

   The bound for the actual three-vertex coefficient algebra used by the manuscript.

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

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