OAI/Algebra/Finitistic/Ordinary/OrdinaryProductSecondDimension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ProductModules.swapInflationEquiv line 15

   Source documentation

   Swapping product factors identifies the two actual inflation constructions.

   def swapInflationEquiv (P : ModuleCat.{v} R) :
       (firstInflation R L).obj P ≃ₛₗ[RingHomClass.toRingHom (RingEquiv.prodComm : R × L ≃+* L × R)]
         (secondInflation L R).obj P where
   …

   Mentions: OAI.LittleFinitistic.ProductModules.firstInflation, OAI.LittleFinitistic.ProductModules.secondInflation

2. theorem OAI.LittleFinitistic.ProductModules.secondInflation_dimensionLE line 27
3. theorem OAI.LittleFinitistic.ProductModules.product_module_bound line 34

   Source documentation

   Each module over the product has the same finite bound as its two factors.

   theorem product_module_bound (n : ℕ)
       (hL : ∀ M : ModuleCat.{v} L, projectiveDimension M ≤ (n : ℕ))
       (hR : ∀ M : ModuleCat.{v} R, projectiveDimension M ≤ (n : ℕ))
       (M : ModuleCat.{v} (L × R)) : projectiveDimension M ≤ (n : ℕ) := by
   …