Foundation Singular Mayer Vietoris Mv Sum Epi Zero

The surjectivity theorem

In algebraic topology, the Mayer-Vietoris sequence is a tool for computing the homology of a space by splitting it into two overlapping pieces. The declaration mvSum_epi_zero is a machine-checked theorem about the very first stage of that sequence. It states: if U and V are open subsets of a topological space X, and their union is all of X, then the map that sends a pair of zero-dimensional cycles, one from U and one from V, to their sum in X is surjective. In plainer terms, every zero-dimensional cycle of the whole space can be written as a sum of a cycle that lives inside U and a cycle that lives inside V.

The proof is not a sketch. It is a formal derivation in a machine-checked library of formal theorems, which means every step is verified by a computer. The theorem is proved for singular homology with integer coefficients, where a zero-dimensional cycle is a formal integer combination of points. The key condition is that the two open sets cover the space; this is what guarantees that any point in X is already in U or in V, so the zero-dimensional cycles from the two pieces generate everything.

This result is a small but necessary step in building the full Mayer-Vietoris sequence in the framework's library. It is the zero-dimensional case of a more general statement about the sequence being exact. The theorem shows that the first map in the sequence is onto, which is one of the two properties needed for exactness at that stage. Without this surjectivity, the sequence would not be a useful computational tool, because it would not capture all cycles of the whole space.

What the theorem does not claim is important. It does not say that the map is injective, so it does not establish exactness at the zero-dimensional stage by itself. It does not apply to higher-dimensional cycles; it is specifically about dimension zero. It also does not say anything about the physical interpretation of cycles in the Recognition Science framework. The theorem is a purely topological result about singular homology, not a statement about ledgers, recognition events, or the framework's cost function.

/-- **The degree-`0` tail**: `H_0(U) ⊞ H_0(V) ⟶ H_0(X)` is surjective; the
Mayer-Vietoris sequence ends `⋯ ⟶ H_0(U) ⊞ H_0(V) ⟶ H_0(X) ⟶ 0`. -/
theorem mvSum_epi_zero (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) : Epi (mvSum U V 0) := by
  haveI h1 : Epi (HomologicalComplex.homologyMap (mvβ U V) 0) := by
    refine epi_homologyMap_chain_zero (mvβ U V) ?_
    intro y
    have hepi : Epi ((mvβ U V).f 0) := (mvSES_degreewise_shortExact U V 0).epi_g
    have hsurj : Function.Surjective ((mvβ U V).f 0) :=
      (ModuleCat.epi_iff_surjective _).mp hepi
    obtain ⟨x, hx⟩ := hsurj y
    refine ⟨x, 0, ?_⟩
    rw [map_zero, add_zero, hx]
  haveI h2 : IsIso (HomologicalComplex.homologyMap (smallι U V) 0) :=
    smallι_isIso_homologyMap hU hV hUV 0
  rw [mvSum_eq]
  infer_instance

What this page does not claim

The theorem does not establish injectivity of the sum map. The theorem does not apply to cycles of dimension greater than zero. The theorem does not make any claim about the physical or recognition-based interpretation of cycles.

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/SingularMayerVietoris.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: