SourceFiltrationReal.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExternalTensor.Section4.SourceFiltration.inr_prod line 14
theorem OAI.ExternalTensor.Section4.SourceFiltration.inclusion_product line 27
Source documentation
The canonical zero-column inclusion has exactly its original term coordinate.
```
theorem inclusion_product (n : ℤ) :
    (inclusion (p2 t) 0 (h2 t)).f n ≫ (totalTermIso (p2 t) 0 (h2 t) n).hom =
      ModuleCat.ofHom (LinearMap.inr (Enveloping k B)
        (Z.X (n+2) × Z.X (n+1)) (t.V₂.X n)) := by
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.p2, OAI.ExternalTensor.Section4.SourceFiltration.h2, OAI.ExternalTensor.Section4.Enveloping
theorem OAI.ExternalTensor.Section4.SourceFiltration.inclusion2_bijective line 40
Source documentation
Removing the two zero columns preserves the actual V2 inclusion.
```
theorem inclusion2_bijective (n : ℤ) :
    Function.Bijective ((inclusion (p2 t) 0 (h2 t)).f n) := by
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.p2, OAI.ExternalTensor.Section4.SourceFiltration.h2
instance OAI.ExternalTensor.Section4.SourceFiltration.inclusion2_isIso line 54
def OAI.ExternalTensor.Section4.SourceFiltration.v2Iso line 59
def OAI.ExternalTensor.Section4.SourceFiltration.v2Inclusion line 62
Source documentation
F>=2 really is V2, embedded by its original vertex summand inclusion.
```
def v2Inclusion : t.V₂ ⟶ total (p1 t) 0 (h1 t) :=
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.p1, OAI.ExternalTensor.Section4.SourceFiltration.h1
theorem OAI.ExternalTensor.Section4.SourceFiltration.v2Inclusion_eq line 66
theorem OAI.ExternalTensor.Section4.SourceFiltration.v2_shortExact line 72
Source documentation
The source-one sequence with V2 itself as its first term.
```
theorem v2_shortExact (n : ℤ) :
    Function.Injective ((v2Inclusion t).f n) ∧
    Function.Exact ((v2Inclusion t).f n) ((quotient1 t).totalMap.f n) ∧
    Function.Surjective ((quotient1 t).totalMap.f n) := by
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.v2Inclusion, OAI.ExternalTensor.Section4.SourceFiltration.quotient1
theorem OAI.ExternalTensor.Section4.SourceFiltration.v2_nested line 91
Source documentation
The composite filtration inclusion is the original V2-to-total map.
```
theorem v2_nested : v2Inclusion t ≫ (include1 t h).totalMap =
    t.in₂ ≫ inclusion t.p t.q h := by
…
```
Mentions: OAI.ExternalTensor.Section4.SourceFiltration.v2Inclusion, OAI.ExternalTensor.Section4.SourceFiltration.include1, OAI.ExternalTensor.Section4.h