structure EilenbergSteenrod.TopPair : Type (u + 1)

A pair of topological spaces (X, A): a space X (the carrier space with topology instTop) together with a subset A ⊆ X (called sub). Pairs of spaces are the objects of the category Top₂ on which a homology theory is defined.

• space : Type u
• instTop : TopologicalSpace self.space
• sub : Set self.space

def EilenbergSteenrod.TopPair.ofSpace (X : Type u) [TopologicalSpace X] : TopPair

The pair (X, ∅) associated with a topological space X, viewing an absolute space as a relative one with empty subspace.

def EilenbergSteenrod.TopPair.subPair (P : TopPair) : TopPair

The pair (A, ∅) obtained by regarding the subspace A of a pair P = (X, A) as a standalone space. This is used to express the boundary map Hₙ(X, A) → Hₙ₋₁(A).

def EilenbergSteenrod.TopPair.point : TopPair

The one-point pair (*, ∅), used as the test object for the dimension axiom of a homology theory.

def EilenbergSteenrod.TopPair.excisePair (P : TopPair) (U : Set P.space) : TopPair

Given a pair P = (X, A) and a subset U ⊆ X, the excised pair (X − U, A − U). This is the source of the excision inclusion (X − U, A − U) ↪ (X, A).

def EilenbergSteenrod.TopPair.coproduct (ι : Type u) (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : TopPair

The pair (∐ᵢ Xᵢ, ∅) formed by the disjoint union of a family of spaces, used to state the Milnor (coproduct) axiom of a homology theory.

structure EilenbergSteenrod.MapOfPairs (P : TopPair) (Q : TopPair) : Type (max u_1 u_2)

A morphism of pairs (X, A) → (Y, B): a continuous map f : X → Y such that f(A) ⊆ B. These are the morphisms in the category of pairs.

• toFun : P.space → Q.space
• continuous_toFun : Continuous self.toFun
• mapsTo : Set.MapsTo self.toFun P.sub Q.sub

def EilenbergSteenrod.MapOfPairs.id (P : TopPair) : MapOfPairs P P

The identity morphism on a pair (X, A).

def EilenbergSteenrod.MapOfPairs.comp {P : TopPair} {Q : TopPair} {R : TopPair} (g : MapOfPairs Q R) (f : MapOfPairs P Q) : MapOfPairs P R

Composition of morphisms of pairs.

def EilenbergSteenrod.MapOfPairs.restrictToSub {P : TopPair} {Q : TopPair} (f : MapOfPairs P Q) : MapOfPairs P.subPair Q.subPair

The restriction of a map of pairs f : (X, A) → (Y, B) to the subspaces, producing f|_A : (A, ∅) → (B, ∅). Used to express naturality of the boundary map.

def EilenbergSteenrod.inclusionSubToSpace (P : TopPair) : MapOfPairs P.subPair (TopPair.ofSpace P.space)

The inclusion of pairs (A, ∅) ↪ (X, ∅) arising from the subspace inclusion A ⊆ X. This is the map i in the relative homology long exact sequence.

def EilenbergSteenrod.inclusionSpaceToPair (P : TopPair) : MapOfPairs (TopPair.ofSpace P.space) P

The map of pairs (X, ∅) → (X, A) given by the identity on X. This is the quotient-type map j in the relative long exact sequence.

def EilenbergSteenrod.excisionInclusion (P : TopPair) (U : Set P.space) : MapOfPairs (P.excisePair U) P

The excision inclusion of pairs (X − U, A − U) ↪ (X, A). The excision axiom asserts this map induces an isomorphism in homology whenever the triple (X, A, U) is excisive.

def EilenbergSteenrod.coproductInclusion (ι : Type u) (X : ι → Type u) [(j : ι) → TopologicalSpace (X j)] (i : ι) : MapOfPairs (TopPair.ofSpace (X i)) (TopPair.coproduct ι X)

The inclusion of the i-th summand Xᵢ ↪ ∐ⱼ Xⱼ of a coproduct of spaces, as a map of pairs. These maps assemble into the Milnor (coproduct) axiom isomorphism.

structure EilenbergSteenrod.HomotopyOfPairMaps {P : TopPair} {Q : TopPair} (f₀ f₁ : MapOfPairs P Q) : Type (max u_1 u_2)

A homotopy of pair maps f₀, f₁ : (X, A) → (Y, B): a continuous map h : X × I → Y interpolating from f₀ to f₁ such that h(A × I) ⊆ B at every time.

• toFun : P.space × ↑unitInterval → Q.space
• continuous_toFun : Continuous self.toFun
• map_zero (x : P.space) : self.toFun (x, ⟨0, unitInterval.zero_mem⟩) = f₀.toFun x
• map_one (x : P.space) : self.toFun (x, ⟨1, unitInterval.one_mem⟩) = f₁.toFun x
• mapsTo (a : P.space) : a ∈ P.sub → ∀ (t : ↑unitInterval), self.toFun (a, t) ∈ Q.sub

def EilenbergSteenrod.AreHomotopic {P : TopPair} {Q : TopPair} (f₀ f₁ : MapOfPairs P Q) : Prop

Two maps of pairs are homotopic if there exists a homotopy of pair maps between them.

structure EilenbergSteenrod.IsExcisiveTriple (P : TopPair) (U : Set P.space) : Prop

A triple (X, A, U) with U ⊆ A ⊆ X is excisive if the closure of U lies inside the interior of A (Definition 10.1). For such a triple, the excision inclusion (X − U, A − U) ↪ (X, A) is required to be a homology isomorphism.

• sub_mem : U ⊆ P.sub
• closure_sub_interior : closure U ⊆ interior P.sub

structure EilenbergSteenrod.HomologyTheory : Type (u + 1)

Definition 11.1 (Eilenberg–Steenrod axioms). A homology theory on Top consists of a sequence of functors Hₙ : Top₂ → Ab (n ∈ ℤ) together with natural boundary maps ∂ : Hₙ(X, A) → Hₙ₋₁(A, ∅) satisfying:

1. Homotopy invariance — homotopic maps of pairs induce equal maps on Hₙ.
2. Excision — excisive inclusions induce isomorphisms in homology.
3. Long exact sequence — for every pair (X, A) the sequence ⋯ → Hₙ(A) → Hₙ(X) → Hₙ(X, A) → Hₙ₋₁(A) → ⋯ is exact.
4. Dimension axiom — Hₙ(pt) vanishes for n ≠ 0.
5. Milnor (additivity) axiom — for any disjoint union ∐ᵢ Xᵢ, the canonical map ⨁ᵢ Hₙ(Xᵢ) → Hₙ(∐ᵢ Xᵢ) is an isomorphism.

• H : ℤ → TopPair → Type u
• instAddCommGroup (n : ℤ) (P : TopPair) : AddCommGroup (self.H n P)
• map (n : ℤ) {P Q : TopPair} : MapOfPairs P Q → self.H n P →+ self.H n Q
• map_id (n : ℤ) (P : TopPair) : self.map n (MapOfPairs.id P) = AddMonoidHom.id (self.H n P)
• map_comp (n : ℤ) {P Q R : TopPair} (f : MapOfPairs P Q) (g : MapOfPairs Q R) : self.map n (g.comp f) = (self.map n g).comp (self.map n f)
• boundary (n : ℤ) (P : TopPair) : self.H (n + 1) P →+ self.H n P.subPair
• boundary_natural (n : ℤ) {P Q : TopPair} (f : MapOfPairs P Q) : (self.map n f.restrictToSub).comp (self.boundary n P) = (self.boundary n Q).comp (self.map (n + 1) f)
• homotopy_invariance (n : ℤ) {P Q : TopPair} (f₀ f₁ : MapOfPairs P Q) : AreHomotopic f₀ f₁ → self.map n f₀ = self.map n f₁
• excision (n : ℤ) (P : TopPair) (U : Set P.space) : IsExcisiveTriple P U → Function.Bijective ⇑(self.map n (excisionInclusion P U))
• exact_at_sub (n : ℤ) (P : TopPair) : Function.Exact ⇑(self.boundary n P) ⇑(self.map n (inclusionSubToSpace P))
• exact_at_space (n : ℤ) (P : TopPair) : Function.Exact ⇑(self.map n (inclusionSubToSpace P)) ⇑(self.map n (inclusionSpaceToPair P))
• exact_at_pair (n : ℤ) (P : TopPair) : Function.Exact ⇑(self.map (n + 1) (inclusionSpaceToPair P)) ⇑(self.boundary n P)
• dimension (n : ℤ) : n ≠ 0 → Subsingleton (self.H n TopPair.point)
• coproduct (n : ℤ) {ι : Type u} [DecidableEq ι] (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : Function.Bijective ⇑(DirectSum.toAddMonoid fun (i : ι) => self.map n (coproductInclusion ι X i))

def IsCover {X : Type u_1} [TopologicalSpace X] (𝒜 : Set (Set X)) : Prop

Definition 11.2 (Cover). A family 𝒜 of subsets of a topological space X is a cover if the union of the interiors of its members equals all of X.

theorem isCover_iff {X : Type u_1} [TopologicalSpace X] (𝒜 : Set (Set X)) : IsCover 𝒜 ↔ ∀ (x : X), ∃ A ∈ 𝒜, x ∈ interior A

Pointwise reformulation of IsCover: a family 𝒜 covers X iff every point of X lies in the interior of some member of 𝒜.

def AlgebraicTopologyI.IsSmall {X : Type u_1} [TopologicalSpace X] {n : ℕ} (𝒜 : Set (Set X)) (σ : SingularSimplex n X) : Prop

Definition 11.3 (𝒜-small simplex). Given a cover 𝒜 of X, a singular n-simplex σ : Δⁿ → X is 𝒜-small if its image lies entirely in some A ∈ 𝒜.

theorem MayerVietoris.exact_at_prod {A : Type u_2} {B : Type u_3} {C : Type u_4} {A' : Type u_5} {B' : Type u_6} {C' : Type u_7} {Bprev : Type u_8} {Bprev' : Type u_9} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [AddCommGroup A'] [AddCommGroup B'] [AddCommGroup C'] [AddCommGroup Bprev] [AddCommGroup Bprev'] (k : C →+ A) (j : A →+ B) (k' : C' →+ A') (j' : A' →+ B') (h : C' →+ C) (f : A' →+ A) (g : B' ≃+ B) (dprev : Bprev →+ C) (d'prev : Bprev' →+ C') (gprev : Bprev' ≃+ Bprev) (exact_A_top : Function.Exact ⇑k ⇑j) (exact_A'_bot : Function.Exact ⇑k' ⇑j') (exact_C_top : Function.Exact ⇑dprev ⇑k) (exact_C'_bot : Function.Exact ⇑d'prev ⇑k') (comm1 : ∀ (x : C'), k (h x) = f (k' x)) (comm2 : ∀ (x : A'), j (f x) = g (j' x)) (comm_prev : ∀ (x : Bprev'), dprev (gprev x) = h (d'prev x)) : Function.Exact (fun (x : C') => (h x, -k' x)) fun (p : C × A') => k p.1 + f p.2

Exactness at the middle term C × A' in the Mayer–Vietoris–style sequence of Lemma 11.6. Given two horizontal exact sequences related by a ladder of vertical maps with the indicated commutation properties, the composite c' ↦ (h c', −k' c') followed by (c, a') ↦ k c + f a' is exact at C × A'.

theorem MayerVietoris.exact_at_A {A : Type u_2} {B : Type u_3} {C : Type u_4} {A' : Type u_5} {B' : Type u_6} {C₂' : Type u_7} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [AddCommGroup A'] [AddCommGroup B'] [AddCommGroup C₂'] (k : C →+ A) (j : A →+ B) (j' : A' →+ B') (d' : B' →+ C₂') (f : A' →+ A) (g : B' ≃+ B) (exact_A_top : Function.Exact ⇑k ⇑j) (exact_B'_bot : Function.Exact ⇑j' ⇑d') (comm2 : ∀ (x : A'), j (f x) = g (j' x)) : Function.Exact (fun (p : C × A') => k p.1 + f p.2) fun (a : A) => d' (g.symm (j a))

Exactness at the term A of the Mayer–Vietoris–style sequence: the composite (c, a') ↦ k c + f a' followed by the connecting map a ↦ d'(g⁻¹(j a)) is exact at A.

theorem MayerVietoris.exact_at_C' {A : Type u_2} {B : Type u_3} {C : Type u_4} {A' : Type u_5} {B' : Type u_6} {C' : Type u_7} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [AddCommGroup A'] [AddCommGroup B'] [AddCommGroup C'] (j : A →+ B) (dtop : B →+ C) (k' : C' →+ A') (d' : B' →+ C') (h : C' →+ C) (g : B' ≃+ B) (exact_B_top : Function.Exact ⇑j ⇑dtop) (exact_C'_bot : Function.Exact ⇑d' ⇑k') (comm3 : ∀ (x : B'), dtop (g x) = h (d' x)) : Function.Exact (fun (a : A) => d' (g.symm (j a))) fun (x : C') => (h x, -k' x)

Exactness at the term C' of the Mayer–Vietoris–style sequence: the connecting map a ↦ d'(g⁻¹(j a)) followed by c' ↦ (h c', −k' c') is exact at C'.

theorem MayerVietoris.exact_sequence {Aprev : Type u_2} {Bprev : Type u_3} {Bprev' : Type u_4} {C : Type u_5} {C' : Type u_6} {A : Type u_7} {A' : Type u_8} {B : Type u_9} {B' : Type u_10} {Cnext' : Type u_11} [AddCommGroup Aprev] [AddCommGroup Bprev] [AddCommGroup Bprev'] [AddCommGroup C] [AddCommGroup C'] [AddCommGroup A] [AddCommGroup A'] [AddCommGroup B] [AddCommGroup B'] [AddCommGroup Cnext'] (jprev : Aprev →+ Bprev) (dprev : Bprev →+ C) (k : C →+ A) (j : A →+ B) (d'prev : Bprev' →+ C') (k' : C' →+ A') (j' : A' →+ B') (d'next : B' →+ Cnext') (gprev : Bprev' ≃+ Bprev) (h : C' →+ C) (f : A' →+ A) (g : B' ≃+ B) (exact_jprev_dprev : Function.Exact ⇑jprev ⇑dprev) (exact_dprev_k : Function.Exact ⇑dprev ⇑k) (exact_k_j : Function.Exact ⇑k ⇑j) (exact_d'prev_k' : Function.Exact ⇑d'prev ⇑k') (exact_k'_j' : Function.Exact ⇑k' ⇑j') (exact_j'_d'next : Function.Exact ⇑j' ⇑d'next) (comm_kh : ∀ (x : C'), k (h x) = f (k' x)) (comm_jf : ∀ (x : A'), j (f x) = g (j' x)) (comm_dg : ∀ (x : Bprev'), dprev (gprev x) = h (d'prev x)) : (Function.Exact (fun (x : C') => (h x, -k' x)) fun (p : C × A') => k p.1 + f p.2) ∧ (Function.Exact (fun (p : C × A') => k p.1 + f p.2) fun (a : A) => d'next (g.symm (j a))) ∧ Function.Exact (fun (a : Aprev) => d'prev (gprev.symm (jprev a))) fun (x : C') => (h x, -k' x)

Lemma 11.6 (Mayer–Vietoris assembly). Given two horizontal exact sequences linked by a ladder of vertical maps satisfying the stated commutativity, the sequence ⋯ → C'ₙ₊₁ → Cₙ₊₁ ⊕ A'ₙ → Aₙ → C'ₙ → ⋯, with morphisms c' ↦ (h c', −k' c'), (c, a') ↦ k c + f a', and the connecting map a ↦ d'(g⁻¹(j a)), is exact at each of C × A', A, and C'. This is the algebraic core of the Mayer–Vietoris theorem (Theorem 11.5).