Algebraic topology of spaces and manifolds
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
DefinitionThe groupoid van Kampen theorem#
For an open cover of X, the fundamental groupoid of
X is the colimit of the fundamental groupoids of the nonempty finite intersections of members
of the cover.
TauCeti.FundamentalGroupoid.isColimitCechCocone.{u, v} {X : TopCat} {ι : Type u}
{U : ι → TopologicalSpace.Opens ↑X} (hU : TopologicalSpace.IsOpenCover U) :
CategoryTheory.Limits.IsColimit (TauCeti.FundamentalGroupoid.cechCocone U)
Lean
Formalized in Tau Ceti as TauCeti.FundamentalGroupoid.isColimitCechCocone.
Sources
TheoremExcision of a set with closure in the interior of the subspace#
If closure Z ⊆ interior B,
the inclusion of pairs (X ∖ Z, B ∖ Z) ⟶ (X, B) induces isomorphisms on relative singular
homology.
TopPair.isIso_singularHomologyMap_excisionMap_compl.{w, v, u} {A : Type u}
[CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A] (R : A) {X : TopCat} (B Z : Set ↑X) (h : closure Z ⊆ interior B)
(n : ℕ) : CategoryTheory.IsIso (TopPair.singularHomologyMap (TopPair.excisionMap Zᶜ B) R n)
Lean
Formalized in Tau Ceti as TopPair.isIso_singularHomologyMap_excisionMap_compl.
Sources
Uses 1
TheoremThe Hurewicz theorem#
If πₖ(X, x) is trivial for every k < n + 2, then the Hurewicz
map πₙ₊₂(X, x) → Hₙ₊₂(X; ℤ), [p] ↦ p_*[Iⁿ⁺²], is bijective.
HomotopyGroup.bijective_hurewicz {X : Type} [TopologicalSpace X] {x : X} {n : ℕ}
(hX : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) X x)) :
Function.Bijective fun a => (ModuleCat.Hom.hom (HomotopyGroup.hurewicz (↧ℤ) (n + 1) a)) 1
Lean
Formalized in Tau Ceti as HomotopyGroup.bijective_hurewicz.
Other forms
The Hurewicz theorem in degree one. Formalized in Tau Ceti as TauCeti.HurewiczOne.hurewiczAddEquiv.
TauCeti.HurewiczOne.hurewiczAddEquiv {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) :
Additive (Abelianization (FundamentalGroup (↑X) x)) ≃+ ↑(TauCeti.HurewiczOne.H₁ X)
The Hurewicz theorem in degree one. Formalized in Tau Ceti as TauCeti.HurewiczOne.hurewiczHomologyAddEquiv.
TauCeti.HurewiczOne.hurewiczHomologyAddEquiv {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) :
Additive (Abelianization (FundamentalGroup (↑X) x)) ≃+
↑(HomologicalComplex.homology ((TauCeti.singularChains ℤ).obj X) 1)
Sources
Uses 2 · Used by 5
TheoremThe relative Hurewicz isomorphism for highly connected spaces#
Let B be a subspace of
Y and b ∈ B. If πₖ(B, b) and πₖ(Y, b) are trivial for every k < n + 2, then the
relative Hurewicz map πₙ₊₂(Y, B, b) → Hₙ₊₂(Y, B; ℤ), [p] ↦ p_*[Iⁿ⁺²], is bijective. In degree
two, that is for n = 0, the hypotheses say that B and Y are simply connected.
TauCeti.RelHomotopyGroup.bijective_hurewicz_of_subsingleton_homotopyGroup {Y : TopCat} {B : Set ↑Y}
{n : ℕ} (b : ↑B) (hB : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) (↑B) b))
(hY : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) ↑Y ↑b)) :
Function.Bijective fun a =>
(ModuleCat.Hom.hom (TauCeti.RelHomotopyGroup.hurewicz (↧ℤ) (n + 1) a)) 1
Lean
Formalized in Tau Ceti as TauCeti.RelHomotopyGroup.bijective_hurewicz_of_subsingleton_homotopyGroup.
Sources
- Tau Ceti documentation:
TauCeti.RelHomotopyGroup.bijective_hurewicz_of_subsingleton_homotopyGroup - Source of
TauCeti.RelHomotopyGroup.bijective_hurewicz_of_subsingleton_homotopyGroupin TauCeti/AlgebraicTopology/Homotopy/Hurewicz/Relative.lean - Tau Ceti roadmap status: Algebraic topology of spaces and manifolds
DefinitionWhitehead's theorem (Hatcher, Theorem 4.5)#
A weak homotopy equivalence f between spaces
of CW type is a homotopy equivalence. This is the homotopy equivalence whose forward map is f
itself (ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv_toFun); its homotopy inverse is a
lift of the identity through f given by
ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic.
ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv.{u_1, u_2} {X : Type u_1} [TopologicalSpace X]
{Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} [TauCeti.CWType X] [TauCeti.CWType Y]
(hf : f.IsWeakHomotopyEquivalence) : ContinuousMap.HomotopyEquiv X Y
Lean
Formalized in Tau Ceti as ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv.
Sources
DefinitionThe Künneth short exact sequence over a hereditary commutative ring splits#
The Künneth short exact sequence over a hereditary commutative ring splits, so that
Hₘ₊₁(X × Y; k) is the direct sum of ⨁_{p + q = m + 1} Hₚ(X; k) ⊗ H_q(Y; k) and
⨁_{p + q = m} Tor₁(Hₚ(X; k), H_q(Y; k))
(CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct).
The splitting depends on chosen splittings of the cycles of the singular chain complexes, and need
not be natural in X and Y.
TopCat.singularHomologyKunnethUnitSplitting.{w} (k : Type w) [CommRing k]
[∀ (V : ModuleCat k), CategoryTheory.HasProjectiveDimensionLE V 1] (X Y : TopCat) (m : ℕ) :
(TopCat.singularHomologyKunnethUnitShortComplex k X Y m).Splitting
DefinitionThe splitting of the universal coefficient sequence of singular cohomology over a hereditary commutative ring#
a k-linear equivalence
Hⁿ⁺¹(X; R, M) ≃ₗ[k] Ext¹(Hₙ(X; R), M) × Hom(Hₙ₊₁(X; R), M) whose second component is the
Kronecker map (TopCat.singularUniversalCoefficientEquiv_apply_snd) and whose inverse restricts
to TopCat.singularExtToCohomology on the first factor
(TopCat.singularUniversalCoefficientEquiv_symm_inl). It is built from the section
TopCat.singularKroneckerSection and is not natural in X.
TopCat.singularUniversalCoefficientEquiv.{w} {k : Type w} [CommRing k]
[∀ (V : ModuleCat k), CategoryTheory.HasProjectiveDimensionLE V 1] (X : TopCat)
(R M : ModuleCat k) [Module.Projective k ↑R] (n : ℕ) :
↑(TopCat.singularCohomology R k M X (n + 1)) ≃ₗ[k]
CategoryTheory.Abelian.Ext
(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj R).obj X) M 1 ×
(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) (n + 1)).obj R).obj X ⟶ M)
DefinitionA classical relative CW complex in a Hausdorff space is a categorical relative CW complex#
The inclusion of the base D into C is the transfinite composition of the inclusions of the
skeleta skeletonLT C n, and the step from skeletonLT C n to skeletonLT C (n + 1) attaches
the n-cells of C along their attaching maps. The body is exposed so that the n-th space is
the skeleton skeletonObj C n and the cells attached at step n are cell C n by definition.
TauCeti.toRelativeCWComplex.{w} {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X}
(C : Set X) [Topology.RelCWComplex C D] :
TopCat.RelativeCWComplex (TopCat.ofHom (ContinuousMap.inclusion ⋯))
DefinitionThe top homology of a compact manifold is the module of parallel families of local classes#
For a compact Hausdorff space modelled on a real normed space of finite dimension n,
the restrictions Hₙ(M, M ∖ M; N) ⟶ Hₙ(M, M ∖ {x}; N) exhibit Hₙ(M, M ∖ M; N) as the limit of
the local homology system: every transport-invariant family of local classes is the family of
restrictions of exactly one class.
TauCeti.isLimitLocalHomologySystemCone.{w} {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) (M E : Type w)
[TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
[ChartedSpace E M] [CompactSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n) :
CategoryTheory.Limits.IsLimit (TauCeti.localHomologySystemCone N M E n)
Uses 2
TheoremExactness of the Milnor sequence at Hⱼ(lim C)#
For a tower whose shift is surjective
in every degree, the image of lim¹ Hᵢ(Cₙ) → Hⱼ(lim C) is the kernel of
Hⱼ(lim C) → lim Hⱼ(Cₙ).
TauCeti.ComplexTower.exact_limOneToHomology_homologyToLim.{v, u, w} {R : Type u} [Ring R]
{ι : Type w} {c : ComplexShape ι} {C : TauCeti.ComplexTower R c}
(hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) {i j : ι} (hij : c.Rel i j) :
Function.Exact ⇑(TauCeti.ComplexTower.limOneToHomology hC hij) ⇑(C.homologyToLim j)
Lean
Formalized in Tau Ceti as TauCeti.ComplexTower.exact_limOneToHomology_homologyToLim.
Sources
TheoremInductive Hurewicz vanishing criterion (singular homology)#
If X is path connected with
trivial π_ 1 X x and its integral singular homology vanishes in every degree n + 2, then all
homotopy groups π_ k X x are trivial.
TauCeti.subsingleton_homotopyGroup_of_isZero_homology_singularChains {X : Type} [TopologicalSpace X]
(x : X) [PathConnectedSpace X] [Subsingleton (HomotopyGroup.Pi 1 X x)]
(hH :
∀ (n : ℕ),
CategoryTheory.Limits.IsZero
(HomologicalComplex.homology ((TauCeti.singularChains ℤ).obj ↧X) (n + 2)))
(k : ℕ) : Subsingleton (HomotopyGroup.Pi k X x)
Lean
Formalized in Tau Ceti as TauCeti.subsingleton_homotopyGroup_of_isZero_homology_singularChains.
Other forms
Inductive Hurewicz vanishing criterion (normalized cubical homology). Formalized in Tau Ceti as TauCeti.subsingleton_homotopyGroup_of_isZero_homology_normalizedCubicalChainComplex.
TauCeti.subsingleton_homotopyGroup_of_isZero_homology_normalizedCubicalChainComplex {X : Type}
[TopologicalSpace X] (x : X) [PathConnectedSpace X] [Subsingleton (HomotopyGroup.Pi 1 X x)]
(hH :
∀ (n : ℕ),
CategoryTheory.Limits.IsZero
(HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex ℤ).obj ↧X) (n + 2)))
(k : ℕ) : Subsingleton (HomotopyGroup.Pi k X x)
Sources
TheoremThe relative universal coefficient theorem above a projective homology module, over a hereditary commutative ring#
for a projective coefficient module R, if Hₙ(X, A; R) is
projective, the relative Kronecker map Hⁿ⁺¹(X, A; R, M) →ₗ[k] (Hₙ₊₁(X, A; R) ⟶ M) is bijective,
for every module M. Nothing is assumed about the relative homology in the other degrees.
TopPair.singularKronecker_bijective_succ_of_projective_homology.{w, u_1} {k : Type u_1} [CommRing k]
(P : TopPair) (R M : ModuleCat k) [Module.Projective k ↑R]
[∀ (V : ModuleCat k), CategoryTheory.HasProjectiveDimensionLE V 1]
[CategoryTheory.Linear k (ModuleCat k)] (n : ℕ)
[CategoryTheory.Projective (P.singularHomology R n)] :
Function.Bijective ⇑(P.singularKronecker k (n + 1))
Lean
Formalized in Tau Ceti as TopPair.singularKronecker_bijective_succ_of_projective_homology.
Sources
Uses 1
TheoremThe relative universal coefficient theorem below the first non-projective homology, over any commutative ring k#
for a projective coefficient module R, if the relative singular
homology modules Hⱼ(X, A; R) of a pair are projective for j < n, for instance zero, the
relative Kronecker map Hⁿ(X, A; R, M) →ₗ[k] (Hₙ(X, A; R) ⟶ M) is bijective, for every module
M.
TopPair.singularKronecker_bijective_of_projective_homology_lt.{w, u_1} {k : Type u_1} [CommRing k]
(P : TopPair) (R M : ModuleCat k) [Module.Projective k ↑R] [CategoryTheory.Linear k (ModuleCat k)]
(n : ℕ) (h : ∀ j < n, CategoryTheory.Projective (P.singularHomology R j)) :
Function.Bijective ⇑(P.singularKronecker k n)
Lean
Formalized in Tau Ceti as TopPair.singularKronecker_bijective_of_projective_homology_lt.
Sources
Uses 1 · Used by 1
TheoremThe universal coefficient theorem above a projective homology module, over a hereditary commutative ring#
for a projective coefficient module R, if Hₙ(X; R) is projective, the
Kronecker map Hⁿ⁺¹(X; R, M) →ₗ[k] (Hₙ₊₁(X; R) ⟶ M) is bijective, for every module M. The
Ext¹(Hₙ(X; R), M) term of the universal coefficient sequence vanishes.
TopCat.singularKronecker_bijective_succ_of_projective_homology.{w} {k : Type w} [CommRing k]
[∀ (V : ModuleCat k), CategoryTheory.HasProjectiveDimensionLE V 1] (X : TopCat)
(R M : ModuleCat k) [Module.Projective k ↑R] (n : ℕ)
[CategoryTheory.Projective
(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj R).obj X)] :
Function.Bijective ⇑(X.singularKronecker k (n + 1))
Lean
Formalized in Tau Ceti as TopCat.singularKronecker_bijective_succ_of_projective_homology.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.