OAI/AlgebraicTopology/IntegralHomology/Relative.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.integralSingularChains line 19

   Source documentation

   The same integral singular chains underlying integralSingularHomology.

   def integralSingularChains : TopCat.{0} ⥤ ChainComplex (ModuleCat.{0} ℤ) ℕ :=
   …

2. def OAI.Kaplansky.relativeSingularChains line 23

   Source documentation

   Relative chains are the actual cokernel of the subspace chain map.

   def relativeSingularChains {A X : TopCat.{0}} (i : A ⟶ X) :
       ChainComplex (ModuleCat.{0} ℤ) ℕ := cokernel (integralSingularChains.map i)

3. def OAI.Kaplansky.relativeChainProjection line 26
4. instance OAI.Kaplansky.(instance at line 30) line 30
5. def OAI.Kaplansky.relativeChainMap line 33
6. theorem OAI.Kaplansky.relativeChainProjection_map line 40
7. theorem OAI.Kaplansky.relativeChainMap_id line 46
8. theorem OAI.Kaplansky.relativeChainMap_comp line 51
9. def OAI.Kaplansky.relativeChainSequence line 61
10. theorem OAI.Kaplansky.relativeChainSequence_shortExact line 68

    Source documentation

    Injectivity of the actual inclusion supplies short exactness; it is not an assumed homological property of the pair.

    theorem relativeChainSequence_shortExact {A X : TopCat.{0}} (i : A ⟶ X)
        [Mono i] : (relativeChainSequence i).ShortExact := by
    …

    Mentions: OAI.Kaplansky.relativeChainSequence

11. def OAI.Kaplansky.subspaceInclusion line 78

    Source documentation

    Inclusion of an arbitrary subspace with its inherited topology.

    def subspaceInclusion {X : Type} [TopologicalSpace X] (U : Set X) :
        TopCat.of U ⟶ TopCat.of X := TopCat.ofHom ⟨Subtype.val, continuous_subtype_val⟩

12. instance OAI.Kaplansky.(instance at line 81) line 81
13. def OAI.Kaplansky.relativeSingularHomology line 89
14. def OAI.Kaplansky.absoluteToRelative line 92
15. def OAI.Kaplansky.relativeHomologyMap line 96
16. theorem OAI.Kaplansky.absoluteToRelative_naturality line 102
17. theorem OAI.Kaplansky.relativeHomologyMap_id line 112
18. theorem OAI.Kaplansky.relativeHomologyMap_comp line 116
19. def OAI.Kaplansky.relativeHomologyBoundary line 129

    Source documentation

    The boundary homomorphism of an actual injective topological map.

    def relativeHomologyBoundary {A X : TopCat.{0}} (i : A ⟶ X) [Mono i] (n : ℕ) :
        relativeSingularHomology i (n+1) ⟶ (integralSingularHomology n).obj A :=
    …

    Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.integralSingularHomology

20. theorem OAI.Kaplansky.absoluteToRelative_boundary line 133
21. theorem OAI.Kaplansky.relativeHomologyBoundary_inclusion line 137
22. theorem OAI.Kaplansky.inclusion_absoluteToRelative line 141
23. theorem OAI.Kaplansky.relativeHomology_exact_at_absolute line 153

    Source documentation

    All three positions in the relative singular homology long exact sequence.

    theorem relativeHomology_exact_at_absolute {A X : TopCat.{0}} (i : A ⟶ X) [Mono i]
        (n : ℕ) : (ShortComplex.mk _ _ (inclusion_absoluteToRelative i n)).Exact :=
    …

    Mentions: OAI.Kaplansky.inclusion_absoluteToRelative

24. theorem OAI.Kaplansky.relativeHomology_exact_at_relative line 157
25. theorem OAI.Kaplansky.relativeHomology_exact_at_subspace line 161
26. def OAI.Kaplansky.relativeChainSequenceMap line 165
27. theorem OAI.Kaplansky.relativeHomologyBoundary_naturality line 177
28. def OAI.Kaplansky.subspaceMap line 191

    Source documentation

    Restriction of a continuous map that really carries one subspace into another.

    def subspaceMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
        (U : Set X) (V : Set Y) (f : C(X,Y)) (h : Set.MapsTo f U V) :
        TopCat.of U ⟶ TopCat.of V :=
    …

29. theorem OAI.Kaplansky.subspaceMap_square line 197
30. def OAI.Kaplansky.compactifiedNonzeroBundle line 205

    Source documentation

    Complement of the actual zero section in the one-point total space. It includes infinity; it is not just the punctured total space.

    def compactifiedNonzeroBundle : Set (OnePoint (TotalSpace V E)) :=
    …

31. theorem OAI.Kaplansky.coe_mem_compactifiedNonzeroBundle line 208
32. theorem OAI.Kaplansky.infty_mem_compactifiedNonzeroBundle line 222
33. def OAI.Kaplansky.sectionNonzeroLocus line 228

    Source documentation

    Nonvanishing locus of this section, with the actual base topology.

    def sectionNonzeroLocus (s : ∀ b, E b) : Set B := {b | s b ≠ 0}
    …

34. theorem OAI.Kaplansky.compactifiedSection_mapsTo_nonzero line 232
35. def OAI.Kaplansky.sectionRelativeHomologyMap line 240

    Source documentation

    The actual map of pairs (B, B minus zeros) to (Thom, Thom minus zero section).

    def sectionRelativeHomologyMap (s : ∀ b, E b)
        (hs : Continuous (fun b => TotalSpace.mk' V b (s b))) (n : ℕ) :
        relativeSingularHomology (subspaceInclusion (sectionNonzeroLocus s)) n ⟶
          relativeSingularHomology
            (subspaceInclusion (compactifiedNonzeroBundle (V := V) (E := E))) n :=
    …

    Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.sectionNonzeroLocus, OAI.Kaplansky.compactifiedNonzeroBundle

36. theorem OAI.Kaplansky.sectionRelativeHomology_comparison line 251

    Source documentation

    Exact comparison with the preserved absolute section map. No local degree, excision, or fundamental-class premise is used in this square.

    theorem sectionRelativeHomology_comparison (s : ∀ b, E b)
        (hs : Continuous (fun b => TotalSpace.mk' V b (s b))) (n : ℕ) :
        absoluteToRelative (subspaceInclusion (sectionNonzeroLocus s)) n ≫
            sectionRelativeHomologyMap s hs n =
          sectionHomologyMap s hs n ≫
            absoluteToRelative (subspaceInclusion (compactifiedNonzeroBundle (V := V) (E := E))) n :=
    …

    Mentions: OAI.Kaplansky.absoluteToRelative, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.sectionNonzeroLocus, OAI.Kaplansky.sectionRelativeHomologyMap, OAI.Kaplansky.sectionHomologyMap, OAI.Kaplansky.compactifiedNonzeroBundle

37. theorem OAI.Kaplansky.relativeClass_lifts_iff line 261

    Source documentation

    A class annihilated by the relative boundary lifts to absolute homology. This is a consequence of the proved long exact sequence, not a lifting axiom.

    theorem relativeClass_lifts_iff {A X : TopCat.{0}} (i : A ⟶ X) [Mono i] (n : ℕ)
        (c : relativeSingularHomology i (n+1)) :
        relativeHomologyBoundary i n c = 0 ↔
          ∃ b : (integralSingularHomology (n+1)).obj X, absoluteToRelative i (n+1) b = c := by
    …

    Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.relativeHomologyBoundary, OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.absoluteToRelative

38. theorem OAI.Kaplansky.sectionHomologyMap_ne_zero_of_relativeClass line 272

    Source documentation

    A precise witness criterion for a nonzero global section map. This does not construct the required local class or compute its image.

    theorem sectionHomologyMap_ne_zero_of_relativeClass (s : ∀ b, E b)
        (hs : Continuous (fun b => TotalSpace.mk' V b (s b))) (n : ℕ)
        (c : relativeSingularHomology (subspaceInclusion (sectionNonzeroLocus s)) (n+1))
        (hc : relativeHomologyBoundary (subspaceInclusion (sectionNonzeroLocus s)) n c = 0)
        (hne : sectionRelativeHomologyMap s hs (n+1) c ≠ 0) :
        sectionHomologyMap s hs (n+1) ≠ 0 := by
    …

    Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.sectionNonzeroLocus, OAI.Kaplansky.relativeHomologyBoundary, OAI.Kaplansky.sectionRelativeHomologyMap, OAI.Kaplansky.sectionHomologyMap