OAI/GroupTheory/PolycyclicRecognition/Algebra/SmallCoefficientConstants.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Removing the constant functions from the small coefficient ring

The constant copy of the integers is a subrepresentation. Its quotient is again projective over the integers: evaluation at the identity splits the underlying sequence. The splitting is not asserted to be equivariant.

  1. def OAI.PolycyclicRecognition.smallCoefficientConstant line 18
  2. def OAI.PolycyclicRecognition.smallCoefficientEvaluation line 23
  3. theorem OAI.PolycyclicRecognition.smallCoefficientEvaluation_constant line 29
  4. def OAI.PolycyclicRecognition.smallCoefficientUnit line 32
  5. def OAI.PolycyclicRecognition.smallCoefficientConstants line 40
  6. theorem OAI.PolycyclicRecognition.smallCoefficientConstants_invariant line 43
  7. abbrev OAI.PolycyclicRecognition.smallCoefficientQuotient line 49
  8. def OAI.PolycyclicRecognition.smallCoefficientQuotientMap line 53
  9. def OAI.PolycyclicRecognition.smallCoefficientReduction line 57
  10. theorem OAI.PolycyclicRecognition.smallCoefficientReduction_constant line 60
  11. def OAI.PolycyclicRecognition.smallCoefficientQuotientSection line 66

    Source documentation

    An integer-linear section of the quotient by the constant functions.

    def smallCoefficientQuotientSection :
    smallCoefficientQuotient G →ₗ[ℤ] SmallCoefficientRing G :=
…

    Mentions: OAI.PolycyclicRecognition.smallCoefficientQuotient, OAI.PolycyclicRecognition.SmallCoefficientRing

  12. theorem OAI.PolycyclicRecognition.smallCoefficientQuotient_section line 72
  13. theorem OAI.PolycyclicRecognition.smallCoefficientQuotient_integer_projective line 87
  14. theorem OAI.PolycyclicRecognition.smallCoefficientUnit_quotient line 92
  15. def OAI.PolycyclicRecognition.smallCoefficientSequence line 100
  16. theorem OAI.PolycyclicRecognition.smallCoefficientSequence_shortExact line 104