OAI/GroupTheory/PolycyclicRecognition/Finiteness/ProjectiveTensorCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Tensoring projectives by an integer-projective coefficient

The internal Hom is exact on epimorphisms when its first argument is projective over the integers. The tensor–Hom adjunction then preserves projective representations, with no finite-rank assumption.

  1. theorem OAI.PolycyclicRecognition.representation_ihom_preserves_epimorphisms line 17
  2. theorem OAI.PolycyclicRecognition.representation_tensor_projective line 27