OAI/Algebra/Finitistic/Localization/SourceModelBridge.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SourceModelBridge.forgetProj line 12
2. abbrev OAI.LittleFinitistic.SourceModelBridge.ambient line 13
3. lemma OAI.LittleFinitistic.SourceModelBridge.ambient_property line 16
4. def OAI.LittleFinitistic.SourceModelBridge.toBounded line 31

   Source documentation

   Forgetting the projective subcategory gives actual bounded projective module complexes.

   def toBounded : SourceVerdier.K P ⥤ BoundedK P :=
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.K

5. instance OAI.LittleFinitistic.SourceModelBridge.(instance at line 33) line 33
6. instance OAI.LittleFinitistic.SourceModelBridge.(instance at line 34) line 34
7. instance OAI.LittleFinitistic.SourceModelBridge.(instance at line 39) line 39
8. instance OAI.LittleFinitistic.SourceModelBridge.(instance at line 40) line 40
9. abbrev OAI.LittleFinitistic.SourceModelBridge.rightStalk line 42
10. def OAI.LittleFinitistic.SourceModelBridge.stalkUnderlyingIso line 44
11. lemma OAI.LittleFinitistic.SourceModelBridge.stalkUnderlying_square line 49
12. def OAI.LittleFinitistic.SourceModelBridge.vertexIso line 63
13. lemma OAI.LittleFinitistic.SourceModelBridge.vertex_arrow01 line 69
14. lemma OAI.LittleFinitistic.SourceModelBridge.vertex_arrow12 line 87