DiagramAssembly.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.ExternalTensor.Section4.AssemblyData line 15
Source documentation
The concrete column/map interface. No composite or null-homotopy is assumed. The three equations are path naturality, the algebra relations, and the chosen relation homotopies after column induction.
```
structure AssemblyData where
…
```
abbrev OAI.ExternalTensor.Section4.AssemblyData.L₀ line 35
abbrev OAI.ExternalTensor.Section4.AssemblyData.L₁ line 36
abbrev OAI.ExternalTensor.Section4.AssemblyData.L₂ line 37
abbrev OAI.ExternalTensor.Section4.AssemblyData.in₀ line 38
abbrev OAI.ExternalTensor.Section4.AssemblyData.in₁ line 39
abbrev OAI.ExternalTensor.Section4.AssemblyData.in₂ line 40
def OAI.ExternalTensor.Section4.AssemblyData.p line 42
def OAI.ExternalTensor.Section4.AssemblyData.q line 47
theorem OAI.ExternalTensor.Section4.AssemblyData.composite line 53
Source documentation
The complete cancellation in Section 4, including the minus sign.
```
theorem composite : s.q ≫ s.p =
    -(biproduct.desc fun r => s.rel r ≫ s.in₂) := by
…
```

def OAI.ExternalTensor.Section4.AssemblyData.sumHomotopy line 76

Source documentation

A componentwise specified finite sum of homotopies.

def sumHomotopy {E : Type*} [Category E] [Preadditive E]
    {X Y : CochainComplex E ℤ} {I : Type} [Fintype I]
    (f : I → (X ⟶ Y)) (H : ∀ i, Homotopy (f i) 0) :
    Homotopy (∑ i, f i) 0 where
…