ControlledCochainComplex.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The complex of controlled homogeneous cochains

The square-zero identity is inherited from the standard homogeneous resolution; the support lemmas prove that its dual differential stays inside the controlled cochains.

def OAI.PolycyclicRecognition.controlledLinearExtension line 20
theorem OAI.PolycyclicRecognition.controlledLinearExtension_coboundary line 25
theorem OAI.PolycyclicRecognition.standardBoundary_squared line 32
theorem OAI.PolycyclicRecognition.controlledCoboundary_squared line 45
Source documentation
The actual controlled coboundary squares to zero.
```
theorem controlledCoboundary_squared (c : controlledCochains R G n) :
    controlledCoboundary (controlledCoboundary c) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains, OAI.PolycyclicRecognition.controlledCoboundary
def OAI.PolycyclicRecognition.controlledCochainComplex line 56
Source documentation
Locally finite scalar homogeneous cochains, with the standard alternating differential.
```
def controlledCochainComplex (R G : Type) [CommRing R] [Group G] :
    CochainComplex (ModuleCat R) ℕ :=
…
```
theorem OAI.PolycyclicRecognition.controlledCochainComplex_d line 65