noncomputable def HomTensorAdjunction.homTensorEquiv (R : Type u_1) [CommSemiring R] (L : Type u_2) (M : Type u_3) (N : Type u_4) [AddCommMonoid L] [AddCommMonoid M] [AddCommMonoid N] [Module R L] [Module R M] [Module R N] : (L →ₗ[R] M →ₗ[R] N) ≃ₗ[R] TensorProduct R L M →ₗ[R] N

Lemma 23.1 (Hom–tensor adjunction). The natural map Hom(L, Hom(M, N)) → Hom(L ⊗ M, N) is an isomorphism, witnessed here as an R-linear equivalence between L →ₗ[R] M →ₗ[R] N and L ⊗[R] M →ₗ[R] N.

@[reducible, inline]

abbrev DirectedSystems.DirectedPoset (I : Type u_1) [Preorder I] : Prop

Definition 23.2. A poset (I, ≤) is directed if for every i, j ∈ I there is some k ∈ I with i ≤ k and j ≤ k.

@[reducible, inline]

abbrev DirectedSystems.DirectedSystemFunctor (I : Type u_1) [Preorder I] [IsDirected I fun (x1 x2 : I) => x1 ≤ x2] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] : Type (max u_1 u_3 u_1 u_2)

Definition 23.4. An I-directed system in a category C (for I a directed poset) is a functor I ⥤ C, i.e. objects X_i together with coherent maps X_i → X_j whenever i ≤ j.

@[reducible, inline]

noncomputable abbrev DirectedSystems.CategoricalDirectLimit {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] : C

Definition 23.8 (categorical form). The direct limit lim→ F of a diagram F : J ⥤ C is the colimit of F, i.e. the initial cocone under F.

@[reducible, inline]

abbrev DirectedSystems.DirectLimit (R : Type u_1) [Semiring R] (ι : Type u_2) [Preorder ι] [DecidableEq ι] (G : ι → Type u_3) [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) : Type (max u_3 u_2)

Definition 23.8 (module form). The direct limit of a directed system of R-modules, realized as Mathlib's Module.DirectLimit of the modules G i along the structure maps f.

noncomputable def DirectLimitTensor.directLimitTensorIso {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (N : Type u_4) [AddCommMonoid N] [Module R N] : TensorProduct R (Module.DirectLimit G f) N ≃ₗ[R] Module.DirectLimit (fun (i : ι) => TensorProduct R (G i) N) fun (i j : ι) (h : i ≤ j) => LinearMap.rTensor N (f i j h)

Proposition 23.10. For a directed system of R-modules G : ι → Mod_R and an R-module N, the tensor product commutes with direct limits: there is a natural isomorphism (lim→ G_i) ⊗_R N ≃ lim→ (G_i ⊗_R N).

theorem DirectLimitCharacterization.directLimit_lift_bijective_iff {R : Type u_1} [Ring R] {ι : Type u_2} [Preorder ι] [DecidableEq ι] [Nonempty ι] [IsDirectedOrder ι] {G : ι → Type u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {L : Type u_4} [AddCommGroup L] [Module R L] (g : (i : ι) → G i →ₗ[R] L) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) : Function.Bijective ⇑(Module.DirectLimit.lift R ι G f g Hg) ↔ (∀ (x : L), ∃ (i : ι) (xᵢ : G i), (g i) xᵢ = x) ∧ ∀ (i : ι) (xᵢ : G i), (g i) xᵢ = 0 → ∃ (j : ι) (hij : i ≤ j), (f i j hij) xᵢ = 0

Lemma 23.11. A cocone (g_i : G_i → L) on a directed system of R-modules exhibits L as the direct limit if and only if (1) every x ∈ L is of the form g_i x_i for some i and x_i ∈ G_i, and (2) any x_i ∈ G_i with g_i x_i = 0 becomes zero in some G_j with j ≥ i.

noncomputable def AlgebraicTopologyI.SingularHomologyGroupQ (n : ℕ) (X : Type) [TopologicalSpace X] : AddCommGrpCat

The n-th singular homology of a space X with rational coefficients, packaged as an object of AddCommGrpCat.

noncomputable def AlgebraicTopologyI.AddCommGrpCat.isoOfAddEquiv' {A B : AddCommGrpCat} (e : ↑A ≃+ ↑B) : A ≅ B

Promote an AddEquiv between objects of AddCommGrpCat to a categorical isomorphism.

theorem AlgebraicTopologyI.universalCoefficientTensorIso (n : ℕ) (X : Type) [TopologicalSpace X] : Nonempty (((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of (TensorProduct ℤ ℤ ℚ))).obj (TopCat.of X) ≅ AddCommGrpCat.of (TensorProduct ℤ ↑(SingularHomologyGroup n X) ℚ))

Auxiliary form of the universal-coefficient style identification used to derive Corollary 23.14: singular homology with coefficients in ℤ ⊗[ℤ] ℚ agrees up to isomorphism with integral homology tensored with ℚ.

theorem AlgebraicTopologyI.rational_homology_eq_tensor (n : ℕ) (X : Type) [TopologicalSpace X] : Nonempty (SingularHomologyGroupQ n X ≅ AddCommGrpCat.of (TensorProduct ℤ ↑(SingularHomologyGroup n X) ℚ))

Corollary 23.14. Rational singular homology agrees with integral singular homology tensored with ℚ: H_n(X; ℚ) ≅ H_n(X) ⊗ ℚ.