OAI/Algebra/Finitistic/Rectification/FiltrationExactness.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.data line 17
2. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.P line 18
3. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.F1 line 20
4. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.G0 line 21
5. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.G1 line 23
6. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.i1 line 26
7. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.pi0 line 28
8. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.i2 line 30
9. abbrev OAI.ExternalTensor.Section4.SourceFiltration.Exactness.pi1 line 32
10. theorem OAI.ExternalTensor.Section4.SourceFiltration.Exactness.exact_source_filtration line 37

    Source documentation

    Section 4's actual two nontrivial source-filtration steps. No decomposition, exactness, extra coherence, vertex equivalence, or main theorem is an input.

    theorem exact_source_filtration (n : ℤ) :
        (Function.Injective ((i1 s D₀ D₁ D₂ f g H).f n) ∧
         Function.Exact ((i1 s D₀ D₁ D₂ f g H).f n) ((pi0 s D₀ D₁ D₂ f g H).f n) ∧
         Function.Surjective ((pi0 s D₀ D₁ D₂ f g H).f n)) ∧
        (Function.Injective ((i2 s D₀ D₁ D₂ f g).f n) ∧
         Function.Exact ((i2 s D₀ D₁ D₂ f g).f n) ((pi1 s D₀ D₁ D₂ f g).f n) ∧
         Function.Surjective ((pi1 s D₀ D₁ D₂ f g).f n)) ∧
        i2 s D₀ D₁ D₂ f g ≫ i1 s D₀ D₁ D₂ f g H =
          (data s D₀ D₁ D₂ f g).in₂ ≫
            inclusion (p s D₀ D₁ D₂ f g) (q s D₀ D₁ D₂ f g)
              (nullHomotopy s D₀ D₁ D₂ f g H) :=
    …

    Mentions: OAI.ExternalTensor.Section4.SourceFiltration.Exactness.i1, OAI.ExternalTensor.Section4.SourceFiltration.Exactness.pi0, OAI.ExternalTensor.Section4.SourceFiltration.Exactness.i2, OAI.ExternalTensor.Section4.SourceFiltration.Exactness.pi1, OAI.ExternalTensor.Section4.SourceFiltration.Exactness.data, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.nullHomotopy

11. theorem OAI.ExternalTensor.Section4.SourceFiltration.Exactness.categorical_source0 line 52
12. theorem OAI.ExternalTensor.Section4.SourceFiltration.Exactness.categorical_source1 line 60