mvInclU
plain-language theorem explainer
Defines the continuous inclusion of the intersection U ∩ V into the open set U, as a morphism of topological spaces. Anyone building the singular Mayer–Vietoris sequence cites it as the left leg of the pair map. The body is a one-line application of the nested-subspace inclusion constructor to the standard fact that an intersection sits inside its left factor.
Claim. For open sets $U,V \subseteq X$, there is a continuous inclusion morphism $U \cap V \hookrightarrow U$ in the category of topological spaces, induced by the subset relation $U \cap V \subseteq U$.
background
The module builds a concrete singular Mayer–Vietoris short complex for a cover $X = U \cup V$ by open sets. Chains on $U$ and on $V$ are assembled into a "small" complex relative to the cover; the connecting maps come from space-level inclusions of the intersection.
The helper subIncl turns any subset relation $W \subseteq W'$ into a TopCat morphism TopCat.of W ⟶ TopCat.of W' via the continuous set-theoretic inclusion. The present definition specialises that helper to $W = U \cap V$ and $W' = U$, using Set.inter_subset_left.
Notation: $U$ and $V$ are the two open pieces of the cover of the ambient space $X$; the intersection is equipped with the subspace topology before being reified as an object of TopCat.
proof idea
One-line definitional wrapper: apply the nested-subspace inclusion constructor to the Lean fact that an intersection is a subset of its left factor. No further algebraic work; the continuity of the inclusion is inherited from the constructor.
why it matters
This inclusion is the left geometric leg of the whole Mayer–Vietoris apparatus in the module. It feeds the degreewise short complex (pair map into the biproduct of chains on $U$ and $V$), the homology-level pair map sending $[c]$ to $([i_*c],-[j_*c])$, the middle-exactness lemma that recovers a chain on the intersection from cancelling chains on $U$ and $V$, and the compatibility of the two routes through $U$ and through $V$ into the small complex.
Downstream, ArcComplementAcyclic uses it in the elementwise MV injectivity statement at $H_1(U \cap V)$ and in the bisection step for complements of two-arc unions. Those results sit in the foundation layer that supports acyclicity arguments for arc complements, which in turn underwrite topological forcing steps in the Recognition Science chain (dimension and covering arguments adjacent to T7–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.