OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalModuleFunctor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rationalization as a functor to rational modules

The codomain remembers the rational scalar action. Flatness proves exactness; it does not assert a finite-dimensionality conclusion.

  1. def OAI.PolycyclicRecognition.rationalModuleFunctor line 18
  2. instance OAI.PolycyclicRecognition.(instance at line 28) line 28
  3. theorem OAI.PolycyclicRecognition.rationalModuleFunctor_map_exact line 34
  4. instance OAI.PolycyclicRecognition.(instance at line 42) line 42
  5. def OAI.PolycyclicRecognition.rationalModuleHomologyIso line 45
  6. theorem OAI.PolycyclicRecognition.rationalModuleHomologyIso_naturality line 50