InducedDiagram.lean`

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.ExternalTensor.Section4.biFiniteBiproducts line 11
instance OAI.ExternalTensor.Section4.biBinaryBiproducts line 13
theorem OAI.ExternalTensor.Section4.smul_comp_add line 16
def OAI.ExternalTensor.Section4.framedMapHomotopy line 22
structure OAI.ExternalTensor.Section4.Quadratic line 40
Source documentation
Only the finite quadratic diagram data used in the column calculation. These equations hold for Section 3's arrows in e_j B e_i and relation basis. No independence of relations is needed for the stronger assembly statement.
```
structure Quadratic where
…
```
def OAI.ExternalTensor.Section4.relationMap line 57
Source documentation
The actual finite relation evaluated on the chosen chain maps.
```
def relationMap (r : R) : D₀ ⟶ D₂ := ∑ a, ∑ b, s.coeff r a b • (f a ≫ g b)
```
def OAI.ExternalTensor.Section4.inducedData line 60
Source documentation
All columns and components are induced from actual modules, paths and maps.
```
def inducedData : AssemblyData (C := BiComplex k B) (A := A) (J := J) (R := R) where
…
```
Mentions: OAI.ExternalTensor.Section4.AssemblyData, OAI.ExternalTensor.Section4.BiComplex
abbrev OAI.ExternalTensor.Section4.L0Prime line 82
abbrev OAI.ExternalTensor.Section4.L1Prime line 83
abbrev OAI.ExternalTensor.Section4.L2Prime line 84
abbrev OAI.ExternalTensor.Section4.p line 85
abbrev OAI.ExternalTensor.Section4.q line 86
theorem OAI.ExternalTensor.Section4.p_arrow01 line 89
theorem OAI.ExternalTensor.Section4.p_arrow12 line 98
theorem OAI.ExternalTensor.Section4.q_relation line 106
def OAI.ExternalTensor.Section4.positiveHomotopy line 123
Source documentation
Positive degree-minus-one h of the manuscript, packaged with its equation.
```
def positiveHomotopy :
    Homotopy (biproduct.desc fun r =>
      (inducedData s D₀ D₁ D₂ f g).rel r ≫ (inducedData s D₀ D₁ D₂ f g).in₂) 0 := by
…
```
Mentions: OAI.ExternalTensor.Section4.inducedData
def OAI.ExternalTensor.Section4.nullHomotopy line 141
Source documentation
The sign-correct null-homotopy required by RectificationTotal.total.
```
def nullHomotopy : Homotopy (q s D₀ D₁ D₂ f g ≫ p s D₀ D₁ D₂ f g) 0 := by
…
```
Mentions: OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.p
def OAI.ExternalTensor.Section4.h line 146
Source documentation
The manuscript h, with zero components away from degree minus one.
```
def h (i j : ℤ) := (positiveHomotopy s D₀ D₁ D₂ f g H).hom i j
```
Mentions: OAI.ExternalTensor.Section4.positiveHomotopy
theorem OAI.ExternalTensor.Section4.h_formula line 148
theorem OAI.ExternalTensor.Section4.h_relation line 153
theorem OAI.ExternalTensor.Section4.h_shape line 167
theorem OAI.ExternalTensor.Section4.square line 171
Source documentation
Precisely the remaining off-diagonal entry in the manuscript's d_P squared.
```
theorem square (n : ℤ) :
    h s D₀ D₁ D₂ f g H n (n-1) ≫ (L0Prime s D₀ D₁ D₂ f g).d (n-1) n +
    (q s D₀ D₁ D₂ f g ≫ p s D₀ D₁ D₂ f g).f n +
    (L2Prime s D₀ D₁ D₂ f g).d n (n+1) ≫ h s D₀ D₁ D₂ f g H (n+1) n = 0 := by
…
```
Mentions: OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.L0Prime, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.L2Prime