OAI/Algebra/AuslanderReiten/Bar/BarBalancedCanonical.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.BarBalanced.canonicalEvaluated line 17
2. def OAI.ArExplicit.BarBalanced.canonicalObject line 20
3. def OAI.ArExplicit.BarBalanced.nativeObject line 23
4. def OAI.ArExplicit.BarBalanced.scalarEvaluatedObject line 26
5. def OAI.ArExplicit.BarBalanced.scalarEvaluatedElement line 35
6. theorem OAI.ArExplicit.BarBalanced.scalarEvaluatedObject_eq line 44
7. theorem OAI.ArExplicit.BarBalanced.scalarEvaluatedElement_transport line 54
8. theorem OAI.ArExplicit.BarBalanced.canonicalScalar_eq line 67
9. theorem OAI.ArExplicit.BarBalanced.canonicalObject_eq line 75
10. def OAI.ArExplicit.BarBalanced.canonicalTransport line 81
11. def OAI.ArExplicit.BarBalanced.nativeElement line 84
12. theorem OAI.ArExplicit.BarBalanced.canonicalTransport_tmul line 90
13. def OAI.ArExplicit.BarBalanced.canonicalEquiv line 98
14. theorem OAI.ArExplicit.BarBalanced.canonicalEquiv_tmul line 101
15. def OAI.ArExplicit.BarBalanced.canonicalMap line 109
16. theorem OAI.ArExplicit.BarBalanced.canonicalMap_tmul line 114
17. theorem OAI.ArExplicit.BarBalanced.canonicalEquiv_map line 122

    Source documentation

    Establish compatibility at arbitrary degrees so induction does not unfold the iterated tensor products in successor degrees.

    private theorem canonicalEquiv_map {m n : ℕ}
        (f : AbsoluteBar.moduleObject k R m ⟶ AbsoluteBar.moduleObject k R n)
        (g : ModuleBar.moduleObject k R X m →ₗ[R] ModuleBar.moduleObject k R X n)
        (h : ∀ (a : AbsoluteBar.moduleObject k R m) (x : X),
          rawEval k R X n (f a ⊗ₜ[k] x) = g (rawEval k R X m (a ⊗ₜ[k] x)))
        (z : canonicalEvaluated k R X m) :
        canonicalEquiv k R X n (canonicalMap k R X f z) =
          g (canonicalEquiv k R X m z) := by
    …

    Mentions: OAI.ArExplicit.AbsoluteBar.moduleObject, OAI.ArExplicit.ModuleBar.moduleObject, OAI.ArExplicit.BarBalanced.rawEval, OAI.ArExplicit.BarBalanced.canonicalEvaluated, OAI.ArExplicit.BarBalanced.canonicalEquiv, OAI.ArExplicit.BarBalanced.canonicalMap

18. theorem OAI.ArExplicit.BarBalanced.canonicalEquiv_differential line 137
19. abbrev OAI.ArExplicit.BarBalanced.cubicHom line 149

    Source documentation

    Naming this morphism keeps kernel checking from repeatedly expanding the iterated tensor-module structures at successor degrees.

    abbrev cubicHom (p : AbsoluteBar.Cochain3 k R) (n : ℕ) :
        AbsoluteBar.moduleObject k R (n+4) ⟶ AbsoluteBar.moduleObject k R (n+1) :=
    …

    Mentions: OAI.ArExplicit.AbsoluteBar.Cochain3, OAI.ArExplicit.AbsoluteBar.moduleObject

20. theorem OAI.ArExplicit.BarBalanced.rawEval_cubic_compatibility line 154
21. theorem OAI.ArExplicit.BarBalanced.canonicalEquiv_cubic line 160