SourceFiltration.lean`

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ExternalTensor.Section4.SourceFiltration.F1₀ line 16
Source documentation
Source at least one: the actual D1 and D2 vertex terms and D1 arrow terms.
```
abbrev F1₀ := t.V₁ ⊞ t.V₂
```
abbrev OAI.ExternalTensor.Section4.SourceFiltration.F1₁ line 17
def OAI.ExternalTensor.Section4.SourceFiltration.Z line 18
def OAI.ExternalTensor.Section4.SourceFiltration.p1 line 24
def OAI.ExternalTensor.Section4.SourceFiltration.h1 line 27
def OAI.ExternalTensor.Section4.SourceFiltration.p0 line 33
Source documentation
Source zero quotient: retain precisely the path-multiplication terms.
```
def p0 : (⨁ t.U) ⟶ t.V₀ := biproduct.desc t.pa₀
```
def OAI.ExternalTensor.Section4.SourceFiltration.q0 line 35
theorem OAI.ExternalTensor.Section4.SourceFiltration.q0_p0 line 38
def OAI.ExternalTensor.Section4.SourceFiltration.h0 line 43
theorem OAI.ExternalTensor.Section4.SourceFiltration.in_p line 49
theorem OAI.ExternalTensor.Section4.SourceFiltration.p_out line 57
theorem OAI.ExternalTensor.Section4.SourceFiltration.q_out line 63
def OAI.ExternalTensor.Section4.SourceFiltration.include1 line 70
Source documentation
The original summand inclusion, as a triple preserving the specified homotopy.
```
def include1 : MapData (p1 t) 0 (h1 t) t.p t.q h where
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.p1, OAI.ExternalTensor.Section4.SourceFiltration.h1, OAI.ExternalTensor.Section4.h
def OAI.ExternalTensor.Section4.SourceFiltration.quotient0 line 80
Source documentation
Projection onto the actual source-zero quotient. The condition only records that the supplied homotopy increases source index; it is proved for Section4 inputs below.
```
def quotient0 (hh : ∀ i j, h.hom i j ≫ (biprod.fst : t.L₀ ⟶ t.V₀).f j = 0) :
    MapData t.p t.q h (p0 t) (q0 t) (h0 t) where
…
```
Mentions: OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.SourceFiltration.p0, OAI.ExternalTensor.Section4.SourceFiltration.q0, OAI.ExternalTensor.Section4.SourceFiltration.h0
def OAI.ExternalTensor.Section4.SourceFiltration.p2 line 90
Source documentation
The second filtration step and its source-one quotient.
```
def p2 : Z (k := k) (B := B) ⟶ t.V₂ := 0
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.Z
def OAI.ExternalTensor.Section4.SourceFiltration.h2 line 92
def OAI.ExternalTensor.Section4.SourceFiltration.pGrade1 line 97
def OAI.ExternalTensor.Section4.SourceFiltration.hGrade1 line 99
def OAI.ExternalTensor.Section4.SourceFiltration.include2 line 104
def OAI.ExternalTensor.Section4.SourceFiltration.quotient1 line 112
theorem OAI.ExternalTensor.Section4.SourceFiltration.cast_hom line 125
Source documentation
Changing the endpoint proofs does not change a homotopy's components.
```
theorem cast_hom {X Y : BiComplex k B} {a b a' b' : X ⟶ Y}
    (ha : a = a') (hb : b = b') (e : Homotopy a b = Homotopy a' b')
    (v : Homotopy a b) : (cast e v).hom = v.hom := by
…
```
Mentions: OAI.ExternalTensor.Section4.BiComplex
theorem OAI.ExternalTensor.Section4.SourceFiltration.induced_h_out line 137
abbrev OAI.ExternalTensor.Section4.SourceFiltration.inducedInclude1 line 162
Source documentation
Actual Section 4 source filtration inclusion; no decomposition is assumed.
```
abbrev inducedInclude1 := include1 (inducedData s D₀ D₁ D₂ f g)
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.include1, OAI.ExternalTensor.Section4.inducedData
abbrev OAI.ExternalTensor.Section4.SourceFiltration.inducedQuotient0 line 165
Source documentation
Actual Section 4 source quotient; homotopy compatibility is proved above.
```
abbrev inducedQuotient0 := quotient0 (inducedData s D₀ D₁ D₂ f g)
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.quotient0, OAI.ExternalTensor.Section4.inducedData