HomogeneousRepresentationCochains.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Controlled cochains as maps from the standard resolution

The coefficient at the identity of an equivariant group-ring-valued map recovers the scalar cochain. Conversely diagonal translation reconstructs that equivariant map, with finite support supplied by controlled-support estimates.

def OAI.PolycyclicRecognition.homogeneousGroupRingValue line 19
theorem OAI.PolycyclicRecognition.homogeneousGroupRingValue_coeff line 22
theorem OAI.PolycyclicRecognition.homogeneousGroupRingValue_covariance line 26
def OAI.PolycyclicRecognition.homogeneousGroupRingLinear line 34
theorem OAI.PolycyclicRecognition.homogeneousGroupRingLinear_single line 39
def OAI.PolycyclicRecognition.homogeneousRepresentationCochain line 45
Source documentation
The reconstructed values give an actual morphism of group representations.
```
def homogeneousRepresentationCochain (c : controlledCochains R G n) :
    (Rep.standardComplex R G).X n ⟶ Rep.leftRegular R G :=
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.homogeneousRepresentationCochain_single_coeff line 61
theorem OAI.PolycyclicRecognition.representationCochain_translate line 67
theorem OAI.PolycyclicRecognition.representationCochain_controlled line 83
Source documentation
Evaluation at the identity has controlled support for every equivariant map from the homogeneous resolution.
```
theorem representationCochain_controlled
    (F : (Rep.standardComplex R G).X n ⟶ Rep.leftRegular R G) :
    (fun x => (F.hom (MonoidAlgebra.single x 1)).coeff 1) ∈
      controlledCochains R G n := by
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
def OAI.PolycyclicRecognition.representationControlledCochain line 103
Source documentation
Scalar coefficient extraction, with its support obligation proved.
```
def representationControlledCochain
    (F : (Rep.standardComplex R G).X n ⟶ Rep.leftRegular R G) :
    controlledCochains R G n :=
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.representationControlledCochain_homogeneous line 109
theorem OAI.PolycyclicRecognition.homogeneousRepresentationCochain_controlled line 116
def OAI.PolycyclicRecognition.homogeneousRepresentationCochainEquiv line 136
Source documentation
Controlled scalar cochains are exactly the equivariant cochains with coefficients in the left regular group ring.
```
def homogeneousRepresentationCochainEquiv :
    controlledCochains R G n ≃ₗ[R]
      ((Rep.standardComplex R G).X n ⟶ Rep.leftRegular R G) where
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains