structure MayerVietoris.MayerVietorisCover : Type (u + 1)

A Mayer-Vietoris cover of a space: a two-element family {A, B} of subsets of X whose interiors cover X. This is the input data for Theorem 11.5.

• X : Type u
• instTop : TopologicalSpace self.X
• A : Set self.X
• B : Set self.X
• cover : interior self.A ∪ interior self.B = Set.univ

def MayerVietoris.MayerVietorisCover.pairX (c : MayerVietorisCover) : EilenbergSteenrod.TopPair

The trivial pair (X, ∅) associated to the ambient space of a Mayer-Vietoris cover.

def MayerVietoris.MayerVietorisCover.pairA (c : MayerVietorisCover) : EilenbergSteenrod.TopPair

The trivial pair (A, ∅) associated to the first cover element.

def MayerVietoris.MayerVietorisCover.pairB (c : MayerVietorisCover) : EilenbergSteenrod.TopPair

The trivial pair (B, ∅) associated to the second cover element.

def MayerVietoris.MayerVietorisCover.pairAB (c : MayerVietorisCover) : EilenbergSteenrod.TopPair

The trivial pair (A ∩ B, ∅) associated to the intersection of the cover elements.

def MayerVietoris.MayerVietorisCover.inclAB_A (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.pairAB c.pairA

The inclusion of pairs (A ∩ B, ∅) ↪ (A, ∅), which underlies the map j_1 : H_n(A ∩ B) → H_n(A) in the Mayer-Vietoris sequence.

def MayerVietoris.MayerVietorisCover.inclAB_B (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.pairAB c.pairB

The inclusion of pairs (A ∩ B, ∅) ↪ (B, ∅), which underlies the map j_2 : H_n(A ∩ B) → H_n(B) in the Mayer-Vietoris sequence.

def MayerVietoris.MayerVietorisCover.inclA_X (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.pairA c.pairX

The inclusion of pairs (A, ∅) ↪ (X, ∅), which underlies the map i_1 : H_n(A) → H_n(X) in the Mayer-Vietoris sequence.

def MayerVietoris.MayerVietorisCover.inclB_X (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.pairB c.pairX

The inclusion of pairs (B, ∅) ↪ (X, ∅), which underlies the map i_2 : H_n(B) → H_n(X) in the Mayer-Vietoris sequence.

structure MayerVietoris.MayerVietorisSequence (h : EilenbergSteenrod.HomologyTheory) (c : MayerVietorisCover) : Type u_1

The Mayer-Vietoris long exact sequence for a homology theory h and a cover c (Theorem 11.5): connecting homomorphisms ∂ : H_{n+1}(X) →+ H_n(A ∩ B) together with exactness of the long sequence ⋯ → H_n(A ∩ B) → H_n(A) ⊕ H_n(B) → H_n(X) → H_{n-1}(A ∩ B) → ⋯, where the first map is [j_{1*}, -j_{2*}] and the second is i_{1*} + i_{2*}.

• connecting (n : ℤ) : h.H (n + 1) c.pairX →+ h.H n c.pairAB
• exact_at_prod (n : ℤ) : Function.Exact (fun (x : h.H n c.pairAB) => ((h.map n c.inclAB_A) x, -(h.map n c.inclAB_B) x)) fun (p : h.H n c.pairA × h.H n c.pairB) => (h.map n c.inclA_X) p.1 + (h.map n c.inclB_X) p.2
• exact_at_X (n : ℤ) : Function.Exact (fun (p : h.H (n + 1) c.pairA × h.H (n + 1) c.pairB) => (h.map (n + 1) c.inclA_X) p.1 + (h.map (n + 1) c.inclB_X) p.2) ⇑(self.connecting n)
• exact_at_AB (n : ℤ) : Function.Exact ⇑(self.connecting n) fun (x : h.H n c.pairAB) => ((h.map n c.inclAB_A) x, -(h.map n c.inclAB_B) x)

def MayerVietoris.MayerVietorisCover.pairXA (c : MayerVietorisCover) : EilenbergSteenrod.TopPair

The pair (X, A) extracted from a Mayer-Vietoris cover, used as the input to the excision axiom that drives the construction of the connecting homomorphism.

theorem MayerVietoris.MayerVietorisCover.excisive (c : MayerVietorisCover) : EilenbergSteenrod.IsExcisiveTriple c.pairXA c.Bᶜ

The complement of B is an excisive subset of the pair (X, A): its closure lies in the interior of A. This is the geometric input that lets us apply excision when building the Mayer-Vietoris connecting homomorphism.

@[reducible, inline]

abbrev MayerVietoris.MayerVietorisCover.EP (c : MayerVietorisCover) : EilenbergSteenrod.TopPair

The excised pair (X \ Bᶜ, A \ Bᶜ), abbreviated EP, used as the intermediate pair through which the connecting homomorphism is factored.

def MayerVietoris.MayerVietorisCover.trSub (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.EP.subPair c.pairAB

The homeomorphism of pairs from the sub-pair of EP to (A ∩ B, ∅): each point of the excised subspace lies in A (by sub-pair membership) and in B (since it is not in Bᶜ).

def MayerVietoris.MayerVietorisCover.trSubInv (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.pairAB c.EP.subPair

Inverse to trSub: each point of A ∩ B lies outside Bᶜ, hence in the sub-pair of the excised pair EP.

def MayerVietoris.MayerVietorisCover.trSp (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs (EilenbergSteenrod.TopPair.ofSpace c.EP.space) c.pairB

The homeomorphism of pairs from the total-space pair of EP to (B, ∅): a point of X that lies outside Bᶜ is the same data as a point of B.

def MayerVietoris.MayerVietorisCover.trSpInv (c : MayerVietorisCover) : EilenbergSteenrod.MapOfPairs c.pairB (EilenbergSteenrod.TopPair.ofSpace c.EP.space)

Inverse to trSp: a point of B corresponds to the point of X lying outside Bᶜ in the total space of the excised pair.

def MayerVietoris.constHomotopy {P : EilenbergSteenrod.TopPair} (f : EilenbergSteenrod.MapOfPairs P P) (hf : ∀ (x : P.space), f.toFun x = x) : EilenbergSteenrod.HomotopyOfPairMaps f (EilenbergSteenrod.MapOfPairs.id P)

The constant homotopy from a self-map of a pair f : P → P that acts as the identity on points (f x = x) to the identity map of P.

theorem MayerVietoris.MayerVietorisCover.trSub_comp_inv_htpy (c : MayerVietorisCover) : EilenbergSteenrod.AreHomotopic (c.trSub.comp c.trSubInv) (EilenbergSteenrod.MapOfPairs.id c.pairAB)

trSub and trSubInv compose (one way) to the identity of (A ∩ B, ∅), up to homotopy of pair maps.

theorem MayerVietoris.MayerVietorisCover.trSubInv_comp_htpy (c : MayerVietorisCover) : EilenbergSteenrod.AreHomotopic (c.trSubInv.comp c.trSub) (EilenbergSteenrod.MapOfPairs.id c.EP.subPair)

trSub and trSubInv compose (the other way) to the identity of EP.subPair, up to homotopy of pair maps.

theorem MayerVietoris.MayerVietorisCover.trSp_comp_inv_htpy (c : MayerVietorisCover) : EilenbergSteenrod.AreHomotopic (c.trSp.comp c.trSpInv) (EilenbergSteenrod.MapOfPairs.id c.pairB)

trSp and trSpInv compose (one way) to the identity of (B, ∅), up to homotopy of pair maps.

theorem MayerVietoris.MayerVietorisCover.trSpInv_comp_htpy (c : MayerVietorisCover) : EilenbergSteenrod.AreHomotopic (c.trSpInv.comp c.trSp) (EilenbergSteenrod.MapOfPairs.id (EilenbergSteenrod.TopPair.ofSpace c.EP.space))

trSp and trSpInv compose (the other way) to the identity of the total-space pair of EP, up to homotopy.

theorem MayerVietoris.hom_inv_id (ht : EilenbergSteenrod.HomologyTheory) (n : ℤ) {P Q : EilenbergSteenrod.TopPair} (f : EilenbergSteenrod.MapOfPairs P Q) (g : EilenbergSteenrod.MapOfPairs Q P) (hgf : EilenbergSteenrod.AreHomotopic (g.comp f) (EilenbergSteenrod.MapOfPairs.id P)) (x : ht.H n P) : (ht.map n g) ((ht.map n f) x) = x

If g ∘ f is homotopic to the identity, then on a homology theory ht.map n g is a left inverse of ht.map n f, by homotopy invariance and functoriality.

theorem MayerVietoris.transfer_bijective (ht : EilenbergSteenrod.HomologyTheory) (n : ℤ) {P Q : EilenbergSteenrod.TopPair} (f : EilenbergSteenrod.MapOfPairs P Q) (g : EilenbergSteenrod.MapOfPairs Q P) (hfg : EilenbergSteenrod.AreHomotopic (f.comp g) (EilenbergSteenrod.MapOfPairs.id Q)) (hgf : EilenbergSteenrod.AreHomotopic (g.comp f) (EilenbergSteenrod.MapOfPairs.id P)) : Function.Bijective ⇑(ht.map n f)

If f and g are pair maps whose compositions are both homotopic to the identity, then ht.map n f is a bijection. This packages the homotopy equivalence into a bijection on homology, used to transfer information across the excised pair.

theorem MayerVietoris.MayerVietorisCover.inclA_X_comp_inclAB_A_eq (c : MayerVietorisCover) : c.inclA_X.comp c.inclAB_A = c.inclB_X.comp c.inclAB_B

The two ways of including A ∩ B into X (via A and via B) agree as pair maps.

theorem MayerVietoris.MayerVietorisCover.inclAB_B_comp_eq (c : MayerVietorisCover) : c.trSp.comp ((EilenbergSteenrod.inclusionSubToSpace c.EP).comp c.trSubInv) = c.inclAB_B

The inclusion (A ∩ B, ∅) ↪ (B, ∅) factors as the round-trip (A ∩ B, ∅) → EP.subPair ↪ EP.space → (B, ∅) through the excised pair.

theorem MayerVietoris.MayerVietorisCover.exc_restrictToSub_eq (c : MayerVietorisCover) : (EilenbergSteenrod.excisionInclusion c.pairXA c.Bᶜ).restrictToSub = c.inclAB_A.comp c.trSub

The restriction of the excision inclusion to subspaces factors as trSub followed by inclAB_A.

theorem MayerVietoris.MayerVietorisCover.comm2_eq (c : MayerVietorisCover) : (EilenbergSteenrod.inclusionSpaceToPair c.pairXA).comp c.inclB_X = (EilenbergSteenrod.excisionInclusion c.pairXA c.Bᶜ).comp ((EilenbergSteenrod.inclusionSpaceToPair c.EP).comp c.trSpInv)

The composite (B, ∅) ↪ (X, ∅) ↪ (X, A) agrees with the composite that goes through the excised pair EP via trSpInv and the excision inclusion.

theorem MayerVietoris.exact_transfer_bij {A : Type u_1} {B : Type u_2} {C : Type u_3} {B' : Type u_4} {C' : Type u_5} [AddCommGroup B] [AddCommGroup C] [AddCommGroup B'] [AddCommGroup C'] {f : A → B} {g : B → C} (he : Function.Exact f g) (ψ : B →+ B') (ψ' : B' →+ B) (hψψ' : ∀ (y : B'), ψ (ψ' y) = y) (hψ'ψ : ∀ (x : B), ψ' (ψ x) = x) (χ : C →+ C') (hχ_inj : Function.Injective ⇑χ) : Function.Exact (⇑ψ ∘ f) fun (y' : B') => χ (g (ψ' y'))

Exactness transfer along bijective homomorphisms: if f, g form an exact sequence at B, ψ : B ≃+ B' is a two-sided inverse pair, and χ : C →+ C' is injective, then (ψ ∘ f, χ ∘ g ∘ ψ⁻¹) is exact at B'. Used to push exactness across the homotopy equivalences trSub, trSp in the Mayer-Vietoris construction.

noncomputable def MayerVietoris.mayer_vietoris_sequence (h : EilenbergSteenrod.HomologyTheory) (c : MayerVietorisCover) : MayerVietorisSequence h c

The Mayer-Vietoris long exact sequence (Theorem 11.5): from any Eilenberg-Steenrod homology theory h and a cover c = {A, B} of X by sets whose interiors cover, we construct the connecting homomorphism ∂ and the three exactness statements assembling into the long exact sequence ⋯ → H_n(A ∩ B) → H_n(A) ⊕ H_n(B) → H_n(X) → H_{n-1}(A ∩ B) → ⋯. The proof factors the boundary H_{n+1}(X) → H_n(A ∩ B) through the long exact sequence of the pair (X, A) and the excised pair, using the homotopy equivalences trSub, trSp.