Foundation Singular Mayer Vietoris Mv Ses Short Exact

The short exact sequence

In algebraic topology, the Mayer-Vietoris theorem is a tool for computing the homology of a space by cutting it into two overlapping pieces. The classic setup starts with a topological space X and two open subsets U and V whose union is all of X. The theorem then relates the homology of X to the homologies of U, V, and their intersection U ∩ V. The engine behind this relation is a short exact sequence of chain complexes, a precise algebraic statement that the image of one map equals the kernel of the next. The declaration mvSES_shortExact in the Recognition Science library is the machine-checked construction of exactly this sequence for singular homology.

The construction begins with a singular n-simplex, a continuous map from the standard n-simplex into X. Such a simplex is called small, a discrete record of a simplex whose image lies entirely inside U or entirely inside V. The library first forms the chain groups generated by these small simplices, then proves that these groups assemble into a chain complex with the usual boundary maps. Two inclusion maps then relate the small groups to the full singular chain groups of U, V, and X. The key lemmas mvSESdeg_epi and mvSESdeg_exact establish that, at every degree n, the map out of the sum of the chain groups of U and V is surjective and that the sequence is exact. These two facts, packaged together, form the short exact sequence that the declaration names.

The short exact sequence itself is a statement about the algebraic structure of the chain groups, not about the topology of X directly. It does not, by itself, compute any homology group. What it provides is the input for the long exact sequence in homology, which is the standard route to the Mayer-Vietoris theorem. The library also proves auxiliary results that make the construction usable: the boundary of a small simplex is small, the inclusion of the small groups into the full groups is injective, and the sum map is surjective when U and V cover X. These are the technical conditions that guarantee the sequence behaves as required.

In Recognition Science, this declaration is one step in a larger program of building algebraic topology from the framework's foundational principles. The framework treats conventional mathematics as its own derivation, so this is not a new result but a formal verification of a classical one. What the declaration adds is certainty: the proof is checked by a machine, leaving no gap in the chain of reasoning. The value for a reader is the assurance that the Mayer-Vietoris sequence, a workhorse of algebraic topology, holds in this formal setting without hidden assumptions.

lemma mvSESdeg_exact (n : ℕ) : (mvSESdeg U V n).Exact := by
  rw [ShortComplex.moduleCat_exact_iff]
  intro z hz
  have hz' : uInc U V n
      ((biprod.fst : Cgrp (TopCat.of U) n ⊞ Cgrp (TopCat.of V) n ⟶ _) z) +
      vInc U V n
      ((biprod.snd : Cgrp (TopCat.of U) n ⊞ Cgrp (TopCat.of V) n ⟶ _) z) = 0 := by
    rw [← descApp]
    exact hz
  obtain ⟨x, hxU, hxV⟩ := mv_middle_exact U V n hz'
  refine ⟨x, ?_⟩
  apply biprod_elem_ext
  · rw [show (mvSESdeg U V n).f x = biprod.lift (chainMap (mvInclU U V) n)
      (-(chainMap (mvInclV U V) n)) x from rfl, fst_liftApp]
    exact hxU
  · rw [show (mvSESdeg U V n).f x = biprod.lift (chainMap (mvInclU U V) n)
      (-(chainMap (mvInclV U V) n)) x from rfl, snd_liftApp, negApp, hxV,
      neg_neg]

lemma mvSESdeg_epi (n : ℕ) : Epi (mvSESdeg U V n).g := by
  show Epi (biprod.desc (uInc U V n) (vInc U V n))
  rw [ModuleCat.epi_iff_surjective]
  intro y
  induction y using freeInduction with
  | unit t =>
      rcases t.2 with h | h
      · refine ⟨(biprod.inl : Cgrp (TopCat.of U) n ⟶ _)
          (unitOf (liftIdx U t.1 h)), ?_⟩
        rw [← ModuleCat.comp_apply, biprod.inl_desc, uInc_unitOf]
        congr 1
      · refine ⟨(biprod.inr : Cgrp (TopCat.of V) n ⟶ _)
          (unitOf (liftIdx V t.1 h)), ?_⟩
        rw [← ModuleCat.comp_apply, biprod.inr_desc, vInc_unitOf]
        congr 1
  | zero => exact ⟨0, map_zero _⟩
  | add x y hx hy =>
      obtain ⟨a, ha⟩ := hx
      obtain ⟨b, hb⟩ := hy
      exact ⟨a + b, by rw [map_add, ha, hb]⟩
  | smulz c x hx =>
      obtain ⟨a, ha⟩ := hx
      exact ⟨c • a, by rw [mapSmul, ha]⟩

/-- A singular `n`-simplex of `X` is *small* (relative to the pair of subsets
`U, V`) when its range lies in `U` or in `V`. -/
def Small (U V : Set X) {n : ℕ} (s : Idx X n) : Prop :=
  Set.range ⇑(simplexEquiv X n s) ⊆ U ∨ Set.range ⇑(simplexEquiv X n s) ⊆ V

/-- The degree-`n` inclusion is a (split) monomorphism. -/
lemma sInc_mono (n : ℕ) : Mono (sInc U V n) :=
  mono_of_mono_fac (sInc_comp_sRet U V n)

/-- The singular subdivision operator preserves the small span. -/
lemma sdOp_mem_smallSpan {U V : Set X} {n : ℕ} {z : Cgrp X n}
    (hz : z ∈ smallSpan U V n) : sdOp X n z ∈ smallSpan U V n := by
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hz
  · rintro _ ⟨s, hs, rfl⟩
    rw [genUnit_eq, ← ModuleCat.comp_apply, gen_sdOp]
    show ev1 (toChain (simplexEquiv X n s) n
      (asub (baryFn n) n (asimplex (idTuple n)))) ∈ smallSpan U V n
    exact toChain_one_mem_smallSpan _ _ fun w _ => small_pushSimplex hs w
  · rw [map_zero]; exact Submodule.zero_mem _
  · intro x y _ _ hx hy
    rw [map_add]; exact Submodule.add_mem _ hx hy
  · intro c x _ hx
    rw [mapSmul]; exact Submodule.smul_mem _ _ hx

What this page does not claim

The declaration does not compute any specific homology group. It does not prove the full Mayer-Vietoris theorem; it only establishes the short exact sequence that feeds into it. It does not require the open sets U and V to be connected or path-connected.

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: