OAI/Algebra/AuslanderReiten/Ext/ExternalEvaluatedFreeValues.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.ExternalBalanced.postShuffle_native_values line 25

   Source comment

   Match the native chain maps' complex shape and scalar structures in the premises. Keep the summand presentation in the conclusion so composition does not need to compare expanded tensor-product structures after specializing the bar complexes.

   private theorem postShuffle_native_values
       (U : ModuleCat.{u} A) (V : ModuleCat.{u} B)
       (g : (factorEvaluation k U (AbsoluteBar.complex k A)).X 0 ⟶
         (ModuleBar.complex k A M).X (c := ComplexShape.down ℕ) 0)
   …

   Mentions: OAI.ArExplicit.A, OAI.ArExplicit.ExternalBalanced.factorEvaluation, OAI.ArExplicit.AbsoluteBar.complex, OAI.ArExplicit.ModuleBar.complex

2. theorem OAI.ArExplicit.ExternalBalanced.nativePostShuffle line 55
3. abbrev OAI.ArExplicit.ExternalBalanced.nativePureStart line 63
4. theorem OAI.ArExplicit.ExternalBalanced.nativePureLeft line 69
5. theorem OAI.ArExplicit.ExternalBalanced.nativePureProof line 75
6. theorem OAI.ArExplicit.ExternalBalanced.shuffledFreeEvaluation_pure line 81
7. abbrev OAI.ArExplicit.ExternalBalanced.summandFreeProof line 85
8. theorem OAI.ArExplicit.ExternalBalanced.summandFreeEvaluation_pure line 88
9. theorem OAI.ArExplicit.ExternalBalanced.valueOfComposite line 92
10. theorem OAI.ArExplicit.ExternalBalanced.totalFreeFromSummand line 98
11. abbrev OAI.ArExplicit.ExternalBalanced.barPureTensor line 102
12. theorem OAI.ArExplicit.ExternalBalanced.totalFreeAt line 111
13. theorem OAI.ArExplicit.ExternalBalanced.totalFreeProof line 116
14. theorem OAI.ArExplicit.ExternalBalanced.totalFreeEvaluation_pure line 122