OAI/Algebra/Finitistic/Selected/SelectedChainHomology.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedChainHomology.representation line 13
2. abbrev OAI.LittleFinitistic.SelectedChainHomology.complex line 14
3. abbrev OAI.LittleFinitistic.SelectedChainHomology.source line 15
4. def OAI.LittleFinitistic.SelectedChainHomology.derivedIso line 17
5. def OAI.LittleFinitistic.SelectedChainHomology.comparison line 22
6. lemma OAI.LittleFinitistic.SelectedChainHomology.derived_map line 27
7. lemma OAI.LittleFinitistic.SelectedChainHomology.comparison_map line 44
8. def OAI.LittleFinitistic.SelectedChainHomology.modelIso line 61
9. lemma OAI.LittleFinitistic.SelectedChainHomology.model_action line 68
10. def OAI.LittleFinitistic.SelectedChainHomology.homologyIso line 76

    Source documentation

    Actual homology of a selected chain tensor, with its chosen target identification.

    def homologyIso (D : SourceVerdier.K P)
        (e : (source (Y := Y)).obj D ≅ target (Y := Y))
    …

    Mentions: OAI.LittleFinitistic.SourceVerdier.K, OAI.LittleFinitistic.SelectedChainHomology.source

11. lemma OAI.LittleFinitistic.SelectedChainHomology.homology_zero line 81
12. lemma OAI.LittleFinitistic.SelectedChainHomology.homology_arrow line 86
13. def OAI.LittleFinitistic.SelectedChainHomology.D0Iso line 108

    Source documentation

    All three actual tensors have the primary H(Y) as homology in both selected degrees.

    def D0Iso (n : ℤ) (hn : n = 0 ∨ n = -3) :
        (complex (Y := Y) fixed.D0).homology n ≅ H (Y := Y) :=
    …

    Mentions: OAI.LittleFinitistic.SelectedChainHomology.complex

14. def OAI.LittleFinitistic.SelectedChainHomology.D1Iso line 111
15. def OAI.LittleFinitistic.SelectedChainHomology.D2Iso line 114
16. lemma OAI.LittleFinitistic.SelectedChainHomology.D0_zero line 118
17. lemma OAI.LittleFinitistic.SelectedChainHomology.D1_zero line 121
18. lemma OAI.LittleFinitistic.SelectedChainHomology.D2_zero line 124
19. lemma OAI.LittleFinitistic.SelectedChainHomology.arrow01 line 129

    Source documentation

    This applies to any chain representative of the same fixed first arrow.

    lemma arrow01 (a : Fin (encoding.generators+1))
        (f : SelectedChainDiagram.D0 ⟶ SelectedChainDiagram.D1)
        (hf : (HomotopyCategory.quotient _ _).map f = (fixed.f a).hom)
        (n : ℤ) (hn : n = 0 ∨ n = -3) :
        HomologicalComplex.homologyMap (tensorMap (representation (Y := Y)) f) n ≫ (D1Iso n hn).hom =
    …

    Mentions: OAI.LittleFinitistic.SelectedChainDiagram.D0, OAI.LittleFinitistic.SelectedChainDiagram.D1, OAI.LittleFinitistic.SelectedChainHomology.representation, OAI.LittleFinitistic.SelectedChainHomology.D1Iso

20. lemma OAI.LittleFinitistic.SelectedChainHomology.arrow12 line 139
21. lemma OAI.LittleFinitistic.SelectedChainHomology.fixed_arrow01 line 149
22. lemma OAI.LittleFinitistic.SelectedChainHomology.fixed_arrow12 line 155