OAI/Algebra/Finitistic/Localization/AmbientQuotientEvaluation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.QuadraticEncoding.Ambient line 15

    Source documentation

    The ambient homotopy category; no bounded-projective identification is asserted here.

    abbrev Ambient := HomotopyCategory (ModuleCat.{u} (B P)ᵐᵒᵖ) (ComplexShape.up ℤ)

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.B

  2. def OAI.LittleFinitistic.QuadraticEncoding.degreeZero line 17
  3. def OAI.LittleFinitistic.QuadraticEncoding.coneS line 18
  4. def OAI.LittleFinitistic.QuadraticEncoding.coneS' line 20
  5. def OAI.LittleFinitistic.QuadraticEncoding.coneGenerators line 23
  6. def OAI.LittleFinitistic.QuadraticEncoding.ambientDenominators line 25
  7. abbrev OAI.LittleFinitistic.QuadraticEncoding.AmbientQuotient line 29

    Source documentation

    A quotient fixed before Y is chosen, for the ambient homotopy category.

    abbrev AmbientQuotient := (ambientDenominators P).Localization
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.ambientDenominators

  8. lemma OAI.LittleFinitistic.QuadraticEncoding.eval_single_isIso line 33
  9. lemma OAI.LittleFinitistic.QuadraticEncoding.evaluation_coneS_zero line 49
  10. lemma OAI.LittleFinitistic.QuadraticEncoding.evaluation_coneS'_zero line 58
  11. lemma OAI.LittleFinitistic.QuadraticEncoding.kills_coneGenerators line 67
  12. def OAI.LittleFinitistic.QuadraticEncoding.ambientQuotientEvaluation line 74

    Source documentation

    Actual tensor evaluation on the ambient quotient, with the generator hypotheses proved.

    def ambientQuotientEvaluation : AmbientQuotient P ⥤
    HomotopyCategory (ModuleCat.{max u v} k) (ComplexShape.up ℤ) :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.AmbientQuotient

  13. def OAI.LittleFinitistic.QuadraticEncoding.ambientQuotientEvaluationFactors line 79