@[reducible, inline]

abbrev BilinearMap.BilinearMapType (R : Type u_1) [CommSemiring R] (M : Type u_2) (N : Type u_3) (P : Type u_4) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] : Type (max u_2 u_4 u_3)

(Definition 20.1) The type of $R$-bilinear maps $\beta : M \times N \to P$, encoded as a linear map $M \to (N \to_{R} P)$; concretely $\beta$ satisfies $\beta(x+x', y) = \beta(x,y) + \beta(x',y)$, $\beta(x, y+y') = \beta(x,y) + \beta(x,y')$, $\beta(rx,y) = r\beta(x,y)$, $\beta(x,ry) = r\beta(x,y)$.

def TensorProduct.universalProperty {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] TensorProduct R M N →ₗ[R] P

(Definition 20.3) The universal property of the tensor product as the universal $R$-bilinear target: $R$-bilinear maps $M \times N \to P$ are in linear bijection with $R$-linear maps $M \otimes_R N \to P$.

theorem TensorProduct.mk_isBilinearMap {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : IsBilinearMap R fun (m : M) (n : N) => m ⊗ₜ[R] n

The canonical map $\beta_0 : M \times N \to M \otimes_R N$, $(m, n) \mapsto m \otimes n$, is $R$-bilinear; this is the universal bilinear map from Definition 20.3.

theorem TensorProduct.lift_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (β : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : (lift β) (m ⊗ₜ[R] n) = (β m) n

Computation rule for the universal map: the linear extension of a bilinear form $\beta$ to $M \otimes_R N$ agrees with $\beta$ on simple tensors, $\widetilde{\beta}(m \otimes n) = \beta(m,n)$.

theorem TensorProduct.lift_unique {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (β : M →ₗ[R] N →ₗ[R] P) (g : TensorProduct R M N →ₗ[R] P) (hg : ∀ (m : M) (n : N), g (m ⊗ₜ[R] n) = (β m) n) : g = lift β

Uniqueness in the universal property of the tensor product: any linear map $g : M \otimes_R N \to P$ that agrees with $\beta$ on simple tensors coincides with the linear extension TensorProduct.lift β.

theorem TensorProduct.construction {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct R M N = (addConGen (Eqv R M N)).Quotient

(Construction 20.4) Definitional unfolding of M ⊗[R] N as the quotient of the free abelian group on $M \times N$ by the additive congruence generated by the bilinearity relations.

theorem TensorProduct.induction {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (C : TensorProduct R M N → Prop) (zero : C 0) (tmul : ∀ (m : M) (n : N), C (m ⊗ₜ[R] n)) (add : ∀ (x y : TensorProduct R M N), C x → C y → C (x + y)) (t : TensorProduct R M N) : C t

Induction principle on $M \otimes_R N$: to prove a predicate $C$ for every tensor it suffices to verify it for $0$, for simple tensors $m \otimes n$, and to show $C$ is closed under sums.

noncomputable def HomologyWithCoefficients.singularH : ℤ → EilenbergSteenrod.TopPair → Type

The underlying type of the $n$-th singular homology group $H_n(X, A)$ of a topological pair, serving as the value of the singular homology theory functor.

@[implicit_reducible]

noncomputable instance HomologyWithCoefficients.singularH_instAddCommGroup (n : ℤ) (P : EilenbergSteenrod.TopPair) : AddCommGroup (singularH n P)

Each singular homology group $H_n(X, A)$ is an abelian group.

noncomputable def HomologyWithCoefficients.singularH_map (n : ℤ) {P Q : EilenbergSteenrod.TopPair} : EilenbergSteenrod.MapOfPairs P Q → singularH n P →+ singularH n Q

Functoriality: a map of pairs $f : (X, A) \to (Y, B)$ induces a group homomorphism $f_* : H_n(X, A) \to H_n(Y, B)$.

theorem HomologyWithCoefficients.singularH_map_id (n : ℤ) (P : EilenbergSteenrod.TopPair) : singularH_map n (EilenbergSteenrod.MapOfPairs.id P) = AddMonoidHom.id (singularH n P)

Functoriality (identities): the identity map of pairs induces the identity on homology.

theorem HomologyWithCoefficients.singularH_map_comp (n : ℤ) {P Q R : EilenbergSteenrod.TopPair} (f : EilenbergSteenrod.MapOfPairs P Q) (g : EilenbergSteenrod.MapOfPairs Q R) : singularH_map n (g.comp f) = (singularH_map n g).comp (singularH_map n f)

Functoriality (compositions): $(g \circ f)_* = g_* \circ f_*$ on singular homology.

noncomputable def HomologyWithCoefficients.singularH_boundary (n : ℤ) (P : EilenbergSteenrod.TopPair) : singularH (n + 1) P →+ singularH n P.subPair

The connecting homomorphism $\partial : H_{n+1}(X, A) \to H_n(A)$ of the long exact sequence of a pair.

theorem HomologyWithCoefficients.singularH_boundary_natural (n : ℤ) {P Q : EilenbergSteenrod.TopPair} (f : EilenbergSteenrod.MapOfPairs P Q) : (singularH_map n f.restrictToSub).comp (singularH_boundary n P) = (singularH_boundary n Q).comp (singularH_map (n + 1) f)

Naturality of the connecting homomorphism with respect to maps of pairs.

theorem HomologyWithCoefficients.singularH_homotopy_invariance (n : ℤ) {P Q : EilenbergSteenrod.TopPair} (f₀ f₁ : EilenbergSteenrod.MapOfPairs P Q) : EilenbergSteenrod.AreHomotopic f₀ f₁ → singularH_map n f₀ = singularH_map n f₁

Homotopy invariance (Eilenberg-Steenrod axiom 1): homotopic maps of pairs induce the same map on singular homology.

theorem HomologyWithCoefficients.singularH_excision (n : ℤ) (P : EilenbergSteenrod.TopPair) (U : Set P.space) : EilenbergSteenrod.IsExcisiveTriple P U → Function.Bijective ⇑(singularH_map n (EilenbergSteenrod.excisionInclusion P U))

Excision (Eilenberg-Steenrod axiom 2): for an excisive triple $(X, A, U)$ the inclusion $(X - U, A - U) \hookrightarrow (X, A)$ induces an isomorphism in homology.

theorem HomologyWithCoefficients.singularH_exact_at_sub (n : ℤ) (P : EilenbergSteenrod.TopPair) : Function.Exact ⇑(singularH_boundary n P) ⇑(singularH_map n (EilenbergSteenrod.inclusionSubToSpace P))

Long exact sequence (exactness at $H_n(A)$): the image of the connecting map $\partial : H_{n+1}(X, A) \to H_n(A)$ equals the kernel of $H_n(A) \to H_n(X)$.

theorem HomologyWithCoefficients.singularH_exact_at_space (n : ℤ) (P : EilenbergSteenrod.TopPair) : Function.Exact ⇑(singularH_map n (EilenbergSteenrod.inclusionSubToSpace P)) ⇑(singularH_map n (EilenbergSteenrod.inclusionSpaceToPair P))

Long exact sequence (exactness at $H_n(X)$): the image of $H_n(A) \to H_n(X)$ equals the kernel of $H_n(X) \to H_n(X, A)$.

theorem HomologyWithCoefficients.singularH_exact_at_pair (n : ℤ) (P : EilenbergSteenrod.TopPair) : Function.Exact ⇑(singularH_map (n + 1) (EilenbergSteenrod.inclusionSpaceToPair P)) ⇑(singularH_boundary n P)

Long exact sequence (exactness at $H_{n+1}(X, A)$): the image of $H_{n+1}(X) \to H_{n+1}(X, A)$ equals the kernel of the connecting map $\partial$.

theorem HomologyWithCoefficients.singularH_dimension (n : ℤ) : n ≠ 0 → Subsingleton (singularH n EilenbergSteenrod.TopPair.point)

Dimension axiom (Eilenberg-Steenrod): $H_n(\mathrm{pt}) = 0$ for $n \neq 0$.

theorem HomologyWithCoefficients.singularH_coproduct (n : ℤ) {ι : Type} [DecidableEq ι] (X : ι → Type) [(i : ι) → TopologicalSpace (X i)] : Function.Bijective ⇑(DirectSum.toAddMonoid fun (i : ι) => singularH_map n (EilenbergSteenrod.coproductInclusion ι X i))

Milnor (additivity) axiom: the inclusions $X_i \hookrightarrow \coprod_i X_i$ induce an isomorphism $\bigoplus_i H_n(X_i) \xrightarrow{\cong} H_n(\coprod_i X_i)$.

noncomputable def HomologyWithCoefficients.singularHomologyTheoryZ : EilenbergSteenrod.HomologyTheory

Singular homology with integer coefficients, packaged as a HomologyTheory (i.e. satisfying all Eilenberg-Steenrod axioms plus the Milnor axiom).

theorem HomologyWithCoefficients.singularH_point_zero_iso : Nonempty (singularH 0 EilenbergSteenrod.TopPair.point ≃+ ℤ)

$H_0(\mathrm{pt}; \mathbf{Z}) \cong \mathbf{Z}$: the zeroth integral singular homology of a point is isomorphic to $\mathbf{Z}$.

theorem HomologyWithCoefficients.singularHomologyTheoryZ_point_zero_iso : Nonempty (singularHomologyTheoryZ.H 0 EilenbergSteenrod.TopPair.point ≃+ ℤ)

Restating singularH_point_zero_iso for the packaged homology theory: the value at a point in degree zero is $\mathbf{Z}$.

theorem HomologyWithCoefficients.exact_lTensor {A B C : Type} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (M : Type) [AddCommGroup M] {f : A →+ B} {g : B →+ C} (hexact : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(TensorProduct.map f.toIntLinearMap LinearMap.id).toAddMonoidHom ⇑(TensorProduct.map g.toIntLinearMap LinearMap.id).toAddMonoidHom

Right exactness of $-\otimes_{\mathbf{Z}} M$ on exact sequences: if $A \to B \to C$ is exact then so is $A \otimes M \to B \otimes M \to C \otimes M$, used to transfer the long exact sequences of singularHomologyTheoryZ to the coefficient theory.

theorem HomologyWithCoefficients.coproduct_lTensor (h : EilenbergSteenrod.HomologyTheory) (M : Type) [AddCommGroup M] (n : ℤ) {ι : Type} [DecidableEq ι] (X : ι → Type) [(i : ι) → TopologicalSpace (X i)] (hbij : Function.Bijective ⇑(DirectSum.toAddMonoid fun (i : ι) => h.map n (EilenbergSteenrod.coproductInclusion ι X i))) : Function.Bijective ⇑(DirectSum.toAddMonoid fun (i : ι) => (TensorProduct.map (h.map n (EilenbergSteenrod.coproductInclusion ι X i)).toIntLinearMap LinearMap.id).toAddMonoidHom)

Compatibility of the Milnor axiom with tensoring by $M$: tensoring a bijection $\bigoplus_i h_n(X_i) \cong h_n(\coprod_i X_i)$ with $M$ yields a bijection $\bigoplus_i (h_n(X_i) \otimes M) \cong h_n(\coprod_i X_i) \otimes M$, the additivity statement for the coefficient-twisted theory.

noncomputable def HomologyWithCoefficients.homologyTheoryWithCoefficients (M : Type) [AddCommGroup M] : EilenbergSteenrod.HomologyTheory

(Proposition 20.11) Homology with coefficients in an abelian group $M$ defines a homology theory $H_*(X, A; M) := H_*(X, A) \otimes_{\mathbf{Z}} M$ satisfying the Eilenberg-Steenrod axioms; in particular $H_0(\mathrm{pt}; M) = M$.