OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicRegularExteriorObstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The exterior square detects a free cyclic orbit

The difference of two indices is invariant under simultaneous translation. It gives an equivariant map from the exterior square of the regular cyclic module to a trivial module with unboundedly many independent coordinates.

  1. abbrev OAI.PolycyclicRecognition.CyclicOrbitModule line 19
  2. def OAI.PolycyclicRecognition.cyclicShiftRepresentation line 21
  3. theorem OAI.PolycyclicRecognition.cyclicShiftRepresentation_single line 37
  4. def OAI.PolycyclicRecognition.cyclicDifferenceBilinear line 42
  5. theorem OAI.PolycyclicRecognition.cyclicDifferenceBilinear_single line 47
  6. def OAI.PolycyclicRecognition.cyclicDifferenceAlternating line 52
  7. def OAI.PolycyclicRecognition.cyclicExteriorDifference line 66
  8. theorem OAI.PolycyclicRecognition.cyclicExteriorDifference_single line 70
  9. theorem OAI.PolycyclicRecognition.cyclicDifferenceBilinear_shift line 77
  10. theorem OAI.PolycyclicRecognition.cyclicExteriorDifference_shift line 92
  11. def OAI.PolycyclicRecognition.rationalCyclicExteriorRepresentation line 105
  12. theorem OAI.PolycyclicRecognition.finite_cyclic_invariant_support line 113

    Source documentation

    An invariant map from a finite cyclic module to a direct sum has one finite support bound valid for every element.

    theorem finite_cyclic_invariant_support {M : Type} [AddCommGroup M] [Module K M]
    (ρ : Representation K (Multiplicative ℤ) M)
    [Module.Finite K[Multiplicative ℤ] ρ.asModule]
    (L : M →ₗ[K] (CyclicOrbitModule (K := K))) (hinv : ∀ g x, L (ρ g x) = L x) :
…

    Mentions: OAI.PolycyclicRecognition.CyclicOrbitModule

  13. theorem OAI.PolycyclicRecognition.rationalCyclicExterior_not_finite line 145