OAI/Algebra/Finitistic/Localization/ModuleActionCompatibility.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LittleFinitistic.QuadraticEncoding.quotientAction_square line 11
  2. def OAI.LittleFinitistic.QuadraticEncoding.presentationRepresentation line 26
  3. lemma OAI.LittleFinitistic.QuadraticEncoding.presentationRepresentation_givenAction line 30
  4. theorem OAI.LittleFinitistic.QuadraticEncoding.module_quotientAction_square line 39

    Source documentation

    For a genuinely presented algebra R, every element of theta evaluates to its R-module action.

    theorem module_quotientAction_square [Module R Y] [IsScalarTower k R Y] (r : R) :
    (boundedQuotientEvaluation (presentationRepresentation (Y := Y) e)).map
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluation, OAI.LittleFinitistic.QuadraticEncoding.presentationRepresentation