OAI/Algebra/Finitistic/Localization/SourceQuotientAction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SourceQuotientAction.vertexIso line 17

   Source documentation

   The two concrete presentations of the same right ideal e_i B.

   def vertexIso (i : Fin 3) : (SourceVerdier.E P i).obj ≅ vertexModule P i :=
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.E

2. def OAI.LittleFinitistic.SourceQuotientAction.nativeHom line 21
3. lemma OAI.LittleFinitistic.SourceQuotientAction.nativeHom_comp line 37
4. lemma OAI.LittleFinitistic.SourceQuotientAction.nativeHom_arrow01 line 45
5. lemma OAI.LittleFinitistic.SourceQuotientAction.nativeHom_arrow12 line 51
6. instance OAI.LittleFinitistic.SourceQuotientAction.singleAdditive line 58
7. instance OAI.LittleFinitistic.SourceQuotientAction.singleLinear line 60
8. instance OAI.LittleFinitistic.SourceQuotientAction.stalkAdditive line 62
9. instance OAI.LittleFinitistic.SourceQuotientAction.stalkLinear line 65
10. abbrev OAI.LittleFinitistic.SourceQuotientAction.vertex line 72
11. abbrev OAI.LittleFinitistic.SourceQuotientAction.a01 line 74
12. abbrev OAI.LittleFinitistic.SourceQuotientAction.a12 line 76
13. instance OAI.LittleFinitistic.SourceQuotientAction.(instance at line 78) line 78
14. instance OAI.LittleFinitistic.SourceQuotientAction.(instance at line 79) line 79
15. def OAI.LittleFinitistic.SourceQuotientAction.path line 81
16. lemma OAI.LittleFinitistic.SourceQuotientAction.path_basis line 85
17. lemma OAI.LittleFinitistic.SourceQuotientAction.path_kills line 91
18. lemma OAI.LittleFinitistic.SourceQuotientAction.commutation line 96
19. lemma OAI.LittleFinitistic.SourceQuotientAction.homogenized line 101
20. def OAI.LittleFinitistic.SourceQuotientAction.theta line 110

    Source documentation

    The actual theta on E0 in the primary's source Verdier quotient.

    def theta {R : Type*} [Ring R] [Algebra k R] (E : SelectionEncoding.Encoding k R) :
        R →ₐ[k] End (vertex E.relations 0) :=
    …

    Mentions: OAI.LittleFinitistic.SelectionEncoding.Encoding, OAI.LittleFinitistic.SourceQuotientAction.vertex