OAI/Algebra/Finitistic/Rectification/SourceFiltrationExact.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ExternalTensor.Section4.SourceFiltration.zeroTermSubsingleton line 12
  2. theorem OAI.ExternalTensor.Section4.SourceFiltration.source0_component0 line 20
  3. theorem OAI.ExternalTensor.Section4.SourceFiltration.source0_component1 line 26
  4. theorem OAI.ExternalTensor.Section4.SourceFiltration.source0_component2 line 32
  5. theorem OAI.ExternalTensor.Section4.SourceFiltration.source0_shortExact line 39

    Source documentation

    The actual F>=1 inclusion and source-zero quotient are termwise short exact.

    theorem source0_shortExact (n : ℤ) :
    Function.Injective ((include1 t h).totalMap.f n) ∧
    Function.Exact ((include1 t h).totalMap.f n) ((quotient0 t h hh).totalMap.f n) ∧
    Function.Surjective ((quotient0 t h hh).totalMap.f n) := by
…

    Mentions: OAI.ExternalTensor.Section4.SourceFiltration.include1, OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.SourceFiltration.quotient0

  6. theorem OAI.ExternalTensor.Section4.SourceFiltration.source1_component0 line 55
  7. theorem OAI.ExternalTensor.Section4.SourceFiltration.source1_component1 line 62
  8. theorem OAI.ExternalTensor.Section4.SourceFiltration.source1_component2 line 69
  9. theorem OAI.ExternalTensor.Section4.SourceFiltration.source1_shortExact line 79

    Source documentation

    The actual F>=2 inclusion and source-one quotient are termwise short exact.

    theorem source1_shortExact (n : ℤ) :
    Function.Injective ((include2 t).totalMap.f n) ∧
    Function.Exact ((include2 t).totalMap.f n) ((quotient1 t).totalMap.f n) ∧
    Function.Surjective ((quotient1 t).totalMap.f n) := by
…

    Mentions: OAI.ExternalTensor.Section4.SourceFiltration.include2, OAI.ExternalTensor.Section4.SourceFiltration.quotient1

  10. theorem OAI.ExternalTensor.Section4.SourceFiltration.induced_source0_shortExact line 101

    Source documentation

    No short-exactness or filtration assumption: all component properties are proved from the actual induced Section 4 sources.

    theorem induced_source0_shortExact (n : ℤ) :
    Function.Injective ((inducedInclude1 s D₀ D₁ D₂ f g H).totalMap.f n) ∧
    Function.Exact ((inducedInclude1 s D₀ D₁ D₂ f g H).totalMap.f n)
      ((inducedQuotient0 s D₀ D₁ D₂ f g H).totalMap.f n) ∧
    Function.Surjective ((inducedQuotient0 s D₀ D₁ D₂ f g H).totalMap.f n) :=
…

    Mentions: OAI.ExternalTensor.Section4.SourceFiltration.inducedInclude1, OAI.ExternalTensor.Section4.SourceFiltration.inducedQuotient0