OAI/GroupTheory/PolycyclicRecognition/Algebra/AscendingQuotientColimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete colimit of an ascending sequence of invariant relations

Every element is represented in the initial quotient. A class vanishes in the quotient by the union precisely when it vanishes at a finite stage.

  1. abbrev OAI.PolycyclicRecognition.RepresentationInvariant line 17
  2. def OAI.PolycyclicRecognition.invariantQuotientMap line 20
  3. def OAI.PolycyclicRecognition.ascendingQuotientDiagram line 29
  4. def OAI.PolycyclicRecognition.ascendingQuotientColimit line 49