def ExactSequence.isComplex {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (f : A →+ B) (g : B →+ C) : Prop

A pair of consecutive group homomorphisms f, g forms a complex when g ∘ f = 0, i.e. the image of f is contained in the kernel of g. This is the "complex" half of Definition 8.1's notion of an exact sequence: a sequence whose composites all vanish.

@[reducible, inline]

abbrev ExactSequence.exactAt {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (f : A →+ B) (g : B →+ C) : Prop

Exactness at the middle term of A →+ B →+ C: the image of f equals the kernel of g. This formalizes the equality im f = ker g from Definition 8.1 by reusing Mathlib's Function.Exact.

structure ExactSequence.IsShortExact {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (i : A →+ B) (p : B →+ C) : Prop

A short exact sequence 0 → A → B → C → 0 of abelian groups, packaged as the injectivity of i, the surjectivity of p, and exactness at the middle term B. This realizes Definition 8.3.

• injective : Function.Injective ⇑i
• surjective : Function.Surjective ⇑p
• exact : Function.Exact ⇑i ⇑p

structure ExactSequence.IntChainComplex : Type (u_4 + 1)

A chain complex indexed by the integers: a sequence of abelian groups X n together with differentials d : X n →+ X (n - 1) satisfying d ∘ d = 0. This is the structure underlying Definition 1.6, used here as the ambient setting for relative chain complexes.

• X : ℤ → Type u_4
• instAddCommGroup (n : ℤ) : AddCommGroup (self.X n)
• d (n : ℤ) : self.X n →+ self.X (n - 1)
• d_comp_d (n : ℤ) : (self.d (n - 1)).comp (self.d n) = 0

structure ExactSequence.IntChainComplex.Subcomplex (B : IntChainComplex) : Type u_4

A subcomplex of an integer-indexed chain complex B: a choice of subgroup in each degree that is closed under the differential d. This is the input data for forming the quotient chain complex in Lemma 8.4.

• toSubgroup (n : ℤ) : AddSubgroup (B.X n)
• d_maps (n : ℤ) (x : B.X n) : x ∈ self.toSubgroup n → (B.d n) x ∈ self.toSubgroup (n - 1)

structure ExactSequence.IntChainMap (B : IntChainComplex) (C : IntChainComplex) : Type (max u_4 u_5)

A chain map between integer-indexed chain complexes: a family of group homomorphisms commuting with the differentials in each degree.

• f (n : ℤ) : B.X n →+ C.X n
• comm (n : ℤ) : (C.d n).comp (self.f n) = (self.f (n - 1)).comp (B.d n)

noncomputable def ExactSequence.IntChainComplex.Subcomplex.quotientD (B : IntChainComplex) (A : B.Subcomplex) (n : ℤ) : B.X n ⧸ A.toSubgroup n →+ B.X (n - 1) ⧸ A.toSubgroup (n - 1)

The induced differential on the quotient B.X n / A.toSubgroup n, obtained by descending d : B.X n →+ B.X (n - 1) through the projection. This realizes the existence half of Lemma 8.4 in the integer-indexed setting.

theorem ExactSequence.IntChainComplex.Subcomplex.quotientD_comp_quotientD (B : IntChainComplex) (A : B.Subcomplex) (n : ℤ) : (quotientD B A (n - 1)).comp (quotientD B A n) = 0

The induced differential on the quotient squares to zero, so the quotient really forms a chain complex (the d ∘ d = 0 half of Lemma 8.4).

noncomputable def ExactSequence.IntChainComplex.Subcomplex.quotientComplex (B : IntChainComplex) (A : B.Subcomplex) : IntChainComplex

The quotient chain complex B / A of an integer-indexed chain complex by a subcomplex: in degree n the group is B.X n / A.toSubgroup n, with the induced differential. This packages the conclusion of Lemma 8.4.

theorem ExactSequence.IntChainComplex.Subcomplex.quotientComplex_unique (B : IntChainComplex) (A : B.Subcomplex) (d' : (n : ℤ) → B.X n ⧸ A.toSubgroup n →+ B.X (n - 1) ⧸ A.toSubgroup (n - 1)) (hcomm : ∀ (n : ℤ), (d' n).comp (QuotientAddGroup.mk' (A.toSubgroup n)) = (QuotientAddGroup.mk' (A.toSubgroup (n - 1))).comp (B.d n)) (n : ℤ) : d' n = quotientD B A n

Uniqueness of the quotient differential: any family d' on the quotient groups that makes the projection B → B / A into a chain map agrees with quotientD. This is the uniqueness assertion of Lemma 8.4.

def ExactSequence.IntChainComplex.castHom (C : IntChainComplex) {m n : ℤ} (h : m = n) : C.X m →+ C.X n

Transport a chain group along an equality of indices, packaged as a group homomorphism C.X m →+ C.X n when m = n. Used to bridge mismatched indices when defining the homology groups.

theorem ExactSequence.IntChainComplex.d_castHom (C : IntChainComplex) {m n : ℤ} (h : m = n) (z : C.X m) : (C.d n) ((C.castHom h) z) = (C.castHom ⋯) ((C.d m) z)

Compatibility of the differential with the cast homomorphism: applying d after casting is the same as casting after applying d.

def ExactSequence.IntChainComplex.d' (C : IntChainComplex) (n : ℤ) : C.X (n + 1) →+ C.X n

A reindexed differential d' : C.X (n + 1) →+ C.X n obtained from d by casting the target along n + 1 - 1 = n. Convenient for stating cycles/boundaries without subtraction in the index.

def ExactSequence.IntChainComplex.cycles (C : IntChainComplex) (n : ℤ) : AddSubgroup (C.X n)

The group of n-cycles Z_n(C) = ker(d : C.X n →+ C.X (n - 1)). Generalizes Definition 1.4 to an abstract integer-indexed chain complex.

def ExactSequence.IntChainComplex.boundaries (C : IntChainComplex) (n : ℤ) : AddSubgroup (C.X n)

The group of n-boundaries B_n(C) = im(d : C.X (n + 1) →+ C.X n). Generalizes the boundary subgroup from Definition 1.7 to an abstract integer-indexed chain complex.

noncomputable def ExactSequence.IntChainComplex.homologyGroup (C : IntChainComplex) (n : ℤ) : Type u_4

The nth homology group H_n(C) = Z_n(C) / B_n(C) of an integer-indexed chain complex, as in Definition 1.7.

@[implicit_reducible]

noncomputable instance ExactSequence.IntChainComplex.instAddCommGroupHomology (C : IntChainComplex) (n : ℤ) : AddCommGroup (C.homologyGroup n)

The homology group inherits an abelian group structure from the quotient construction.

noncomputable def ExactSequence.RelativeHomology (n : ℤ) (B : IntChainComplex) (A : B.Subcomplex) : Type u_4

The nth relative homology of a chain complex B modulo a subcomplex A, defined as the homology of the quotient complex B / A. This is the abstract algebraic version of the relative homology of Definition 8.6.

def AlgebraicTopologyI.singularSimplexInclusion (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : SingularSimplex n ↑A → SingularSimplex n X

Push a singular n-simplex of the subspace A ⊆ X forward along the inclusion A ↪ X to obtain a singular n-simplex of X.

def AlgebraicTopologyI.singularChainsInclusion (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : SingularChains n ↑A →+ SingularChains n X

The inclusion of singular chain groups S_n(A) →+ S_n(X) induced by the inclusion A ↪ X, obtained by freely extending singularSimplexInclusion.

def AlgebraicTopologyI.RelativeSingularChains (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : Type u_1

The relative singular n-chains S_n(X, A) = S_n(X) / S_n(A), defined by quotienting the singular chains of X by the image of the inclusion from the singular chains of A. This is the underlying group of Definition 8.5 in a single degree.

@[implicit_reducible]

instance AlgebraicTopologyI.RelativeSingularChains.instAddCommGroup (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : AddCommGroup (RelativeSingularChains n X A)

The relative chain group S_n(X, A) inherits an abelian group structure from the quotient.

theorem AlgebraicTopologyI.SingularSimplex.map_face {n : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (i : Fin (n + 2)) (σ : SingularSimplex (n + 1) X) : face i (map f σ) = map f (face i σ)

Taking the ith face commutes with pushforward along a continuous map: the ith face of f ∘ σ equals f composed with the ith face of σ.

theorem AlgebraicTopologyI.SingularChains.map_comp_boundaryMap {n : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : (boundaryMap n Y).comp (map f) = (map f).comp (boundaryMap n X)

Naturality of the singular boundary map: pushforward along a continuous map commutes with the boundary, i.e. f_* ∘ d = d ∘ f_*.

theorem AlgebraicTopologyI.boundaryMap_comp_boundaryMap (n : ℕ) (X : Type u_1) [TopologicalSpace X] : (boundaryMap n X).comp (boundaryMap (n + 1) X) = 0

The singular boundary squares to zero, d ∘ d = 0, so the singular chains form a genuine chain complex. This is Theorem 1.5 applied to the singular complex.

theorem AlgebraicTopologyI.singularChainsInclusion_comm_boundary (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : (boundaryMap n X).comp (singularChainsInclusion (n + 1) X A) = (singularChainsInclusion n X A).comp (boundaryMap n ↑A)

The inclusion S_*(A) →+ S_*(X) commutes with the boundary maps, exhibiting S_*(A) as a subcomplex of S_*(X). This is the input needed to form S_*(X, A).

structure AlgebraicTopologyI.NatChainComplex : Type (u_1 + 1)

A non-negatively graded chain complex: a sequence of abelian groups X n for n : ℕ together with differentials d : X (n + 1) →+ X n satisfying d ∘ d = 0. This is the form most naturally suited to the singular chain complex.

• X : ℕ → Type u_1
• instAddCommGroup (n : ℕ) : AddCommGroup (self.X n)
• d (n : ℕ) : self.X (n + 1) →+ self.X n
• d_comp_d (n : ℕ) : (self.d n).comp (self.d (n + 1)) = 0

noncomputable def AlgebraicTopologyI.singularChainNatComplex (X : Type u_1) [TopologicalSpace X] : NatChainComplex

The singular chain complex S_*(X) of a topological space X, packaged as a NatChainComplex: in degree n the group is SingularChains n X, with differential the singular boundary map.

structure AlgebraicTopologyI.NatChainComplex.Subcomplex (B : NatChainComplex) : Type u_1

A subcomplex of a naturally indexed chain complex B: a subgroup in each degree that is preserved by the differential. This will be used to package S_*(A) ⊆ S_*(X).

• toSubgroup (n : ℕ) : AddSubgroup (B.X n)
• d_maps (n : ℕ) (x : B.X (n + 1)) : x ∈ self.toSubgroup (n + 1) → (B.d n) x ∈ self.toSubgroup n

noncomputable def AlgebraicTopologyI.NatChainComplex.Subcomplex.quotientD (B : NatChainComplex) (A : B.Subcomplex) (n : ℕ) : B.X (n + 1) ⧸ A.toSubgroup (n + 1) →+ B.X n ⧸ A.toSubgroup n

The induced differential on B.X (n + 1) / A.toSubgroup (n + 1) →+ B.X n / A.toSubgroup n, defined by descending B.d n through the projection. This is the naturally indexed analogue of IntChainComplex.Subcomplex.quotientD and the heart of Lemma 8.4.

theorem AlgebraicTopologyI.NatChainComplex.Subcomplex.quotientD_comp_quotientD (B : NatChainComplex) (A : B.Subcomplex) (n : ℕ) : (quotientD B A n).comp (quotientD B A (n + 1)) = 0

The induced differential on the quotient squares to zero (d ∘ d = 0), so the quotient really forms a chain complex.

noncomputable def AlgebraicTopologyI.NatChainComplex.Subcomplex.quotientComplex (B : NatChainComplex) (A : B.Subcomplex) : NatChainComplex

The quotient chain complex B / A of a naturally indexed chain complex by a subcomplex: degree n is B.X n / A.toSubgroup n, with the induced differential. This realizes Lemma 8.4 in the ℕ-graded setting.

noncomputable def AlgebraicTopologyI.singularSubcomplex (X : Type u_1) [TopologicalSpace X] (A : Set X) : (singularChainNatComplex X).Subcomplex

The singular chains of a subspace A ⊆ X form a subcomplex of S_*(X): the image of S_*(A) →+ S_*(X) is preserved by the boundary map.

noncomputable def AlgebraicTopologyI.relativeSingularChainComplex (X : Type u_1) [TopologicalSpace X] (A : Set X) : NatChainComplex

The relative singular chain complex S_*(X, A) = S_*(X) / S_*(A) of a pair (X, A), as a NatChainComplex. This is the chain complex of Definition 8.5.

noncomputable def AlgebraicTopologyI.relativeBoundaryMap (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : RelativeSingularChains (n + 1) X A →+ RelativeSingularChains n X A

The relative boundary map S_{n+1}(X, A) →+ S_n(X, A), defined directly by descending the singular boundary through the quotient by S_*(A).

@[simp]

theorem AlgebraicTopologyI.relativeBoundaryMap_mk (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) (c : SingularChains (n + 1) X) : (relativeBoundaryMap n X A) ↑c = ↑((boundaryMap n X) c)

The relative boundary of the class [c] ∈ S_{n+1}(X, A) is the class of the ordinary singular boundary dc ∈ S_n(X).

def AlgebraicTopologyI.NatChainComplex.cycles (C : NatChainComplex) (n : ℕ) : AddSubgroup (C.X n)

The group of n-cycles Z_n(C) of a naturally indexed chain complex. In degree 0 everything is a cycle (since S_{-1} is zero); in positive degrees it is the kernel of the differential. Compare Definition 1.4.

def AlgebraicTopologyI.NatChainComplex.boundaries (C : NatChainComplex) (n : ℕ) : AddSubgroup (C.X n)

The group of n-boundaries B_n(C) = im(d : C.X (n + 1) →+ C.X n) of a naturally indexed chain complex.

noncomputable def AlgebraicTopologyI.NatChainComplex.homologyGroup (C : NatChainComplex) (n : ℕ) : Type u_1

The nth homology group H_n(C) = Z_n(C) / B_n(C) of a naturally indexed chain complex, as in Definition 1.7.

@[implicit_reducible]

noncomputable instance AlgebraicTopologyI.NatChainComplex.instAddCommGroupHomology (C : NatChainComplex) (n : ℕ) : AddCommGroup (C.homologyGroup n)

The homology group of a naturally indexed chain complex inherits its abelian group structure from the quotient construction.

noncomputable def AlgebraicTopologyI.SingularRelativeHomology (n : ℕ) (X : Type u_1) [TopologicalSpace X] (A : Set X) : Type u_1

The nth relative singular homology H_n(X, A) = H_n(S_*(X, A)) of a pair (X, A). This is Definition 8.6.