OAI/Algebra/Finitistic/Localization/QuotientActionEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.QuadraticEncoding.quotientVertexIso line 13

   Source documentation

   The canonical evaluation identification on each vertex of the fixed quotient.

   def quotientVertexIso (i : Fin 3) :
       (boundedQuotientEvaluation X).obj (vertexQ P i) ≅
         (vectorStalk (k := k)).obj (ModuleCat.of k (ULift.{u} Y)) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluation, OAI.LittleFinitistic.QuadraticEncoding.vertexQ, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk

2. lemma OAI.LittleFinitistic.QuadraticEncoding.quotient_arrow01_square line 18
3. lemma OAI.LittleFinitistic.QuadraticEncoding.quotient_arrow12_square line 27
4. lemma OAI.LittleFinitistic.QuadraticEncoding.actionArrow_zero line 36
5. lemma OAI.LittleFinitistic.QuadraticEncoding.quotient_inverse_s_square line 38
6. theorem OAI.LittleFinitistic.QuadraticEncoding.normalizedGenerator_evaluates line 47

   Source documentation

   The normalized quotient generator evaluates to the given generator on Y.

   theorem normalizedGenerator_evaluates (h : Fin d) :
       (boundedQuotientEvaluation X).map (normalizedGenerator P h) ≫ (quotientVertexIso X 0).hom =
         (quotientVertexIso X 0).hom ≫ (vectorStalk (k := k)).map (actionArrow X h.succ) := by
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluation, OAI.LittleFinitistic.QuadraticEncoding.normalizedGenerator, OAI.LittleFinitistic.QuadraticEncoding.quotientVertexIso, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk, OAI.LittleFinitistic.QuadraticEncoding.actionArrow