def IsExcisive (X : Type u_1) [TopologicalSpace X] (A U : Set X) : Prop

Definition 10.1 (Excisive triple). The triple (X, A, U) is excisive when closure U ⊆ interior A, i.e. the closure of U lies in the topological interior of A.

This is the hypothesis under which the excision theorem (Theorem 10.2) asserts that the inclusion (X ∖ U, A ∖ U) → (X, A) induces an isomorphism on relative homology.

@[reducible, inline]

noncomputable abbrev Excision.singularChainZ : CategoryTheory.Functor TopCat (ChainComplex AddCommGrpCat ℕ)

The singular chain complex functor with integer coefficients, X ↦ C_*(X; \mathbb{Z}).

def Excision.subspaceTopInclusion {X : Type} [TopologicalSpace X] (A : Set X) : TopCat.of ↑A ⟶ TopCat.of X

The continuous inclusion A ↪ X of a subspace, as a morphism in TopCat.

noncomputable def Excision.subspaceChainInclusion (X : Type) [TopologicalSpace X] (A : Set X) : singularChainZ.obj (TopCat.of ↑A) ⟶ singularChainZ.obj (TopCat.of X)

The chain map C_*(A; ℤ) → C_*(X; ℤ) induced by the subspace inclusion A ↪ X.

noncomputable def Excision.relativeSingularChainComplex (X : Type) [TopologicalSpace X] (A : Set X) : ChainComplex AddCommGrpCat ℕ

The relative singular chain complex C_*(X, A; ℤ) := C_*(X) / C_*(A), defined as the cokernel of the chain inclusion C_*(A) ↪ C_*(X).

noncomputable def Excision.RelativeSingularHomologyGroup (n : ℕ) (X : Type) [TopologicalSpace X] (A : Set X) : AddCommGrpCat

The n-th relative singular homology group H_n(X, A; ℤ), defined as the n-th homology of the relative singular chain complex C_*(X, A).

def Excision.excisedSubsetToSubspace (X : Type) [TopologicalSpace X] (A U : Set X) : TopCat.of ↑(Subtype.val ⁻¹' A) ⟶ TopCat.of ↑A

The continuous inclusion A ∖ U ↪ A obtained by viewing A \ U first as a subset of X \ U and then forgetting the complement.

def Excision.complementInclusion (X : Type) [TopologicalSpace X] (U : Set X) : TopCat.of ↑Uᶜ ⟶ TopCat.of X

The continuous inclusion X ∖ U ↪ X.

theorem Excision.excision_square_comm (X : Type) [TopologicalSpace X] (A U : Set X) : CategoryTheory.CategoryStruct.comp (subspaceTopInclusion (Subtype.val ⁻¹' A)) (complementInclusion X U) = CategoryTheory.CategoryStruct.comp (excisedSubsetToSubspace X A U) (subspaceTopInclusion A)

Commutativity of the square (A ∖ U) ↪ (X ∖ U); (A ∖ U) ↪ A with (X ∖ U) ↪ X; A ↪ X, which is what makes the excision pair-inclusion a well-defined morphism of pairs.

noncomputable def Excision.excisionRelativeChainMap (X : Type) [TopologicalSpace X] (A U : Set X) : relativeSingularChainComplex (↑Uᶜ) (Subtype.val ⁻¹' A) ⟶ relativeSingularChainComplex X A

The chain map between relative chain complexes C_*(X ∖ U, A ∖ U) → C_*(X, A) induced by the pair inclusion. Excision asserts that this map is a quasi-isomorphism whenever (X, A, U) is excisive.

noncomputable def Excision.excisionHomologyMap (X : Type) [TopologicalSpace X] (A U : Set X) (n : ℕ) : RelativeSingularHomologyGroup n (↑Uᶜ) (Subtype.val ⁻¹' A) ⟶ RelativeSingularHomologyGroup n X A

The induced map on degree-n relative homology H_n(X ∖ U, A ∖ U) → H_n(X, A) coming from the excision chain map.

theorem Excision.cover_of_excisive {X : Type} [TopologicalSpace X] {A U : Set X} (hexc : IsExcisive X A U) : interior A ∪ interior Uᶜ = Set.univ

An excisive triple (X, A, U) produces an open cover of X by interior A and interior Uᶜ. This converts the excision hypothesis into the form needed by the locality principle.

noncomputable def Excision.smallChainComplex (X : Type) [TopologicalSpace X] (A B : Set X) : ChainComplex AddCommGrpCat ℕ

The small chain complex C^{\{A, B\}}_*(X) for the two-element cover {A, B}: the image of the chain map C_*(A) ⊕ C_*(B) → C_*(X) sending a pair to the sum of its components in C_*(X).

noncomputable def Excision.smallChainInclusion (X : Type) [TopologicalSpace X] (A B : Set X) : smallChainComplex X A B ⟶ singularChainZ.obj (TopCat.of X)

The inclusion C^{\{A, B\}}_*(X) ↪ C_*(X) of the small chain complex into the full singular chain complex (the canonical image inclusion).

theorem Excision.twoElementCover_isCover {X : Type} [TopologicalSpace X] {A B : Set X} (hcover : interior A ∪ interior B = Set.univ) : IsCover {A, B}

If interior A ∪ interior B = X, then {A, B} is a cover of X in the sense required by the locality principle.

instance Excision.smallSingularInclusion_mono (X : Type) [TopologicalSpace X] (𝒜 : Set (Set X)) : CategoryTheory.Mono (LocalityPrinciple.smallSingularInclusion (TopCat.of X) 𝒜)

The inclusion of small singular chains into all singular chains is a monomorphism.

noncomputable def Excision.smallChainFactorization (X : Type) [TopologicalSpace X] (A B : Set X) : singularChainZ.obj (TopCat.of ↑A) ⊞ singularChainZ.obj (TopCat.of ↑B) ⟶ LocalityPrinciple.smallSingularChainComplex (TopCat.of X) {A, B}

The canonical strong epimorphism C_*(A) ⊕ C_*(B) ↠ C^{\{A, B\}}_*(X) from the biproduct to the small singular chain complex for the two-element cover {A, B}.

instance Excision.smallChainFactorization_strongEpi (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.StrongEpi (smallChainFactorization X A B)

The factorization map C_*(A) ⊕ C_*(B) → C^{\{A, B\}}_*(X) is a strong epimorphism.

theorem Excision.smallChainFactorization_comp (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.CategoryStruct.comp (smallChainFactorization X A B) (LocalityPrinciple.smallSingularInclusion (TopCat.of X) {A, B}) = CategoryTheory.Limits.biprod.desc (subspaceChainInclusion X A) (subspaceChainInclusion X B)

Compatibility: the factorization through the small chain complex composed with the inclusion into C_*(X) recovers the canonical biproduct map C_*(A) ⊕ C_*(B) → C_*(X).

noncomputable def Excision.smallChainIso_of_twoElementCover (X : Type) [TopologicalSpace X] (A B : Set X) : smallChainComplex X A B ≅ LocalityPrinciple.smallSingularChainComplex (TopCat.of X) {A, B}

The image presentation smallChainComplex X A B is canonically isomorphic to the small singular chain complex C^{\{A, B\}}_*(X) defined via the cover machinery.

theorem Excision.smallChainInclusion_comm_of_twoElementCover (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.CategoryStruct.comp (smallChainIso_of_twoElementCover X A B).hom (LocalityPrinciple.smallSingularInclusion (TopCat.of X) {A, B}) = smallChainInclusion X A B

Compatibility of the isomorphism smallChainIso_of_twoElementCover with the inclusions into C_*(X): the two presentations of C^{\{A, B\}}_*(X) ↪ C_*(X) agree.

theorem Excision.localityPrinciple (X : Type) [TopologicalSpace X] (A B : Set X) (hcover : interior A ∪ interior B = Set.univ) : QuasiIso (smallChainInclusion X A B)

Locality principle (two-element cover form). If {A, B} is a topological cover of X (i.e. interior A ∪ interior B = X), then the inclusion C^{\{A, B\}}_*(X) ↪ C_*(X) is a quasi-isomorphism.

This is the key technical input to the excision theorem: it says that every singular chain can be subdivided into one supported on A or B without changing homology.

noncomputable def Excision.smallChainInclusionA (X : Type) [TopologicalSpace X] (A B : Set X) : singularChainZ.obj (TopCat.of ↑A) ⟶ smallChainComplex X A B

The chain map C_*(A) → C^{\{A, B\}}_*(X) factoring the inclusion C_*(A) ↪ C_*(X) through the small chain complex.

theorem Excision.smallChainInclusionA_comp_ι (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.CategoryStruct.comp (smallChainInclusionA X A B) (smallChainInclusion X A B) = subspaceChainInclusion X A

Compatibility: the small-complex factorization of C_*(A) ↪ C_*(X) composed with the inclusion of the small complex into C_*(X) recovers the original inclusion.

noncomputable def Excision.bottomSES (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.ShortComplex (ChainComplex AddCommGrpCat ℕ)

The defining short exact sequence of the relative chain complex 0 → C_*(A) → C_*(X) → C_*(X, A) → 0.

noncomputable def Excision.topSES (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.ShortComplex (ChainComplex AddCommGrpCat ℕ)

The short exact sequence with A-chains, small chains, and their cokernel: 0 → C_*(A) → C^{\{A, B\}}_*(X) → C^{\{A, B\}}_*(X) / C_*(A) → 0. Used to compare with bottomSES via the excision SES morphism.

noncomputable def Excision.excisionSESMorphism (X : Type) [TopologicalSpace X] (A B : Set X) : topSES X A B ⟶ bottomSES X A

The morphism of short exact sequences from topSES X A B (small chains) to bottomSES X A (full chains), with identity on C_*(A), the small inclusion on the middle term, and the induced map on cokernels on the right.

theorem Excision.sigmaConst_map_mono_of_injective (J K : Type) (f : J → K) (hf : Function.Injective f) (R : AddCommGrpCat) : CategoryTheory.Mono ((CategoryTheory.Limits.sigmaConst.obj R).map (have this := f; this))

For a fixed abelian group R, the constant-coefficient J ↦ ⊕_J R functor sends injective functions to monomorphisms. (Split mono when J is nonempty; zero object when empty.)

instance Excision.toSSet_preservesMono : TopCat.toSSet.PreservesMonomorphisms

The total singular simplicial set functor TopCat ⥤ SSet preserves monomorphisms: an injective continuous map is sent to a degreewise-injective map of simplicial sets.

instance Excision.singularChainZ_preservesMono : singularChainZ.PreservesMonomorphisms

The singular chain functor C_*(-; ℤ) : TopCat ⥤ ChainComplex AddCommGrp preserves monomorphisms.

instance Excision.subspaceChainInclusion_mono (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (subspaceChainInclusion X A)

The chain inclusion C_*(A) ↪ C_*(X) induced by A ↪ X is a monomorphism.

instance Excision.smallChainInclusionA_mono (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.Mono (smallChainInclusionA X A B)

The map C_*(A) → C^{\{A, B\}}_*(X) is a monomorphism.

instance Excision.topSES_mono_f (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.Mono (topSES X A B).f

The first map in topSES X A B is a monomorphism.

instance Excision.topSES_epi_g (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.Epi (topSES X A B).g

The second map in topSES X A B is an epimorphism (as a cokernel projection).

theorem Excision.topSES_shortExact (X : Type) [TopologicalSpace X] (A B : Set X) : (topSES X A B).ShortExact

The short complex topSES X A B is short-exact.

instance Excision.bottomSES_mono_f (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (bottomSES X A).f

The first map in bottomSES X A is a monomorphism.

instance Excision.bottomSES_epi_g (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Epi (bottomSES X A).g

The second map in bottomSES X A is an epimorphism (as a cokernel projection).

theorem Excision.bottomSES_shortExact (X : Type) [TopologicalSpace X] (A : Set X) : (bottomSES X A).ShortExact

The short complex bottomSES X A is short-exact.

theorem Excision.thirdIso_shortExact {A B C : ChainComplex AddCommGrpCat ℕ} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Mono f] [CategoryTheory.Mono g] [CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f g)] : { X₁ := CategoryTheory.Limits.cokernel f, X₂ := CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g), X₃ := CategoryTheory.Limits.cokernel g, f := CategoryTheory.Limits.cokernel.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id A) g ⋯, g := CategoryTheory.Limits.cokernel.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id C) ⋯, zero := ⋯ }.ShortExact

Third isomorphism theorem (short-exact form). Given monomorphisms f : A ↪ B and g : B ↪ C with f ≫ g also mono (which is automatic), the sequence 0 → B / A → C / A → C / B → 0 is short-exact.

theorem Excision.secondIso_kernel_pullback_cond {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.biprod.desc φ ψ)) CategoryTheory.Limits.biprod.fst) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.biprod.desc φ ψ)) CategoryTheory.Limits.biprod.snd) ψ

Compatibility condition exhibiting the kernel of [φ, ψ] : 𝒜 ⊕ ℬ → 𝒳 as a span over 𝒳 via the negated first projection and the second projection. Auxiliary lemma for the abstract second isomorphism theorem.

theorem Excision.secondIso_fwd_cond {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd φ ψ) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ)) (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ)))))) = 0

Vanishing condition needed to factor the cokernel of pullback.snd through the cokernel of biprod.inl ∘ factorThruImage. Used in constructing the forward map of the abstract second isomorphism theorem.

theorem Excision.secondIso_kernel_kills_snd_cokernel {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.biprod.desc φ ψ)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.pullback.snd φ ψ))) = 0

Vanishing condition: the kernel of [φ, ψ] projected to the ℬ factor lands in the image of pullback.snd, hence its image in coker(pullback.snd) vanishes.

noncomputable def Excision.secondIso_coimToCokerPS {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.Abelian.coimage (CategoryTheory.Limits.biprod.desc φ ψ) ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.pullback.snd φ ψ)

The induced map coim([φ, ψ]) → coker(pullback.snd) from the coimage of the biproduct map to the cokernel of the pullback projection.

noncomputable def Excision.secondIso_imgToCokerPS {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.Limits.image (CategoryTheory.Limits.biprod.desc φ ψ) ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.pullback.snd φ ψ)

The induced map image([φ, ψ]) → coker(pullback.snd), obtained from secondIso_coimToCokerPS via the canonical iso image ≅ coimage in an abelian category.

theorem Excision.secondIso_inv_kills_inclA {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ))) (secondIso_imgToCokerPS φ ψ) = 0

Vanishing condition needed to descend secondIso_imgToCokerPS to a map out of the cokernel coker(biprod.inl ∘ factorThruImage).

noncomputable def Excision.secondIso_fwd {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.Limits.cokernel (CategoryTheory.Limits.pullback.snd φ ψ) ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ)))

Forward direction of the abstract second isomorphism: a map from coker(pullback.snd) to coker(biprod.inl ∘ factorThruImage), induced by the inclusion of ℬ into the biproduct.

noncomputable def Excision.secondIso_inv {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ))) ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.pullback.snd φ ψ)

Inverse direction of the abstract second isomorphism: the descent of secondIso_imgToCokerPS from the image to coker(biprod.inl ∘ factorThruImage).

theorem Excision.secondIso_fwd_inv_id {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.CategoryStruct.comp (secondIso_fwd φ ψ) (secondIso_inv φ ψ) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.cokernel (CategoryTheory.Limits.pullback.snd φ ψ))

The composition secondIso_fwd ≫ secondIso_inv is the identity. One half of the isomorphism claim.

theorem Excision.secondIso_inv_fwd_id {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.CategoryStruct.comp (secondIso_inv φ ψ) (secondIso_fwd φ ψ) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ))))

The composition secondIso_inv ≫ secondIso_fwd is the identity. The other half of the isomorphism claim.

noncomputable def Excision.secondIsoOfMorphisms {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Abelian 𝒞] {𝒜 ℬ 𝒳 : 𝒞} (φ : 𝒜 ⟶ 𝒳) (ψ : ℬ ⟶ 𝒳) : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc φ ψ))) ≅ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.pullback.snd φ ψ)

Abstract second isomorphism theorem. For morphisms φ : 𝒜 → 𝒳 and ψ : ℬ → 𝒳 in an abelian category, there is a canonical isomorphism $$(\mathcal{A} + \mathcal{B}) / \mathcal{A} \;\cong\; \mathcal{B} / (\mathcal{A} \cap \mathcal{B}),$$ where 𝒜 + ℬ is the image of [φ, ψ] : 𝒜 ⊕ ℬ → 𝒳 and 𝒜 ∩ ℬ is the pullback of φ along ψ.

noncomputable def Excision.secondIsomorphismIso_fwdMap (X : Type) [TopologicalSpace X] (A B : Set X) : smallChainComplex X A B ⟶ relativeSingularChainComplex (↑B) (Subtype.val ⁻¹' A)

The concrete forward map for the second isomorphism applied to chain complexes: C^{\{A, B\}}_*(X) → C_*(B, A ∩ B).

theorem Excision.secondIsomorphismIso_fwdMap_comp (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.CategoryStruct.comp (smallChainInclusionA X A B) (secondIsomorphismIso_fwdMap X A B) = 0

The forward map vanishes on C_*(A), so it descends to a map from the cokernel C^{\{A, B\}}_*(X) / C_*(A).

noncomputable def Excision.secondIsomorphismIso_invMap (X : Type) [TopologicalSpace X] (A B : Set X) : relativeSingularChainComplex (↑B) (Subtype.val ⁻¹' A) ⟶ CategoryTheory.Limits.cokernel (smallChainInclusionA X A B)

The concrete inverse map for the second isomorphism: C_*(B, A ∩ B) → C^{\{A, B\}}_*(X) / C_*(A).

theorem Excision.secondIsomorphismIso_hom_inv (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc (smallChainInclusionA X A B) (secondIsomorphismIso_fwdMap X A B) ⋯) (secondIsomorphismIso_invMap X A B) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.cokernel (smallChainInclusionA X A B))

Hom-inv identity for the second isomorphism isomorphism of chain complexes.

theorem Excision.secondIsomorphismIso_inv_hom (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.CategoryStruct.comp (secondIsomorphismIso_invMap X A B) (CategoryTheory.Limits.cokernel.desc (smallChainInclusionA X A B) (secondIsomorphismIso_fwdMap X A B) ⋯) = CategoryTheory.CategoryStruct.id (relativeSingularChainComplex (↑B) (Subtype.val ⁻¹' A))

Inv-hom identity for the second isomorphism isomorphism of chain complexes.

noncomputable def Excision.secondIsomorphismIso (X : Type) [TopologicalSpace X] (A B : Set X) : CategoryTheory.Limits.cokernel (smallChainInclusionA X A B) ≅ relativeSingularChainComplex (↑B) (Subtype.val ⁻¹' A)

Second isomorphism (concrete form for singular chains). The cokernel C^{\{A, B\}}_*(X) / C_*(A) is canonically isomorphic to the relative chain complex C_*(B, A ∩ B).

theorem Excision.secondIsomorphismIso_fwdMap_comp_excision (X : Type) [TopologicalSpace X] (A U : Set X) : CategoryTheory.CategoryStruct.comp (secondIsomorphismIso_fwdMap X A Uᶜ) (excisionRelativeChainMap X A U) = CategoryTheory.CategoryStruct.comp (smallChainInclusion X A Uᶜ) (CategoryTheory.Limits.cokernel.π (subspaceChainInclusion X A))

Compatibility between the second-isomorphism forward map and the excision chain map: both factor a chain in the small complex through the relative complex C_*(X, A).

theorem Excision.secondIsomorphismIso_hom_comp (X : Type) [TopologicalSpace X] (A U : Set X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (smallChainInclusionA X A Uᶜ)) (CategoryTheory.CategoryStruct.comp (secondIsomorphismIso X A Uᶜ).hom (excisionRelativeChainMap X A U)) = CategoryTheory.CategoryStruct.comp (smallChainInclusion X A Uᶜ) (CategoryTheory.Limits.cokernel.π (subspaceChainInclusion X A))

Pre-composition of secondIsomorphismIso_fwdMap_comp_excision with the cokernel projection, in the form needed to identify (excisionSESMorphism).τ₃ with the excision chain map.

theorem Excision.excisionSESMorphism_τ₃_comm (X : Type) [TopologicalSpace X] (A U : Set X) : (excisionSESMorphism X A Uᶜ).τ₃ = CategoryTheory.CategoryStruct.comp (secondIsomorphismIso X A Uᶜ).hom (CategoryTheory.CategoryStruct.comp (excisionRelativeChainMap X A U) (CategoryTheory.Iso.refl (relativeSingularChainComplex X A)).inv)

The right-most map τ₃ in the morphism of short exact sequences excisionSESMorphism agrees, up to the second-isomorphism identification, with the excision chain map.

theorem Excision.excisionRelativeChainMap_quasiIsoAt {X : Type} [TopologicalSpace X] {A U : Set X} (hexc : IsExcisive X A U) (n : ℕ) : QuasiIsoAt (excisionRelativeChainMap X A U) n

Pointwise version of the excision theorem at the chain level: for an excisive triple (X, A, U), the excision chain map is a quasi-isomorphism in every degree n.

theorem excision_theorem {X : Type} [TopologicalSpace X] {A U : Set X} (hexc : IsExcisive X A U) (n : ℕ) : CategoryTheory.IsIso (Excision.excisionHomologyMap X A U n)

Theorem 10.2 (Excision). Let (X, A, U) be an excisive triple, meaning closure U ⊆ interior A. Then for every n, the pair inclusion $$(X \setminus U,\; A \setminus U) \hookrightarrow (X, A)$$ induces an isomorphism on relative singular homology $$H_n(X \setminus U,\; A \setminus U;\, \mathbb{Z}) \;\xrightarrow{\sim}\; H_n(X, A;\, \mathbb{Z}).$$

Proved by passing to small chains via the locality principle and the second isomorphism.

def SphereHomology.Sphere (n : ℕ) : Type

The n-sphere S^n = \{x \in \mathbb{R}^{n+1} : \|x\| = 1\}.

@[implicit_reducible]

instance SphereHomology.Sphere.instTopologicalSpace (n : ℕ) : TopologicalSpace (Sphere n)

The subspace topology on Sphere n.

def SphereHomology.Disk (n : ℕ) : Type

The closed n-disk D^n = \{x \in \mathbb{R}^n : \|x\| \le 1\}.

@[implicit_reducible]

instance SphereHomology.Disk.instTopologicalSpace (n : ℕ) : TopologicalSpace (Disk n)

The subspace topology on Disk n.

def SphereHomology.DiskBoundary (n : ℕ) : Type

The boundary ∂D^n = S^{n-1} of the n-disk, as a stand-alone type.

def SphereHomology.diskBoundarySubset (n : ℕ) : Set (Disk n)

The boundary ∂D^n ⊆ D^n as a subset of the n-disk.

@[reducible, inline]

noncomputable abbrev SphereHomology.singularChainZF : CategoryTheory.Functor TopCat (ChainComplex AddCommGrpCat ℕ)

Local copy of singularChainZ in the SphereHomology namespace: the integer singular chain complex functor X ↦ C_*(X; ℤ).

theorem SphereHomology.sigmaConst_map_mono_of_injective' (J K : Type) (f : J → K) (hf : Function.Injective f) (R : AddCommGrpCat) : CategoryTheory.Mono ((CategoryTheory.Limits.sigmaConst.obj R).map (have this := f; this))

Local copy of sigmaConst_map_mono_of_injective in the SphereHomology namespace.

instance SphereHomology.toSSet_preservesMono' : TopCat.toSSet.PreservesMonomorphisms

Local copy of toSSet_preservesMono in the SphereHomology namespace.

instance SphereHomology.singularChainZ_preserves_mono : singularChainZF.PreservesMonomorphisms

The singularChainZF functor preserves monomorphisms.

noncomputable def SphereHomology.inclChain (X : Type) [TopologicalSpace X] (A : Set X) : singularChainZF.obj (TopCat.of ↑A) ⟶ singularChainZF.obj (TopCat.of X)

The chain-level inclusion C_*(A) → C_*(X) for a subspace A ⊆ X (local copy of subspaceChainInclusion in the SphereHomology namespace).

instance SphereHomology.inclTopMono {X : Type} [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })

The topological inclusion A ↪ X is a monomorphism in TopCat.

instance SphereHomology.inclChainMono (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (inclChain X A)

The chain-level inclusion inclChain is a monomorphism.

noncomputable def SphereHomology.pairSES (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.ShortComplex (ChainComplex AddCommGrpCat ℕ)

The pair short exact sequence 0 → C_*(A) → C_*(X) → C_*(X)/C_*(A) → 0.

instance SphereHomology.pairSES_f_mono (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (pairSES X A).f

The left map of the pair short exact sequence is a monomorphism.

instance SphereHomology.pairSES_g_epi (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Epi (pairSES X A).g

The right map of the pair short exact sequence is an epimorphism.

def SphereHomology.pairSES_shortExact (X : Type) [TopologicalSpace X] (A : Set X) : (pairSES X A).ShortExact

The pair sequence is short exact.

noncomputable def SphereHomology.pairδIso (X : Type) [TopologicalSpace X] (A : Set X) (q : ℕ) (hi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (pairSES X A).X₂ (q + 1))) (hj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (pairSES X A).X₂ q)) : HomologicalComplex.homology (pairSES X A).X₃ (q + 1) ≅ HomologicalComplex.homology (pairSES X A).X₁ q

The boundary-map isomorphism in the pair long exact sequence under vanishing of the homology of C_*(X) in two adjacent degrees: H_{q+1}(X, A) ≅ H_q(A).

theorem SphereHomology.isZero_SHG_contractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] (k : ℕ) (hk : k ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (singularChainZF.obj (TopCat.of X)) k)

The homology H_k(X; ℤ) of a contractible space X vanishes for k ≠ 0.

noncomputable def SphereHomology.bdryToSphereIso (n : ℕ) : TopCat.of ↑(diskBoundarySubset (n + 2)) ≅ TopCat.of (Sphere (n + 1))

The natural identification ∂D^{n+2} ≅ S^{n+1} between the boundary subspace and the sphere of the appropriate dimension, as objects of TopCat.

theorem SphereHomology.sphere_homology_top_aux (n : ℕ) (hn : n > 0) : Nonempty (HomologicalComplex.homology (singularChainZF.obj (TopCat.of (Sphere n))) n ≅ AddCommGrpCat.of ℤ)

Auxiliary form of sphere_homology_top: the top homology of S^n is ℤ, expressed in terms of the singularChainZF complex.

theorem SphereHomology.relative_homology_base : Nonempty (Excision.RelativeSingularHomologyGroup 1 (Disk 1) (diskBoundarySubset 1) ≅ AddCommGrpCat.of ℤ)

Base case for the relative homology of the disk pair: H_1(D^1, S^0) ≅ ℤ.

theorem SphereHomology.relative_homology_top (n : ℕ) (hn : n > 0) : Nonempty (Excision.RelativeSingularHomologyGroup n (Disk n) (diskBoundarySubset n) ≅ AddCommGrpCat.of ℤ)

Top relative homology of the disk pair (part of Proposition 10.4): H_n(D^n, S^{n-1}) ≅ ℤ for n > 0.

theorem SphereHomology.relative_homology_vanishing (q n : ℕ) (hn : n > 0) (hqn : q ≠ n) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup q (Disk n) (diskBoundarySubset n))

Vanishing of off-degree relative homology (part of Proposition 10.4): H_q(D^n, S^{n-1}) = 0 for q ≠ n.

instance SphereHomology.suspSingularChainZ_preserves_mono : ((AlgebraicTopology.singularChainComplexFunctor AddCommGrpCat).obj (AddCommGrpCat.of ℤ)).PreservesMonomorphisms

The singular chain functor used in the suspension-isomorphism proof preserves monomorphisms.

@[reducible, inline]

noncomputable abbrev SphereHomology.suspSingularChainZF : CategoryTheory.Functor TopCat (ChainComplex AddCommGrpCat ℕ)

Local copy of singularChainZF in the suspension-isomorphism proof.

noncomputable def SphereHomology.suspInclChain (X : Type) [TopologicalSpace X] (A : Set X) : suspSingularChainZF.obj (TopCat.of ↑A) ⟶ suspSingularChainZF.obj (TopCat.of X)

Local copy of inclChain for the suspension-isomorphism proof.

instance SphereHomology.suspInclTopMono {X : Type} [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })

Local copy of inclTopMono for the suspension-isomorphism proof.

instance SphereHomology.suspInclChainMono (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (suspInclChain X A)

Local copy of inclChainMono for the suspension-isomorphism proof.

noncomputable def SphereHomology.suspPairSES (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.ShortComplex (ChainComplex AddCommGrpCat ℕ)

Local copy of pairSES for the suspension-isomorphism proof.

instance SphereHomology.suspPairSES_f_mono (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Mono (suspPairSES X A).f

Local copy of pairSES_f_mono for the suspension-isomorphism proof.

instance SphereHomology.suspPairSES_g_epi (X : Type) [TopologicalSpace X] (A : Set X) : CategoryTheory.Epi (suspPairSES X A).g

Local copy of pairSES_g_epi for the suspension-isomorphism proof.

def SphereHomology.suspPairSES_shortExact (X : Type) [TopologicalSpace X] (A : Set X) : (suspPairSES X A).ShortExact

Local copy of pairSES_shortExact for the suspension-isomorphism proof.

noncomputable def SphereHomology.suspPairδIso (X : Type) [TopologicalSpace X] (A : Set X) (q : ℕ) (hi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (suspPairSES X A).X₂ (q + 1))) (hj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (suspPairSES X A).X₂ q)) : HomologicalComplex.homology (suspPairSES X A).X₃ (q + 1) ≅ HomologicalComplex.homology (suspPairSES X A).X₁ q

Local copy of pairδIso for the suspension-isomorphism proof.

theorem SphereHomology.suspIsZero_SHG_contractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] (k : ℕ) (hk : k ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (suspSingularChainZF.obj (TopCat.of X)) k)

Local copy of isZero_SHG_contractible for the suspension-isomorphism proof.

noncomputable def SphereHomology.suspBdryToSphereIso (n : ℕ) : TopCat.of ↑(diskBoundarySubset (n + 1)) ≅ TopCat.of (Sphere n)

Local copy of bdryToSphereIso: the identification ∂D^{n+1} ≅ S^n.

theorem SphereHomology.suspension_homology_iso (n q : ℕ) (hq : q ≥ 1) : Nonempty (AlgebraicTopologyI.SingularHomologyGroup q (Sphere n) ≅ AlgebraicTopologyI.SingularHomologyGroup (q + 1) (Sphere (n + 1)))

Suspension isomorphism for sphere homology. For q ≥ 1, there is an isomorphism H_q(S^n) ≅ H_{q+1}(S^{n+1}), obtained by chasing the pair long exact sequences of (D^{n+1}, S^n) and (D^{n+2}, S^{n+1}) together with the known relative homology of the disk pair.

instance SphereHomology.sphere_zero_finite : Finite (Sphere 0)

S^0 is finite (it is just the two-point set {-1, +1}).

instance SphereHomology.sphere_zero_totallyDisconnected : TotallyDisconnectedSpace (Sphere 0)

S^0 is totally disconnected (discrete two-point space).

theorem SphereHomology.sphere_zero_homology_vanishing (q : ℕ) (hq : q > 0) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q (Sphere 0))

For q > 0, the singular homology of S^0 vanishes: H_q(S^0) = 0.

theorem SphereHomology.sphere_zero_homology_zero : Nonempty (AlgebraicTopologyI.SingularHomologyGroup 0 (Sphere 0) ≅ AddCommGrpCat.of (ℤ × ℤ))

Zeroth homology of S^0. Since S^0 has two path components, H_0(S^0) ≅ ℤ ⊕ ℤ.

structure SphereHomology.SphereAndDiskHomology : Prop

Proposition 10.4 (packaged). The singular homology of spheres and the relative homology of disk pairs: H_n(S^n) = ℤ, H_0(S^n) = ℤ for n > 0, H_0(S^0) = ℤ ⊕ ℤ, otherwise zero; and H_n(D^n, S^{n-1}) = ℤ, otherwise zero.

• sphere_top (n : ℕ) : n > 0 → Nonempty (AlgebraicTopologyI.SingularHomologyGroup n (Sphere n) ≅ AddCommGrpCat.of ℤ)
• sphere_zero (n : ℕ) : n > 0 → Nonempty (AlgebraicTopologyI.SingularHomologyGroup 0 (Sphere n) ≅ AddCommGrpCat.of ℤ)
• sphere_zero_zero : Nonempty (AlgebraicTopologyI.SingularHomologyGroup 0 (Sphere 0) ≅ AddCommGrpCat.of (ℤ × ℤ))
• sphere_vanishing (q n : ℕ) : n > 0 → q ≠ 0 → q ≠ n → CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q (Sphere n))
• sphere_zero_vanishing (q : ℕ) : q > 0 → CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q (Sphere 0))
• relative_top (n : ℕ) : n > 0 → Nonempty (Excision.RelativeSingularHomologyGroup n (Disk n) (diskBoundarySubset n) ≅ AddCommGrpCat.of ℤ)
• relative_vanishing (q n : ℕ) : n > 0 → q ≠ n → CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup q (Disk n) (diskBoundarySubset n))

theorem SphereHomology.sphere_homology_top (n : ℕ) (hn : n > 0) : Nonempty (AlgebraicTopologyI.SingularHomologyGroup n (Sphere n) ≅ AddCommGrpCat.of ℤ)

Top homology of the sphere. H_n(S^n) ≅ ℤ for n > 0.

theorem SphereHomology.suspension_vanishing_step (q n : ℕ) (hq : q ≥ 1) (h : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q (Sphere n))) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup (q + 1) (Sphere (n + 1)))

Inductive step for sphere-homology vanishing: if H_q(S^n) = 0 for q ≥ 1, then H_{q+1}(S^{n+1}) = 0.

theorem SphereHomology.sphere_h1_vanishing (n : ℕ) (hn : n ≥ 2) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup 1 (Sphere n))

For n ≥ 2, the first homology of the sphere vanishes: H_1(S^n) = 0.

theorem SphereHomology.sphere_homology_vanishing (q n : ℕ) (hn : n > 0) (hq0 : q ≠ 0) (hqn : q ≠ n) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q (Sphere n))

Off-degree vanishing of sphere homology. For n > 0, 0 < q ≠ n, we have H_q(S^n) = 0. The proof is a two-variable induction on q + n, combining sphere_h1_vanishing, sphere_zero_homology_vanishing, and suspension_vanishing_step.

theorem SphereHomology.sphere_homology_zero (n : ℕ) (hn : n > 0) : Nonempty (AlgebraicTopologyI.SingularHomologyGroup 0 (Sphere n) ≅ AddCommGrpCat.of ℤ)

Zeroth homology of S^n for n > 0: H_0(S^n) ≅ ℤ (the sphere is path connected).

theorem SphereHomology.sphereAndDiskHomology : SphereAndDiskHomology

Proposition 10.4 (final form). All the sphere/disk-pair homology computations packaged into a single SphereAndDiskHomology record.

noncomputable def SphereHomology.homotopyEquiv_singularHomologyIso {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) (q : ℕ) : AlgebraicTopologyI.SingularHomologyGroup q X ≅ AlgebraicTopologyI.SingularHomologyGroup q Y

A homotopy equivalence X ≃ₕ Y induces an isomorphism H_q(X; ℤ) ≅ H_q(Y; ℤ) on singular homology for every q.

theorem SphereHomology.addCommGrpCat_int_not_isZero : ¬CategoryTheory.Limits.IsZero (AddCommGrpCat.of ℤ)

The group ℤ is not a zero object in AddCommGrpCat.

theorem SphereHomology.sphere_not_homotopy_equiv (m n : ℕ) (hmn : m ≠ n) : IsEmpty (ContinuousMap.HomotopyEquiv (Sphere m) (Sphere n))

Corollary 10.5. If m ≠ n, then S^m and S^n are not homotopy equivalent.

theorem SphereHomology.punctured_euclidean_homotopyEquiv_sphere (n : ℕ) : Nonempty (ContinuousMap.HomotopyEquiv ↑{x : EuclideanSpace ℝ (Fin (n + 1)) | x ≠ 0} ↑(Metric.sphere 0 1))

The punctured Euclidean space ℝ^{n+1} ∖ {0} is homotopy equivalent to the unit sphere S^n ⊆ ℝ^{n+1}, via the radial deformation retraction x ↦ x/‖x‖.

def SphereHomology.homeomorphSubtypeNe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (x : X) : ↑{y : X | y ≠ x} ≃ₜ ↑{z : Y | z ≠ f x}

A homeomorphism f : X ≃ₜ Y restricts to a homeomorphism {x | x ≠ p} ≃ₜ {y | y ≠ f p} between punctured spaces.

def SphereHomology.puncturedTranslateHomeomorph {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (p : G) : ↑{x : G | x ≠ p} ≃ₜ ↑{y : G | y ≠ 0}

Translation by -p gives a homeomorphism {x | x ≠ p} ≃ₜ {y | y ≠ 0}.

theorem SphereHomology.euclidean_not_homeomorph (m n : ℕ) (hmn : m ≠ n) : IsEmpty (EuclideanSpace ℝ (Fin m) ≃ₜ EuclideanSpace ℝ (Fin n))

Corollary 10.6 (Invariance of dimension). If m ≠ n, then ℝ^m and ℝ^n are not homeomorphic. The proof punctures the spaces, applies the homotopy equivalence ℝ^{n+1} ∖ {0} ≃ₕ S^n, and uses that spheres of different dimensions are not homotopy equivalent.

@[reducible, inline]

abbrev BrouwerFixedPoint.Disk (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

Local abbreviation for the closed unit disk D^n ⊆ ℝ^n in the Brouwer fixed-point section.

@[reducible, inline]

abbrev BrouwerFixedPoint.Sphere (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

Local abbreviation for the unit sphere S^{n-1} ⊆ ℝ^n in the Brouwer fixed-point section.

structure BrouwerFixedPoint.IsRetraction (n : ℕ) (r : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) : Prop

A retraction of D^n onto S^{n-1}: a continuous map r : ℝ^n → ℝ^n sending the disk to the sphere and fixing the boundary. Brouwer's theorem amounts to ruling out such retractions.

• continuous_r : Continuous r
• maps_to (x : EuclideanSpace ℝ (Fin n)) : x ∈ Disk n → r x ∈ Sphere n
• fixes_boundary (x : EuclideanSpace ℝ (Fin n)) : x ∈ Sphere n → r x = x

@[reducible, inline]

noncomputable abbrev BrouwerFixedPoint.homFunctorZ (k : ℕ) : CategoryTheory.Functor TopCat AddCommGrpCat

The functor H_k(−; ℤ) : TopCat → AddCommGrpCat, packaged for use in the Brouwer proof.

theorem BrouwerFixedPoint.isZero_homology_of_contractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] (k : ℕ) (hk : k ≠ 0) : CategoryTheory.Limits.IsZero ((homFunctorZ k).obj (TopCat.of X))

The singular homology of a contractible space vanishes in positive degree.

noncomputable def BrouwerFixedPoint.sphereInclusion (n : ℕ) : TopCat.of ↑(Sphere n) ⟶ TopCat.of ↑(Disk n)

The inclusion S^{n-1} ↪ D^n of the boundary sphere into the disk, as a morphism of TopCat.

noncomputable def BrouwerFixedPoint.diskRetraction (n : ℕ) (r : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hr : IsRetraction n r) : TopCat.of ↑(Disk n) ⟶ TopCat.of ↑(Sphere n)

A retraction r : ℝ^n → ℝ^n of D^n onto S^{n-1} packaged as a TopCat morphism D^n ⟶ S^{n-1}.

theorem BrouwerFixedPoint.sphereInclusion_diskRetraction (n : ℕ) (r : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hr : IsRetraction n r) : CategoryTheory.CategoryStruct.comp (sphereInclusion n) (diskRetraction n r hr) = CategoryTheory.CategoryStruct.id (TopCat.of ↑(Sphere n))

A retraction satisfies (sphereInclusion) ≫ (diskRetraction r) = id, the categorical definition of r being a retraction.

theorem BrouwerFixedPoint.not_isZero_of_nontrivial (G : Type u_1) [AddCommGroup G] [Nontrivial G] : ¬CategoryTheory.Limits.IsZero (AddCommGrpCat.of G)

A nontrivial abelian group is not zero in AddCommGrpCat.

noncomputable def BrouwerFixedPoint.coordProj : EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ

The projection ℝ^1 → ℝ onto the (only) coordinate, as a continuous linear map.

theorem BrouwerFixedPoint.norm_fin1_eq_abs_coord (x : EuclideanSpace ℝ (Fin 1)) : ‖x‖ = |coordProj x|

In ℝ^1, the Euclidean norm equals the absolute value of the unique coordinate.

theorem BrouwerFixedPoint.no_retraction_dim_one (r : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)) (hr : IsRetraction 1 r) : False

No retraction D^1 → S^0 (base case for Brouwer). The interval [-1, 1] is connected but S^0 = {-1, +1} is not, so the intermediate-value theorem rules out a continuous retraction.

theorem BrouwerFixedPoint.no_retraction_higher (m : ℕ) (hm : 0 < m) (r : EuclideanSpace ℝ (Fin (m + 1)) → EuclideanSpace ℝ (Fin (m + 1))) (hr : IsRetraction (m + 1) r) : False

No retraction D^{m+1} → S^m for m ≥ 1 (inductive step for Brouwer). If such a retraction existed, then H_m(S^m) ≅ ℤ would be a retract of H_m(D^{m+1}) = 0, contradiction.

theorem BrouwerFixedPoint.no_retraction_disk_to_sphere (n : ℕ) (hn : 0 < n) (r : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hr : IsRetraction n r) : False

No retraction D^n → S^{n-1} for any n ≥ 1. Combines no_retraction_dim_one (for n = 1) and no_retraction_higher (for n ≥ 2). This is the key topological input to Brouwer's fixed-point theorem.

noncomputable def BrouwerFixedPoint.rayDiscrim {n : ℕ} (a v : EuclideanSpace ℝ (Fin n)) : ℝ

Discriminant of the quadratic equation ‖a + t v‖ = 1 in t, used in the geometric construction of a retraction from a fixed-point-free self-map of D^n.

noncomputable def BrouwerFixedPoint.rayParam {n : ℕ} (a v : EuclideanSpace ℝ (Fin n)) : ℝ

The positive root t = (−⟨a,v⟩ + √Δ) / ‖v‖² of the equation ‖a + t v‖ = 1, where Δ = rayDiscrim a v. Geometrically: the parameter at which the ray t ↦ a + t v (with t ≥ 0) hits the unit sphere.

noncomputable def BrouwerFixedPoint.retractionMap {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin n)

Geometric retraction associated to a fixed-point-free self-map f of D^n: from each point x, follow the ray from f x through x until it hits the boundary sphere.

noncomputable def BrouwerFixedPoint.projBall {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin n)

Radial projection of ℝ^n onto the closed unit ball: x ↦ x / max(1, ‖x‖).

theorem BrouwerFixedPoint.projBall_continuous (n : ℕ) : Continuous projBall

The radial projection projBall is continuous.

theorem BrouwerFixedPoint.projBall_mem_disk (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : projBall x ∈ Disk n

projBall x lies in the closed unit disk.

theorem BrouwerFixedPoint.projBall_eq_of_mem_disk (n : ℕ) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ Disk n) : projBall x = x

For x already in the unit disk, projBall x = x.

theorem BrouwerFixedPoint.quadratic_ray_root (c β s α : ℝ) (hc : c ≠ 0) (hs : s ^ 2 = β ^ 2 + c * (1 - α)) : c * ((-β + s) / c) ^ 2 + 2 * β * ((-β + s) / c) + α = 1

Algebraic identity: the positive root of the quadratic c t² + 2 β t + (α - 1) = 0 yields c t² + 2 β t + α = 1. Used to verify that rayParam solves ‖a + t v‖ = 1.

theorem BrouwerFixedPoint.retractionMap_norm_eq_one {n : ℕ} {a v : EuclideanSpace ℝ (Fin n)} (ha : ‖a‖ ≤ 1) (hv : v ≠ 0) : ‖a + rayParam a v • v‖ = 1

For ‖a‖ ≤ 1 and v ≠ 0, the point a + rayParam a v • v has unit norm: the ray from a in direction v hits the unit sphere exactly at this parameter.

theorem BrouwerFixedPoint.rayParam_eq_one_of_norm_one {n : ℕ} {a x : EuclideanSpace ℝ (Fin n)} (ha : ‖a‖ ≤ 1) (hx : ‖x‖ = 1) (hne : a ≠ x) : rayParam a (x - a) = 1

If x is already on the unit sphere (and a ≠ x with ‖a‖ ≤ 1), then the ray from a through x hits the sphere exactly at x, i.e. rayParam a (x - a) = 1.

theorem BrouwerFixedPoint.retraction_of_fixed_point_free (n : ℕ) (_hn : 0 < n) (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hf_cont : Continuous f) (hf_maps : ∀ x ∈ Disk n, f x ∈ Disk n) (hf_no_fp : ∀ x ∈ Disk n, f x ≠ x) : ∃ (r : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)), IsRetraction n r

From a fixed-point-free self-map to a retraction. Given a continuous self-map of the disk with no fixed point, the geometric construction retractionMap produces a continuous retraction of the disk onto its boundary sphere. This is the standard reduction of Brouwer's theorem to the non-existence of such a retraction.

theorem BrouwerFixedPoint.brouwer_fixed_point (n : ℕ) (hn : 0 < n) (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hf_cont : Continuous f) (hf_maps : ∀ x ∈ Disk n, f x ∈ Disk n) : ∃ x ∈ Disk n, f x = x

Theorem 10.7 (Brouwer fixed-point theorem). Every continuous self-map f : D^n → D^n of the closed unit disk in ℝ^n (for n ≥ 1) has a fixed point. The proof: a fixed-point-free f would yield a retraction D^n → S^{n-1}, contradicting no_retraction_disk_to_sphere.

def ExcisionApplications.IsSubspaceDeformationRetract {X : Type u} [TopologicalSpace X] (A B : Set X) : Prop

A subset A ⊆ B is a deformation retract within B if A ⊆ B and there exists a deformation retraction of B onto A (viewed as a subset of B). Hypothesis of Corollary 10.3.

def ExcisionApplications.collapseSetoid {X : Type u} [TopologicalSpace X] (A : Set X) : Setoid X

The equivalence relation on X that collapses the subset A to a single point: two points are related iff they are equal, or both lie in A. Used to form the quotient X / A.

def ExcisionApplications.QuotientSpace (X : Type u) [TopologicalSpace X] (A : Set X) : Type u

The quotient space X / A: the set of equivalence classes of collapseSetoid A, with the quotient topology.

@[implicit_reducible]

instance ExcisionApplications.instTopologicalSpaceQuotientSpace {X : Type u} [TopologicalSpace X] (A : Set X) : TopologicalSpace (QuotientSpace X A)

The quotient topology on QuotientSpace X A.

def ExcisionApplications.quotientBasepoint {X : Type u} [TopologicalSpace X] (A : Set X) {a : X} : a ∈ A → QuotientSpace X A

The basepoint of X / A: the image in QuotientSpace X A of any point a ∈ A.

def ExcisionApplications.quotientPair {X : Type u} [TopologicalSpace X] (A : Set X) {a : X} (ha : a ∈ A) : EilenbergSteenrod.TopPair

The pointed pair (X / A, [a]) where [a] is the collapsed image of A.

def ExcisionApplications.collapseMapOfPairs {X : Type u} [TopologicalSpace X] (A : Set X) {a : X} (ha : a ∈ A) : EilenbergSteenrod.MapOfPairs { space := X, instTop := inferInstance, sub := A } (quotientPair A ha)

The quotient map of pairs (X, A) → (X/A, *) sending each point to its equivalence class.

def ExcisionApplications.subspacePair {X : Type u} [TopologicalSpace X] (A B : Set X) : EilenbergSteenrod.TopPair

The pair (B, A ∩ B) viewed inside B via the subtype inclusion ↥B ↪ X.

def ExcisionApplications.pairInclusion {X : Type u} [TopologicalSpace X] (A B : Set X) : EilenbergSteenrod.MapOfPairs (subspacePair A B) { space := X, instTop := inferInstance, sub := A }

The pair map (B, A ∩ B) → (X, A) given by the subtype inclusion ↥B ↪ X.

theorem ExcisionApplications.mapOfPairs_ext {P : EilenbergSteenrod.TopPair} {Q : EilenbergSteenrod.TopPair} {f g : EilenbergSteenrod.MapOfPairs P Q} (h : f.toFun = g.toFun) : f = g

Two maps of pairs are equal iff their underlying continuous maps are equal.

def ExcisionApplications.subspacePairToExcisePair {X : Type u} [TopologicalSpace X] (A B : Set X) : EilenbergSteenrod.MapOfPairs (subspacePair A B) ({ space := X, instTop := inferInstance, sub := A }.excisePair Bᶜ)

Identification of (B, A ∩ B) with the excised pair (X ∖ Bᶜ, A ∖ Bᶜ) in the forward direction.

def ExcisionApplications.excisePairToSubspacePair {X : Type u} [TopologicalSpace X] (A B : Set X) : EilenbergSteenrod.MapOfPairs ({ space := X, instTop := inferInstance, sub := A }.excisePair Bᶜ) (subspacePair A B)

Identification of the excised pair (X ∖ Bᶜ, A ∖ Bᶜ) with (B, A ∩ B) in the reverse direction. Inverse to subspacePairToExcisePair.

theorem ExcisionApplications.excisionInclusion_comp_subspacePairToExcisePair {X : Type u} [TopologicalSpace X] (A B : Set X) : (EilenbergSteenrod.excisionInclusion { space := X, instTop := inferInstance, sub := A } Bᶜ).comp (subspacePairToExcisePair A B) = pairInclusion A B

The excision inclusion composed with the identification (B, A ∩ B) ≅ (X ∖ Bᶜ, A ∖ Bᶜ) recovers the pair inclusion (B, A ∩ B) → (X, A).

theorem ExcisionApplications.roundTrip_subspacePair {X : Type u} [TopologicalSpace X] (A B : Set X) : (excisePairToSubspacePair A B).comp (subspacePairToExcisePair A B) = EilenbergSteenrod.MapOfPairs.id (subspacePair A B)

One direction of the inverse pair: excisePairToSubspacePair ∘ subspacePairToExcisePair = id.

theorem ExcisionApplications.roundTrip_excisePair {X : Type u} [TopologicalSpace X] (A B : Set X) : (subspacePairToExcisePair A B).comp (excisePairToSubspacePair A B) = EilenbergSteenrod.MapOfPairs.id ({ space := X, instTop := inferInstance, sub := A }.excisePair Bᶜ)

The other direction of the inverse pair: subspacePairToExcisePair ∘ excisePairToSubspacePair = id.

def ExcisionApplications.collapseFactorization {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) {a : X} (ha : a ∈ A) (_hClosure : closure A ⊆ interior B) (_hDR : IsSubspaceDeformationRetract A B) : h.H n (subspacePair A B) →+ h.H n (quotientPair A ha)

The homology map H_n(B, A ∩ B) → H_n(X/A, *) induced by the composition "include into (X, A) then collapse A". This is the factorization used to deduce that the collapse map induces an isomorphism on homology (Corollary 10.3).

theorem ExcisionApplications.subsingleton_relative_of_inclusionBijective (h : EilenbergSteenrod.HomologyTheory) (P : EilenbergSteenrod.TopPair) (hbij : ∀ (m : ℤ), Function.Bijective ⇑(h.map m (EilenbergSteenrod.inclusionSubToSpace P))) (n : ℤ) : Subsingleton (h.H (n + 1) P)

If the inclusion A ↪ X of a pair P = (X, A) induces a bijection on H_m for every m, then the relative homology H_{n+1}(X, A) is trivial. Used to deduce relative-homology vanishing from absolute-homology equivalence via the long exact sequence.

theorem ExcisionApplications.subsingleton_relative_of_inclusionBijective' (h : EilenbergSteenrod.HomologyTheory) (P : EilenbergSteenrod.TopPair) (hbij : ∀ (m : ℤ), Function.Bijective ⇑(h.map m (EilenbergSteenrod.inclusionSubToSpace P))) (m : ℤ) : Subsingleton (h.H m P)

Reindexed version of subsingleton_relative_of_inclusionBijective: the relative homology H_m(X, A) vanishes in every degree m when the inclusion A ↪ X is a homology equivalence.

theorem ExcisionApplications.inclusionSubToSpace_bijective_of_DR (h : EilenbergSteenrod.HomologyTheory) (m : ℤ) {Y : Type u} [TopologicalSpace Y] (S : Set Y) (hdr : Nonempty (DeformationRetract.IsDeformationRetract S)) : Function.Bijective ⇑(h.map m (EilenbergSteenrod.inclusionSubToSpace { space := Y, instTop := inferInstance, sub := S }))

If S ⊆ Y is a deformation retract of Y, then the inclusion S ↪ Y induces an isomorphism on homology in every degree (homotopy invariance applied to the retraction).

theorem ExcisionApplications.quotientSpace_inclusionBijective_of_DR (h : EilenbergSteenrod.HomologyTheory) (m : ℤ) {Y : Type u} [TopologicalSpace Y] (S : Set Y) (hdr : Nonempty (DeformationRetract.IsDeformationRetract S)) {s : Y} (hs : s ∈ S) : Function.Bijective ⇑(h.map m (EilenbergSteenrod.inclusionSubToSpace (quotientPair S hs)))

The image [S] of a deformation retract S ⊆ Y becomes a single point in the quotient Y / S, and the inclusion {[S]} ↪ Y / S is a homology equivalence.

theorem ExcisionApplications.collapseSubspaceMap_bijective {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) {a : X} (ha : a ∈ A) (hAB : A ⊆ B) (hDR : IsSubspaceDeformationRetract A B) : Function.Bijective ⇑(h.map n (collapseMapOfPairs (Subtype.val ⁻¹' A) ha))

Bijectivity of the collapse map on relative homology inside B: when A is a deformation retract of B, the map of pairs (B, A) → (B/A, *) induces an isomorphism on homology (a key ingredient in the proof of Corollary 10.3).

theorem ExcisionApplications.quotientInclusionMap_bijective {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) {a : X} (ha : a ∈ A) (hAB : A ⊆ B) (hClosure : closure A ⊆ interior B) : ∃ (f : EilenbergSteenrod.MapOfPairs (quotientPair (Subtype.val ⁻¹' A) ha) (quotientPair A ha)), (∀ (b : ↑B), f.toFun ⟦b⟧ = ⟦↑b⟧) ∧ Function.Bijective ⇑(h.map n f)

Under the excision hypothesis closure A ⊆ interior B, the inclusion B/A ↪ X/A between quotient spaces is induced by a well-defined map of pairs, and this map is a homology isomorphism.

theorem ExcisionApplications.collapseFactorization_bijective {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) {a : X} (ha : a ∈ A) (hClosure : closure A ⊆ interior B) (hDR : IsSubspaceDeformationRetract A B) : Function.Bijective ⇑(collapseFactorization h n A B ha hClosure hDR)

The composite map H_n(B, A ∩ B) → H_n(X/A, *) (collapse map composed with pair inclusion) is bijective under the excision and deformation-retract hypotheses. Combines quotientInclusionMap_bijective with collapseSubspaceMap_bijective.

theorem ExcisionApplications.pairInclusion_homologyMap_bijective_of_closure {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) (hClosure : closure A ⊆ interior B) (hAB : A ⊆ B) : Function.Bijective ⇑(h.map n (pairInclusion A B))

Excision in subspace form: when closure A ⊆ interior B, the pair inclusion (B, A ∩ B) → (X, A) induces an isomorphism on homology in every degree. Obtained by transporting the excision theorem along the identification (B, A ∩ B) ≅ (X ∖ Bᶜ, A ∖ Bᶜ).

theorem ExcisionApplications.collapseMapOfPairs_homologyMap_bijective_of_DR {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) {a : X} (ha : a ∈ A) (hClosure : closure A ⊆ interior B) (hDR : IsSubspaceDeformationRetract A B) : Function.Bijective ⇑(h.map n (collapseMapOfPairs A ha))

The collapse map of pairs (X, A) → (X/A, *) is a homology isomorphism whenever A is contained in a larger subset B such that closure A ⊆ interior B and A is a deformation retract of B. This is the technical heart of Corollary 10.3.

theorem ExcisionApplications.collapseMapOfPairs_homologyMap_bijective {X : Type u} [TopologicalSpace X] (h : EilenbergSteenrod.HomologyTheory) (n : ℤ) (A B : Set X) {a : X} (ha : a ∈ A) (hClosure : closure A ⊆ interior B) (hDR : IsSubspaceDeformationRetract A B) : Function.Bijective ⇑(h.map n (collapseMapOfPairs A ha))

Corollary 10.3 (Quotient–pair excision). If A ⊆ X admits a neighbourhood B such that closure A ⊆ interior B and A is a deformation retract of B, then the quotient map of pairs (X, A) → (X/A, *) induces an isomorphism on homology in every degree.

Concretely, this lets one compute the homology of a quotient X / A (with * the collapsed point) in terms of the relative homology H_n(X, A).

@[reducible, inline]

noncomputable abbrev DegreeTheory.homologyFunctorZ (n : ℕ) : CategoryTheory.Functor TopCat AddCommGrpCat

The functor Top ⥤ AddCommGrp sending a space X to its n-th singular homology group $H_n(X; \mathbb{Z})$ with integer coefficients.

theorem DegreeTheory.addCommGrpCat_endZ_apply (f : AddCommGrpCat.of ℤ ⟶ AddCommGrpCat.of ℤ) (x : ℤ) : (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) 1 * x

Any endomorphism f : ℤ ⟶ ℤ in AddCommGrp is multiplication by f 1.

def DegreeTheory.degreeOfEndo {G : AddCommGrpCat} (φ : G ≅ AddCommGrpCat.of ℤ) (e : G ⟶ G) : ℤ

The degree of an endomorphism e : G ⟶ G of an abelian group G ≅ ℤ: transport e along the chosen isomorphism φ : G ≅ ℤ and evaluate at 1.

theorem DegreeTheory.degreeOfEndo_comp {G : AddCommGrpCat} (φ : G ≅ AddCommGrpCat.of ℤ) (e₁ e₂ : G ⟶ G) : degreeOfEndo φ (CategoryTheory.CategoryStruct.comp e₁ e₂) = degreeOfEndo φ e₁ * degreeOfEndo φ e₂

Multiplicativity of degree: deg(e₁ ∘ e₂) = deg(e₁) · deg(e₂).

theorem DegreeTheory.degreeOfEndo_id {G : AddCommGrpCat} (φ : G ≅ AddCommGrpCat.of ℤ) : degreeOfEndo φ (CategoryTheory.CategoryStruct.id G) = 1

The degree of the identity endomorphism is 1.

theorem DegreeTheory.degreeOfEndo_eq_smul {G : AddCommGrpCat} (φ : G ≅ AddCommGrpCat.of ℤ) (e : G ⟶ G) (x : ℤ) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp φ.inv (CategoryTheory.CategoryStruct.comp e φ.hom))) x = degreeOfEndo φ e * x

Under the identification G ≅ ℤ, the transported endomorphism acts as multiplication by the degree of e.

def DegreeTheory.selfMapSetoid (S : TopCat) : Setoid (S ⟶ S)

The homotopy equivalence relation on self-maps of S: two continuous maps f, g : S → S are related iff there is a homotopy from f to g.

def DegreeTheory.SelfMapHomotopyClass (S : TopCat) : Type

Homotopy classes of self-maps of S, denoted [S, S].

@[implicit_reducible]

instance DegreeTheory.instMonoidSelfMapHomotopyClass (S : TopCat) : Monoid (SelfMapHomotopyClass S)

The monoid structure on [S, S] induced by composition of representatives.

noncomputable def DegreeTheory.degreeHom (n : ℕ) (S : TopCat) (φ : (homologyFunctorZ n).obj S ≅ AddCommGrpCat.of ℤ) : SelfMapHomotopyClass S →* ℤ

The degree homomorphism deg : [S, S] → ℤ for a space S with H_n(S) ≅ ℤ: assigns to each homotopy class of self-maps [f] the degree of the induced endomorphism of H_n(S). Multiplicative under composition.

def DegreeTheory.sphereTopCat (n : ℕ) : TopCat

The n-sphere S^n ⊆ ℝ^{n+1} packaged as an object of TopCat.

theorem DegreeTheory.exists_selfmap_of_degree_one (φ : (homologyFunctorZ 1).obj (sphereTopCat 1) ≅ AddCommGrpCat.of ℤ) (k : ℤ) : ∃ (f : sphereTopCat 1 ⟶ sphereTopCat 1), degreeOfEndo φ ((homologyFunctorZ 1).map f) = k

Base case for the surjectivity of degree on S^1: for every integer k, the self-map z ↦ z^k of S^1 has degree k.

theorem DegreeTheory.degreeOfEndo_iso_independent {G : AddCommGrpCat} (φ φ' : G ≅ AddCommGrpCat.of ℤ) (e : G ⟶ G) : degreeOfEndo φ e = degreeOfEndo φ' e

The degree of an endomorphism is independent of the chosen isomorphism G ≅ ℤ: any two isomorphisms differ by an automorphism of ℤ (i.e. ±1), and the conjugation cancels.

theorem DegreeTheory.degreeOfEndo_conj {G H : AddCommGrpCat} (φ : G ≅ AddCommGrpCat.of ℤ) (ψ : H ≅ AddCommGrpCat.of ℤ) (α : G ≅ H) (e : G ⟶ G) : degreeOfEndo ψ (CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp e α.hom)) = degreeOfEndo φ e

Conjugation invariance of degree: transporting e across an isomorphism α : G ≅ H preserves its degree (with respect to compatible identifications of G and H with ℤ).

noncomputable def DegreeTheory.suspSafeNorm (n : ℕ) (w : EuclideanSpace ℝ (Fin (n + 1))) : SphereHomology.Sphere n

Safe normalization map ℝ^{n+1} → S^n: sends a non-zero vector w to w / ‖w‖ and maps 0 to the basepoint e_0, so as to be defined everywhere.

noncomputable def DegreeTheory.suspInitProj (n : ℕ) (v : EuclideanSpace ℝ (Fin (n + 2))) : EuclideanSpace ℝ (Fin (n + 1))

Project an element of ℝ^{n+2} onto its first n+1 coordinates, viewed as an element of ℝ^{n+1}.

noncomputable def DegreeTheory.suspSnocProj (n : ℕ) (w : EuclideanSpace ℝ (Fin (n + 1))) (t : ℝ) : EuclideanSpace ℝ (Fin (n + 2))

Append a real scalar t as the last coordinate to a vector in ℝ^{n+1}, producing a vector in ℝ^{n+2}.

noncomputable def DegreeTheory.suspRaw (n : ℕ) (f : sphereTopCat n ⟶ sphereTopCat n) (v : EuclideanSpace ℝ (Fin (n + 2))) : EuclideanSpace ℝ (Fin (n + 2))

The raw suspension of a self-map f : S^n → S^n: a map ℝ^{n+2} → ℝ^{n+2} that scales the first n+1 coordinates by f (after radial normalization) and leaves the last coordinate unchanged. Restricted to S^{n+1} this defines the topological suspension.

theorem DegreeTheory.suspRaw_norm (n : ℕ) (f : sphereTopCat n ⟶ sphereTopCat n) (v : EuclideanSpace ℝ (Fin (n + 2))) (hv : ‖v‖ = 1) : ‖suspRaw n f v‖ = 1

The raw suspension suspRaw n f preserves the unit sphere: if ‖v‖ = 1 then ‖suspRaw n f v‖ = 1. This is what makes suspRaw descend to a well-defined map S^{n+1} → S^{n+1}.

theorem DegreeTheory.suspSafeNorm_val_of_ne_zero (n : ℕ) (w : EuclideanSpace ℝ (Fin (n + 1))) (hw : w ≠ 0) : ↑(suspSafeNorm n w) = ‖w‖⁻¹ • w

Away from zero, the safe normalization map is given by the expected formula w ↦ w / ‖w‖.

theorem DegreeTheory.continuous_suspRaw (n : ℕ) (f : sphereTopCat n ⟶ sphereTopCat n) : Continuous (suspRaw n f)

Continuity of the raw suspension suspRaw n f. The only non-trivial point is w = 0 in the first n+1 coordinates, where the radial normalization is squeezed to 0 by the boundedness ‖f(·)‖ = 1.

noncomputable def DegreeTheory.suspensionOfSphereMap (n : ℕ) (_hn : n ≥ 1) (f : sphereTopCat n ⟶ sphereTopCat n) : sphereTopCat (n + 1) ⟶ sphereTopCat (n + 1)

The (unreduced) suspension Σf : S^{n+1} → S^{n+1} of a self-map f : S^n → S^n, obtained by restricting suspRaw n f to the unit sphere.

theorem DegreeTheory.suspensionMap_degree_eq (n : ℕ) (hn : n ≥ 1) (f : sphereTopCat n ⟶ sphereTopCat n) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) (ψ : (homologyFunctorZ (n + 1)).obj (sphereTopCat (n + 1)) ≅ AddCommGrpCat.of ℤ) : degreeOfEndo ψ ((homologyFunctorZ (n + 1)).map (suspensionOfSphereMap n hn f)) = degreeOfEndo φ ((homologyFunctorZ n).map f)

Suspension preserves degree: deg(Σf) = deg(f) for any self-map f : S^n → S^n. This is the inductive step used to extend exists_selfmap_of_degree_one from S^1 to all spheres S^n, n ≥ 1.

theorem DegreeTheory.addCommGrpCat_endZ_eq_of_apply_one (e₁ e₂ : AddCommGrpCat.of ℤ ⟶ AddCommGrpCat.of ℤ) (h : (CategoryTheory.ConcreteCategory.hom e₁) 1 = (CategoryTheory.ConcreteCategory.hom e₂) 1) : e₁ = e₂

Two endomorphisms of ℤ (in AddCommGrp) agree iff they agree on 1.

theorem DegreeTheory.endo_eq_of_same_degree' {G : AddCommGrpCat} (φ : G ≅ AddCommGrpCat.of ℤ) (e₁ e₂ : G ⟶ G) (h : degreeOfEndo φ e₁ = degreeOfEndo φ e₂) : e₁ = e₂

Two endomorphisms of G ≅ ℤ are equal iff they have the same degree.

theorem DegreeTheory.suspensionMap_homology_eq (n : ℕ) (hn : n ≥ 1) (f : sphereTopCat n ⟶ sphereTopCat n) (α : AlgebraicTopologyI.SingularHomologyGroup n (SphereHomology.Sphere n) ≅ AlgebraicTopologyI.SingularHomologyGroup (n + 1) (SphereHomology.Sphere (n + 1))) : (homologyFunctorZ (n + 1)).map (suspensionOfSphereMap n hn f) = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp ((homologyFunctorZ n).map f) α.hom)

The homology endomorphism induced by Σf : S^{n+1} → S^{n+1} agrees, up to the suspension isomorphism α : H_n(S^n) ≅ H_{n+1}(S^{n+1}), with the endomorphism induced by f on H_n(S^n).

theorem DegreeTheory.exists_selfmap_of_degree_succ (n : ℕ) (hn : n ≥ 1) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) (ψ : (homologyFunctorZ (n + 1)).obj (sphereTopCat (n + 1)) ≅ AddCommGrpCat.of ℤ) (k : ℤ) (hk : ∃ (f : sphereTopCat n ⟶ sphereTopCat n), degreeOfEndo φ ((homologyFunctorZ n).map f) = k) : ∃ (g : sphereTopCat (n + 1) ⟶ sphereTopCat (n + 1)), degreeOfEndo ψ ((homologyFunctorZ (n + 1)).map g) = k

Inductive step for exists_selfmap_of_degree: if every integer is realized as a degree of a self-map of S^n, then the same holds for S^{n+1} (take the suspension).

theorem DegreeTheory.exists_selfmap_of_degree (n : ℕ) (hn : n ≥ 1) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) (k : ℤ) : ∃ (f : sphereTopCat n ⟶ sphereTopCat n), degreeOfEndo φ ((homologyFunctorZ n).map f) = k

For every n ≥ 1 and every integer k, there exists a self-map of S^n of degree k. Proved by induction on n: base case n = 1 is exists_selfmap_of_degree_one, induction step is exists_selfmap_of_degree_succ.

theorem DegreeTheory.degree_surjective (n : ℕ) (hn : n ≥ 1) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) : Function.Surjective ⇑(degreeHom n (sphereTopCat n) φ)

Theorem 10.8 (Surjectivity of degree). For every n ≥ 1, the degree homomorphism deg : [S^n, S^n] → ℤ is surjective: every integer is realized as the degree of some continuous self-map of the n-sphere.

theorem DegreeTheory.update_neg_mem_sphere (n : ℕ) (i : Fin (n + 1)) (x : SphereHomology.Sphere n) : (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (Function.update ((WithLp.equiv 2 (Fin (n + 1) → ℝ)) ↑x) i (-(↑x).ofLp i)) ∈ Metric.sphere 0 1

Negating one coordinate of a point on S^n produces another point on S^n (the coordinate-reflected image).

theorem DegreeTheory.continuous_update_neg (n : ℕ) (i : Fin (n + 1)) : Continuous fun (v : EuclideanSpace ℝ (Fin (n + 1))) => (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (Function.update ((WithLp.equiv 2 (Fin (n + 1) → ℝ)) v) i (-v.ofLp i))

The coordinate reflection map on ℝ^{n+1} (negating the i-th coordinate) is continuous.

def DegreeTheory.antipodalMap (n : ℕ) : sphereTopCat n ⟶ sphereTopCat n

The antipodal map S^n → S^n, x ↦ -x. Has degree (-1)^{n+1}.

def DegreeTheory.coordReflection (n : ℕ) (i : Fin (n + 1)) : sphereTopCat n ⟶ sphereTopCat n

The coordinate reflection r_i : S^n → S^n that negates the i-th coordinate and fixes the others. Has degree -1.

def DegreeTheory.iteratedReflection (n k : ℕ) (hk : k ≤ n + 1) : sphereTopCat n ⟶ sphereTopCat n

The composition of the first k coordinate reflections r_{k-1} ∘ ... ∘ r_0, a self-map of S^n. Taking k = n + 1 recovers the antipodal map (up to homotopy).

theorem DegreeTheory.degree_coordReflection (n : ℕ) (i : Fin (n + 1)) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) : degreeOfEndo φ ((homologyFunctorZ n).map (coordReflection n i)) = -1

Each coordinate reflection r_i : S^n → S^n has degree -1.

theorem DegreeTheory.iteratedReflection_full (n : ℕ) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) : degreeOfEndo φ ((homologyFunctorZ n).map (antipodalMap n)) = degreeOfEndo φ ((homologyFunctorZ n).map (iteratedReflection n (n + 1) ⋯))

The antipodal map x ↦ -x is homotopic (and hence equal in homology) to the composition of all n + 1 coordinate reflections.

theorem DegreeTheory.degree_iteratedReflection (n : ℕ) (φ : (homologyFunctorZ n).obj (sphereTopCat n) ≅ AddCommGrpCat.of ℤ) (k : ℕ) (hk : k ≤ n + 1) : degreeOfEndo φ ((homologyFunctorZ n).map (iteratedReflection n k hk)) = (-1) ^ k

The degree of iteratedReflection n k equals (-1)^k, by multiplicativity of degree and degree_coordReflection. In particular, taking k = n + 1 shows that the antipodal map has degree (-1)^{n+1}.