OAI/Algebra/Finitistic/Localization/QuotientRelations.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.QuadraticEncoding.boundedKLinear line 16
2. instance OAI.LittleFinitistic.QuadraticEncoding.boundedQLinear line 17
3. lemma OAI.LittleFinitistic.QuadraticEncoding.pathMap_target line 19
4. def OAI.LittleFinitistic.QuadraticEncoding.pathModuleMap line 25

   Source documentation

   Left multiplication by a length-two path, as a linear family of module maps.

   def pathModuleMap : Paths k d →ₗ[k] (vertexModule P 0 ⟶ vertexModule P 2) where
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.Paths, OAI.LittleFinitistic.QuadraticEncoding.vertexModule

5. lemma OAI.LittleFinitistic.QuadraticEncoding.pathModuleMap_basis line 38
6. instance OAI.LittleFinitistic.QuadraticEncoding.degreeZeroAdditive line 45
7. instance OAI.LittleFinitistic.QuadraticEncoding.degreeZeroLinear line 48
8. def OAI.LittleFinitistic.QuadraticEncoding.vertexHomEquiv line 51
9. def OAI.LittleFinitistic.QuadraticEncoding.vertexHomMap line 57

   Source documentation

   Transport module maps to the concrete degree-zero objects of K.

   def vertexHomMap (i j : Fin 3) :
       (vertexModule P i ⟶ vertexModule P j) →ₗ[k] (vertexK P i ⟶ vertexK P j) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.vertexModule, OAI.LittleFinitistic.QuadraticEncoding.vertexK

10. lemma OAI.LittleFinitistic.QuadraticEncoding.vertexHomMap_eq line 62
11. lemma OAI.LittleFinitistic.QuadraticEncoding.vertexHomMap_comp line 69
12. def OAI.LittleFinitistic.QuadraticEncoding.pathQMap line 79
13. lemma OAI.LittleFinitistic.QuadraticEncoding.pathQMap_basis line 83
14. lemma OAI.LittleFinitistic.QuadraticEncoding.pathModuleMap_kills line 90
15. lemma OAI.LittleFinitistic.QuadraticEncoding.pathQMap_kills line 96
16. lemma OAI.LittleFinitistic.QuadraticEncoding.quotient_commutation line 100
17. lemma OAI.LittleFinitistic.QuadraticEncoding.quotient_homogenized line 106