ControlledGroupRingCoefficients.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recovering group-ring coefficients from controlled scalar cochains

Diagonal translation turns a scalar cochain into a finitely supported coefficient function. The covariance formula is the actual left regular action needed to identify these cochains with the standard group resolution.

theorem OAI.PolycyclicRecognition.finite_support_diagonal_translate line 19
Source documentation
Only finitely many diagonal translates of a fixed tuple can have a nonzero value under a controlled cochain.
```
theorem finite_support_diagonal_translate (c : controlledCochains R G n)
    (x : Fin (n + 1) → G) :
    (support (fun h => c (fun i => h⁻¹ * x i))).Finite := by
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
def OAI.PolycyclicRecognition.controlledGroupRingValue line 35
Source documentation
The group-ring value of a scalar homogeneous cochain.
```
def controlledGroupRingValue (c : controlledCochains R G n) (x : Fin (n + 1) → G) :
    G →₀ R := Finsupp.ofSupportFinite (fun h => c (fun i => h⁻¹ * x i))
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.controlledGroupRingValue_apply line 39
theorem OAI.PolycyclicRecognition.controlledGroupRingValue_one line 43
theorem OAI.PolycyclicRecognition.controlledGroupRingValue_covariance line 49
Source documentation
Equivariance is forced by diagonal translation; the group action is not inserted as an assumption on the coarse map.
```
theorem controlledGroupRingValue_covariance (c : controlledCochains R G n)
    (x : Fin (n + 1) → G) (g h : G) :
    controlledGroupRingValue c (fun i => g * x i) h =
      controlledGroupRingValue c x (g⁻¹ * h) := by
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains, OAI.PolycyclicRecognition.controlledGroupRingValue
theorem OAI.PolycyclicRecognition.controlledGroupRingValue_injective line 56
Source documentation
Recovering the coefficient at the identity recovers the scalar cochain.
```
theorem controlledGroupRingValue_injective :
    Injective (fun c : controlledCochains R G n => controlledGroupRingValue c) := by
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains, OAI.PolycyclicRecognition.controlledGroupRingValue