HomogeneousCochainCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Coordinates for scalar homogeneous cochains

The first vertex records translation and the remaining vertices record relative positions. This identifies controlled-support homogeneous cochains with arbitrary cochains valued in the group ring.

def OAI.PolycyclicRecognition.homogeneousCoordinates line 21
theorem OAI.PolycyclicRecognition.homogeneousCoordinates_apply line 34
theorem OAI.PolycyclicRecognition.controlled_homogeneous_of_finsupp line 41
Source documentation
Arbitrary group-ring-valued cochains have finite support at each controlled scale after passing to scalar homogeneous coordinates.
```
theorem controlled_homogeneous_of_finsupp (f : (Fin n → G) → (G →₀ R)) :
    (fun x => f (homogeneousCoordinates x).1 (homogeneousCoordinates x).2) ∈
      controlledCochains R G n := by
…
```
Mentions: OAI.PolycyclicRecognition.homogeneousCoordinates, OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.finite_support_homogeneous_coefficient line 61
Source documentation
Recovering a coefficient function from a homogeneous cochain produces a finite support, since all translated copies have the same finite scale.
```
theorem finite_support_homogeneous_coefficient (c : controlledCochains R G n)
    (a : Fin n → G) :
    (support (fun h => c (homogeneousCoordinates.symm (a, h)))).Finite := by
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
def OAI.PolycyclicRecognition.homogeneousCochainEquiv line 83
Source documentation
The concrete coordinate isomorphism underlying the group-ring cohomology comparison. No equivariance of the coarse map is needed.
```
def homogeneousCochainEquiv : ((Fin n → G) → (G →₀ R)) ≃ₗ[R] controlledCochains R G n where
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains