OAI/Algebra/Finitistic/Dimension/PDBarDetection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.PDBar.tensorComplex line 14
2. def OAI.LittleFinitistic.PDBar.torIsoResolution line 19

   Source documentation

   Any actual projective resolution computes the same Tor, including the constructed absolute bar resolution.

   def torIsoResolution (P : ProjectiveResolution M.cat) (n : ℕ) :
       PDTensor.Tor (k := k) U M.cat n ≅ (tensorComplex M U P).homology n :=
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDBar.tensorComplex

3. abbrev OAI.LittleFinitistic.PDBar.resolution line 23
4. def OAI.LittleFinitistic.PDBar.torIsoBar line 26

   Source documentation

   No extra identification between the bar augmentation and M is assumed.

   def torIsoBar (n : ℕ) :
       PDTensor.Tor (k := k) U M.cat n ≅ (tensorComplex M U (resolution M)).homology n :=
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDBar.tensorComplex, OAI.LittleFinitistic.PDBar.resolution

5. theorem OAI.LittleFinitistic.PDBar.pdLE_iff_residue_resolution line 31
6. theorem OAI.LittleFinitistic.PDBar.pdLE_iff_simple_resolution line 37