OAI/Algebra/Finitistic/Localization/BoundedQuotientGenerators.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.QuadraticEncoding.vertexK line 12

    Source documentation

    The actual degree-zero right vertex projective in K.

    def vertexK (i : Fin 3) : BoundedK P :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedK

  2. def OAI.LittleFinitistic.QuadraticEncoding.arrowK01 line 16
  3. def OAI.LittleFinitistic.QuadraticEncoding.arrowK12 line 19
  4. theorem OAI.LittleFinitistic.QuadraticEncoding.s_denominator line 23
  5. instance OAI.LittleFinitistic.QuadraticEncoding.quotient_s_isIso line 39
  6. theorem OAI.LittleFinitistic.QuadraticEncoding.s'_denominator line 42
  7. instance OAI.LittleFinitistic.QuadraticEncoding.quotient_s'_isIso line 58
  8. def OAI.LittleFinitistic.QuadraticEncoding.vertexQ line 62

    Source documentation

    The three actual images in the fixed quotient.

    def vertexQ (i : Fin 3) : BoundedQ P := (boundedDenominators P).Q.obj (vertexK P i)

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedQ, OAI.LittleFinitistic.QuadraticEncoding.boundedDenominators, OAI.LittleFinitistic.QuadraticEncoding.vertexK

  9. def OAI.LittleFinitistic.QuadraticEncoding.arrowQ01 line 63
  10. def OAI.LittleFinitistic.QuadraticEncoding.arrowQ12 line 65
  11. instance OAI.LittleFinitistic.QuadraticEncoding.arrowQ01_zero_isIso line 68
  12. instance OAI.LittleFinitistic.QuadraticEncoding.arrowQ12_zero_isIso line 69
  13. def OAI.LittleFinitistic.QuadraticEncoding.normalizedGenerator line 72

    Source documentation

    The normalized generator s^{-1} a_h on L=E_0 in Q.

    def normalizedGenerator (h : Fin d) : End (vertexQ P 0) :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.vertexQ