OAI/Algebra/Finitistic/Localization/AdditiveSplitImage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.AdditiveSplitImage.fixed line 14
2. theorem OAI.LittleFinitistic.AdditiveSplitImage.mem_fixed line 16
3. def OAI.LittleFinitistic.AdditiveSplitImage.forward line 19
4. def OAI.LittleFinitistic.AdditiveSplitImage.inverse line 27
5. def OAI.LittleFinitistic.AdditiveSplitImage.equiv line 31

   Source documentation

   Any additive module-valued functor preserves the actual image of a split idempotent.

   def equiv : F.obj V ≃ₗ[R] fixed F i p where
   …

   Mentions: OAI.LittleFinitistic.AdditiveSplitImage.fixed

6. theorem OAI.LittleFinitistic.AdditiveSplitImage.equiv_apply_val line 44
7. theorem OAI.LittleFinitistic.AdditiveSplitImage.equiv_symm_apply line 45