OAI/Algebra/Finitistic/Bar/StrictSupportExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.supportedExtensionXIso line 15

   Source documentation

   Actual component isomorphisms for extension after restriction of a complex which is already zero outside the index embedding.

   def supportedExtensionXIso (j : ι') : ((K.restriction e).extend e).X j ≅ K.X j := by
   …

2. theorem OAI.DerivedBar.supportedExtensionXIso_image line 23
3. def OAI.DerivedBar.strictSupportExtensionIso line 35

   Source documentation

   The genuine chain isomorphism, including all boundary differentials.

   def strictSupportExtensionIso : (K.restriction e).extend e ≅ K :=
   …