OAI/Algebra/Finitistic/Rectification/ColumnComplex.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ExternalTensor.Section4.rightModuleK line 14
2. instance OAI.ExternalTensor.Section4.rightModuleTower line 16
3. abbrev OAI.ExternalTensor.Section4.Enveloping line 22
4. abbrev OAI.ExternalTensor.Section4.RightComplex line 23
5. abbrev OAI.ExternalTensor.Section4.BiComplex line 24
6. def OAI.ExternalTensor.Section4.columnFunctor line 27

   Source documentation

   Induction by the actual left ideal Be, on right modules and maps.

   def columnFunctor (e : B) : ModuleCat.{u} Bᵐᵒᵖ ⥤ ModuleCat.{u} (Enveloping k B) where
   …

   Mentions: OAI.ExternalTensor.Section4.Enveloping

7. instance OAI.ExternalTensor.Section4.columnFunctor_additive line 34
8. instance OAI.ExternalTensor.Section4.columnFunctor_linear line 37
9. abbrev OAI.ExternalTensor.Section4.columnComplex line 47
10. def OAI.ExternalTensor.Section4.pathNat line 51

    Source documentation

    Right multiplication on the left tensor factor, natural in the right module.

    def pathNat (ei ej a : B) (ha : a * ei = a) :
        columnFunctor k B ej ⟶ columnFunctor k B ei where
    …

    Mentions: OAI.ExternalTensor.Section4.columnFunctor

11. abbrev OAI.ExternalTensor.Section4.path line 62
12. theorem OAI.ExternalTensor.Section4.path_naturality line 66
13. theorem OAI.ExternalTensor.Section4.sum_f line 72
14. theorem OAI.ExternalTensor.Section4.sum_hom line 76
15. theorem OAI.ExternalTensor.Section4.sum_smul_component_apply line 81
16. theorem OAI.ExternalTensor.Section4.paths_relation line 94

    Source documentation

    The vertex-zero component vanishes by the actual quadratic relation in B.

    theorem paths_relation {A J : Type} [Fintype A] [Fintype J]
        (e₀ e₁ e₂ : B) (a : A → B) (b : J → B)
        (ha : ∀ i, a i * e₀ = a i) (hb : ∀ j, b j * e₁ = b j)
        (r : A → J → k) (hr : ∑ i, ∑ j, r i j • (b j * a i) = 0)
        (D : RightComplex B) :
        ∑ i, ∑ j, r i j • (path k B e₁ e₂ (b j) (hb j) D ≫
          path k B e₀ e₁ (a i) (ha i) D) = 0 := by
    …

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