OAI/Algebra/Finitistic/Dimension/PDMinimalResolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDMinimal.complex line 14

   Source documentation

   The actual chain complex of the successive projective covers.

   def complex : ChainComplex (ModuleCat A) ℕ := ChainComplex.of
   …

2. theorem OAI.LittleFinitistic.PDMinimal.complex_d line 19
3. instance OAI.LittleFinitistic.PDMinimal.term_projective line 24
4. lemma OAI.LittleFinitistic.PDMinimal.complex_exactAt line 27
5. lemma OAI.LittleFinitistic.PDMinimal.complex_d_augment line 35
6. lemma OAI.LittleFinitistic.PDMinimal.complex_exact_augment line 39
7. instance OAI.LittleFinitistic.PDMinimal.augment_epi line 46
8. def OAI.LittleFinitistic.PDMinimal.resolution line 50

   Source documentation

   A projective resolution, including its augmentation quasi-isomorphism.

   def resolution : ProjectiveResolution M.cat where
   …