OAI/Algebra/Finitistic/Selected/SelectedUnderlyingHomology.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedUnderlyingHomology.tensorMap line 15

   Source documentation

   Tensor an actual map of the underlying right-module complexes.

   abbrev tensorMap {D E : SourceVerdier.K P}
       (f : UnderlyingRepresentatives.complex P D ⟶ UnderlyingRepresentatives.complex P E) :=
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.K, OAI.LittleFinitistic.UnderlyingRepresentatives.complex

2. lemma OAI.LittleFinitistic.SelectedUnderlyingHomology.derived_map line 20
3. lemma OAI.LittleFinitistic.SelectedUnderlyingHomology.comparison_map line 47
4. lemma OAI.LittleFinitistic.SelectedUnderlyingHomology.homology_arrow line 62
5. lemma OAI.LittleFinitistic.SelectedUnderlyingHomology.arrow01 line 82
6. lemma OAI.LittleFinitistic.SelectedUnderlyingHomology.arrow12 line 91