OAI/Algebra/Finitistic/Rectification/ColumnFinite.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExternalTensor.Section4.forgetK line 13
2. instance OAI.ExternalTensor.Section4.forgetK_additive line 15
3. def OAI.ExternalTensor.Section4.columnKIso line 19
4. theorem OAI.ExternalTensor.Section4.finite_of_iso line 34
5. theorem OAI.ExternalTensor.Section4.column_finite line 39
6. abbrev OAI.ExternalTensor.Section4.termK line 44
7. theorem OAI.ExternalTensor.Section4.sum_finite line 47
8. theorem OAI.ExternalTensor.Section4.biprod_finite line 55
9. theorem OAI.ExternalTensor.Section4.biprod_term_finite line 64
10. theorem OAI.ExternalTensor.Section4.columns_finite line 79

    Source documentation

    Finite-dimensionality of the actual three induced columns, from exactly finite-dimensional B and finite generation of the right-module input terms.

    theorem columns_finite [FiniteDimensional k B]
        (h₀ : ∀ n, Module.Finite Bᵐᵒᵖ (D₀.X n))
        (h₁ : ∀ n, Module.Finite Bᵐᵒᵖ (D₁.X n))
        (h₂ : ∀ n, Module.Finite Bᵐᵒᵖ (D₂.X n)) (n : ℤ) :
        FiniteDimensional k ((forgetK k B).obj ((L0Prime s D₀ D₁ D₂ f g).X n)) ∧
        FiniteDimensional k ((forgetK k B).obj ((L1Prime s D₀ D₁ D₂ f g).X n)) ∧
        FiniteDimensional k ((forgetK k B).obj ((L2Prime s D₀ D₁ D₂ f g).X n)) := by
    …

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