OAI/Algebra/AuslanderReiten/Bar/ConcreteNativeBar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.T.simpleNativeBarIso line 19
2. theorem OAI.ArExplicit.T.three_isos_hom_f line 24
3. theorem OAI.ArExplicit.T.simpleNativeBarIso_hom line 31
4. theorem OAI.ArExplicit.T.simpleCoefficientNativeIso_hom line 37
5. theorem OAI.ArExplicit.T.simpleNativeBarIso_hom_f line 44

   Source documentation

   The degreewise map of the native comparison is the composite of its three factors.

   theorem simpleNativeBarIso_hom_f (n : ℕ) :
       (simpleNativeBarIso q).hom.f n =
         (simpleOrdinaryBarIso q).hom.f n ≫
           ((simpleCoefficientComplexIso q).hom.f n ≫
             (ExternalBalanced.nativeTotalBarIso k T₀ T₀ S S).hom.f n) := by
   …

   Mentions: OAI.ArExplicit.T.simpleNativeBarIso, OAI.ArExplicit.q, OAI.ArExplicit.T.simpleOrdinaryBarIso, OAI.ArExplicit.T.simpleCoefficientComplexIso, OAI.ArExplicit.ExternalBalanced.nativeTotalBarIso

6. def OAI.ArExplicit.T.simpleNativeFirst line 53
7. def OAI.ArExplicit.T.simpleNativeSecond line 58
8. theorem OAI.ArExplicit.T.compose_native_squares line 63
9. theorem OAI.ArExplicit.T.simpleCoefficientNative_first line 74
10. theorem OAI.ArExplicit.T.simpleCoefficientNative_second line 85
11. theorem OAI.ArExplicit.T.simpleNativeBarIso_first line 96
12. theorem OAI.ArExplicit.T.simpleNativeBarIso_second line 104