OAI/Algebra/Finitistic/Rectification/ColumnProperties.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExternalTensor.Section4.forgetRight line 16

   Source documentation

   Restrict genuine bimodules to right B-modules.

   def forgetRight : ModuleCat.{u} (Enveloping k B) ⥤ ModuleCat.{u} Bᵐᵒᵖ :=
   …

   Mentions: OAI.ExternalTensor.Section4.Enveloping

2. instance OAI.ExternalTensor.Section4.forgetRight_additive line 20
3. def OAI.ExternalTensor.Section4.columnRightIso line 25

   Source documentation

   The restricted action is the right action already verified for the actual tensor.

   def columnRightIso (e : B) (N : ModuleCat.{u} Bᵐᵒᵖ) :
       (forgetRight k B).obj ((columnFunctor k B e).obj N) ≅
         ModuleCat.of Bᵐᵒᵖ (Column k B N e) :=
   …

   Mentions: OAI.ExternalTensor.Section4.forgetRight, OAI.ExternalTensor.Section4.columnFunctor, OAI.ExternalTensor.Column

4. theorem OAI.ExternalTensor.Section4.column_right_projective line 40
5. theorem OAI.ExternalTensor.Section4.column_isZero line 47

   Source documentation

   Exact boundedness transfer for each induced column.

   theorem column_isZero (e : B) (D : RightComplex B) (i : ℤ)
       (hi : IsZero (D.X i)) : IsZero (((columnComplex k B e).obj D).X i) :=
   …

   Mentions: OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.columnComplex

6. instance OAI.ExternalTensor.Section4.rightFiniteBiproducts line 51
7. instance OAI.ExternalTensor.Section4.rightBinaryBiproducts line 53
8. abbrev OAI.ExternalTensor.Section4.termRight line 56
9. theorem OAI.ExternalTensor.Section4.sum_right_projective line 59
10. theorem OAI.ExternalTensor.Section4.biprod_right_projective line 72
11. theorem OAI.ExternalTensor.Section4.sum_isZero line 81
12. theorem OAI.ExternalTensor.Section4.sum_term_isZero line 90
13. theorem OAI.ExternalTensor.Section4.biprod_term_isZero line 95
14. theorem OAI.ExternalTensor.Section4.columns_right_projective line 108

    Source documentation

    Exactly the three right-projectivity inputs to RectificationTotal.total_projective_after.

    theorem columns_right_projective
        (h₀ : ∀ n, Module.Projective Bᵐᵒᵖ (D₀.X n))
        (h₁ : ∀ n, Module.Projective Bᵐᵒᵖ (D₁.X n))
        (h₂ : ∀ n, Module.Projective Bᵐᵒᵖ (D₂.X n)) (n : ℤ) :
        Projective ((forgetRight k B).obj ((L0Prime s D₀ D₁ D₂ f g).X n)) ∧
        Projective ((forgetRight k B).obj ((L1Prime s D₀ D₁ D₂ f g).X n)) ∧
        Projective ((forgetRight k B).obj ((L2Prime s D₀ D₁ D₂ f g).X n)) := by
    …

    Mentions: OAI.ExternalTensor.Section4.forgetRight, OAI.ExternalTensor.Section4.L0Prime, OAI.ExternalTensor.Section4.L1Prime, OAI.ExternalTensor.Section4.L2Prime

15. theorem OAI.ExternalTensor.Section4.columns_isZero line 135
16. theorem OAI.ExternalTensor.Section4.columns_bounded line 158

    Source documentation

    Uniform bounds on the input complexes give the same bounds on all three columns.

    theorem columns_bounded (lo hi : ℤ)
        (h₀ : ∀ n, n < lo ∨ hi < n → IsZero (D₀.X n))
        (h₁ : ∀ n, n < lo ∨ hi < n → IsZero (D₁.X n))
        (h₂ : ∀ n, n < lo ∨ hi < n → IsZero (D₂.X n)) :
        ∀ n, n < lo ∨ hi < n →
          IsZero ((L0Prime s D₀ D₁ D₂ f g).X n) ∧
          IsZero ((L1Prime s D₀ D₁ D₂ f g).X n) ∧
          IsZero ((L2Prime s D₀ D₁ D₂ f g).X n) :=
    …

    Mentions: OAI.ExternalTensor.Section4.L0Prime, OAI.ExternalTensor.Section4.L1Prime, OAI.ExternalTensor.Section4.L2Prime