Encyclopedia Foundation Foundation Singular Prism Homotopic Maps Induce Same Homology

ARTICLE 4 claims 4 theorems

Foundation Singular Prism Homotopic Maps Induce Same Homology

Two continuous maps that can be deformed into each other produce identical algebraic measurements of a space's holes.

Verify this page

Homotopy invariance of homology

In algebraic topology, homology groups are a way to count the holes in a space. A sphere has a two-dimensional hole, a circle has a one-dimensional hole, and so on. A continuous map from one space to another sends points in the first to points in the second, and it also sends their holes along for the ride, inducing a map between the homology groups. The central question is how much of this induced map depends on the original map itself.

The answer is that it depends only on the homotopy class, meaning the family of maps that can be continuously deformed into one another. Two maps are homotopic if one can be stretched and bent into the other without tearing. The classical theorem, proved by the Polish mathematician Witold Hurewicz in the 1930s, states that homotopic maps induce the same map on homology. This is the foundational invariance that makes homology computable and well-defined.

In Recognition Science, the framework's machine-checked library of formal theorems contains a declaration, homotopic_maps_induce_same_homology, which establishes this same classical result. The framework constructs a singular chain complex from a space, a sequence of free abelian groups built from continuous maps of simplices into the space. It then builds a prism operator, a formal algebraic device that witnesses the deformation between two homotopic maps. The theorem proves that this prism operator yields a chain homotopy between the chain maps induced by the two maps, which in turn implies they induce the same map on homology.

The framework's proof is a direct construction. It defines a prism map on each simplex, dividing a higher-dimensional prism into smaller pieces, and shows that the boundary of this prism exactly accounts for the difference between the two chain maps. The key lemmas verify the face and boundary compatibility conditions, ensuring the algebraic signs and compositions align. This is not a new mathematical discovery but a formal verification of a known theorem, carried out in a way that leaves no step unchecked.

What the theorem does not claim is also important. It does not claim that the induced map on homology is an isomorphism. That stronger statement requires the two spaces to be homotopy equivalent, meaning there are maps in both directions whose compositions are homotopic to the identity. The framework proves this separately in isIso_homology_map_of_homotopyEquiv. The declaration also does not claim anything about the reverse direction: two maps inducing the same homology map need not be homotopic. Homology is a coarse invariant, and many non-homotopic maps can produce identical homology maps.

The practical consequence is that homology can be computed using convenient models. To compute the homology of a circle, one can use a single point and a loop, and any map that wraps the loop once is as good as any other. This invariance is what allows topologists to replace complicated spaces with simpler ones that have the same homotopy type, confident that the hole count will not change.

THEOREM prismHomotopy · IndisputableMonolith/Foundation/SingularPrism.lean
prismHomotopy · IndisputableMonolith/Foundation/SingularPrism.lean:836 
/-- A homotopy of continuous maps induces a chain homotopy of the induced
maps of singular chain complexes, via the prism operator. -/
noncomputable def prismHomotopy {F₀ F₁ : X ⟶ Y}
    (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) :
    Homotopy (sChainMap F₀) (sChainMap F₁) where
  hom i j :=
    if h : i + 1 = j then
      (-prismOp Ho.toContinuousMap i prism) ≫ eqToHom (by subst h; rfl)
    else 0
  zero i j hij := by
    rw [dif_neg]
    intro h
    exact hij (by simpa using h)
  comm i := by
    match i with
    | 0 =>
      rw [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex]
      rw [dif_pos rfl, eqToHom_refl, Category.comp_id, Preadditive.neg_comp]
      show chainMap F₀ 0 =
        0 + -prismOp Ho.toContinuousMap 0 prism ≫ bnd Y 0 + chainMap F₁ 0
      have h0 := prism_chain_homotopy_zero Ho
      rw [eq_sub_iff_add_eq] at h0
      rw [← h0]
      abel
    | n + 1 =>
      rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex]
      rw [dif_pos rfl, dif_pos rfl, eqToHom_refl, eqToHom_refl, Category.comp_id,
        Category.comp_id, Preadditive.neg_comp, Preadditive.comp_neg]
      show chainMap F₀ (n + 1) =
        -bnd X n ≫ prismOp Ho.toContinuousMap n prism +
          -prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1) +
          chainMap F₁ (n + 1)
      have h0 := prism_chain_homotopy_succ Ho n
      rw [eq_sub_iff_add_eq] at h0
      rw [← h0]
      abel
THEOREM prism_chain_homotopy_succ · IndisputableMonolith/Foundation/SingularPrism.lean
prism_chain_homotopy_succ · IndisputableMonolith/Foundation/SingularPrism.lean:758 
/-- The chain homotopy identity in positive degrees:
`∂ ∘ P + P ∘ ∂ = (F₁)♯ − (F₀)♯` on the degree-`(n+1)` chain group. -/
lemma prism_chain_homotopy_succ (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) (n : ℕ) :
    bnd X n ≫ prismOp Ho.toContinuousMap n prism +
        prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1) =
      chainMap F₁ (n + 1) - chainMap F₀ (n + 1) := by
  apply Sigma.hom_ext
  intro s
  have hL1 : gen X (n + 1) s ≫ (bnd X n ≫ prismOp Ho.toContinuousMap n prism) =
      ∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
        gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
          ((TopCat.toSSet.obj X).δ k s)) := by
    rw [← Category.assoc, gen_d, Preadditive.sum_comp]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Preadditive.zsmul_comp, gen_prismOp, Pgen, Finset.smul_sum]
    refine Finset.sum_congr rfl fun i' _ => ?_
    rw [smul_smul, ← pow_add]
  have hL2 : gen X (n + 1) s ≫ (prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1)) =
      ∑ i : Fin (n + 2), ∑ j : Fin (n + 3), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) •
        gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
          (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)) := by
    rw [← Category.assoc, gen_prismOp, Pgen, Preadditive.sum_comp]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Preadditive.zsmul_comp, gen_d, Finset.smul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [smul_smul, ← pow_add]
  rw [Preadditive.comp_add, hL1, hL2, Preadditive.comp_sub, gen_map, gen_map,
    add_comm (∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
      gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
        ((TopCat.toSSet.obj X).δ k s)))]
  refine Eq.trans (prism_sum_cancellation n
    (fun i j => gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
      (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)))
    (fun k i' => gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
      ((TopCat.toSSet.obj X).δ k s)))
    (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
      Ho.toContinuousMap (prism i.succ) (prism i)
      (prism_comp_face_of_le (Fin.le_def.mpr (by simpa using hij))) s))
    (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
      Ho.toContinuousMap (prism i.castSucc) (prism i)
      (prism_comp_face_of_gt (Fin.lt_def.mpr (by simpa using hij))) s))
    (fun i => congrArg (gen Y (n + 1)) (δ_prismSimplex_congr
      Ho.toContinuousMap (prism i.castSucc) (prism i.succ)
      (prism_comp_face_cancel i) s))) ?_
  congr 1
  · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_top Ho (n + 1) s)
  · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_bot Ho (n + 1) s)
THEOREM prism_chain_homotopy_succ · IndisputableMonolith/Foundation/SingularPrism.lean
prism_chain_homotopy_succ · IndisputableMonolith/Foundation/SingularPrism.lean:758 
/-- The chain homotopy identity in positive degrees:
`∂ ∘ P + P ∘ ∂ = (F₁)♯ − (F₀)♯` on the degree-`(n+1)` chain group. -/
lemma prism_chain_homotopy_succ (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) (n : ℕ) :
    bnd X n ≫ prismOp Ho.toContinuousMap n prism +
        prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1) =
      chainMap F₁ (n + 1) - chainMap F₀ (n + 1) := by
  apply Sigma.hom_ext
  intro s
  have hL1 : gen X (n + 1) s ≫ (bnd X n ≫ prismOp Ho.toContinuousMap n prism) =
      ∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
        gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
          ((TopCat.toSSet.obj X).δ k s)) := by
    rw [← Category.assoc, gen_d, Preadditive.sum_comp]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Preadditive.zsmul_comp, gen_prismOp, Pgen, Finset.smul_sum]
    refine Finset.sum_congr rfl fun i' _ => ?_
    rw [smul_smul, ← pow_add]
  have hL2 : gen X (n + 1) s ≫ (prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1)) =
      ∑ i : Fin (n + 2), ∑ j : Fin (n + 3), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) •
        gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
          (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)) := by
    rw [← Category.assoc, gen_prismOp, Pgen, Preadditive.sum_comp]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Preadditive.zsmul_comp, gen_d, Finset.smul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [smul_smul, ← pow_add]
  rw [Preadditive.comp_add, hL1, hL2, Preadditive.comp_sub, gen_map, gen_map,
    add_comm (∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
      gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
        ((TopCat.toSSet.obj X).δ k s)))]
  refine Eq.trans (prism_sum_cancellation n
    (fun i j => gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
      (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)))
    (fun k i' => gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
      ((TopCat.toSSet.obj X).δ k s)))
    (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
      Ho.toContinuousMap (prism i.succ) (prism i)
      (prism_comp_face_of_le (Fin.le_def.mpr (by simpa using hij))) s))
    (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
      Ho.toContinuousMap (prism i.castSucc) (prism i)
      (prism_comp_face_of_gt (Fin.lt_def.mpr (by simpa using hij))) s))
    (fun i => congrArg (gen Y (n + 1)) (δ_prismSimplex_congr
      Ho.toContinuousMap (prism i.castSucc) (prism i.succ)
      (prism_comp_face_cancel i) s))) ?_
  congr 1
  · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_top Ho (n + 1) s)
  · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_bot Ho (n + 1) s)
THEOREM isIso_homology_map_of_homotopyEquiv · IndisputableMonolith/Foundation/SingularPrism.lean
isIso_homology_map_of_homotopyEquiv · IndisputableMonolith/Foundation/SingularPrism.lean:912 
/-- The map on singular homology induced by (the forward map of) a homotopy
equivalence is an isomorphism. -/
theorem isIso_homology_map_of_homotopyEquiv
    (h : ContinuousMap.HomotopyEquiv X Y) (n : ℕ) :
    IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
      (ModuleCat.of ℤ ℤ)).map (TopCat.ofHom h.toFun)) :=
  inferInstanceAs (IsIso ((homotopyEquiv_homology_iso h n).hom))

What this page does not claim

The declaration does not prove that homotopy equivalent spaces have isomorphic homology groups. The declaration does not claim that the induced map on homology is injective or surjective. The declaration does not address the converse, that maps inducing the same homology map must be homotopic.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SingularPrism.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND