OAI/Algebra/Finitistic/Ordinary/OrdinaryProductComponent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ProductModules.firstSpace line 13

   Source documentation

   The actual first central-idempotent summand of an arbitrary product-ring module.

   def firstSpace : Submodule (L × R) M where
   …

2. def OAI.LittleFinitistic.ProductModules.firstScalar line 24
3. def OAI.LittleFinitistic.ProductModules.firstAction line 35
4. instance OAI.LittleFinitistic.ProductModules.firstModule line 64
5. abbrev OAI.LittleFinitistic.ProductModules.firstObject line 66
6. def OAI.LittleFinitistic.ProductModules.firstMap line 70
7. def OAI.LittleFinitistic.ProductModules.firstFunctor line 78

   Source documentation

   The actual component functor, constructed on every module and map.

   def firstFunctor : ModuleCat.{v} (L × R) ⥤ ModuleCat.{v} L where
   …

8. theorem OAI.LittleFinitistic.ProductModules.firstMap_surjective line 85

   Source documentation

   Surjections remain surjections on the selected component, by projecting a preimage.

   theorem firstMap_surjective (f : M ⟶ N) (hf : Function.Surjective f.hom) :
       Function.Surjective (firstMap L R f) := by
   …

   Mentions: OAI.LittleFinitistic.ProductModules.firstMap