HF
plain-language theorem explainer
Degree-n homology functor from chain complexes of ℤ-modules to ℤ-modules, with the standard downward grading. Cited wherever Singular Mayer–Vietoris needs a short name for H_n. Pure one-line abbreviation of Mathlib’s homologyFunctor at ComplexShape.down.
Claim. For each $n \in \mathbb{N}$, write $H_n$ for the degree-$n$ homology functor $\mathbf{Ch}_{\downarrow}(\mathrm{Mod}_{\mathbb{Z}}) \to \mathrm{Mod}_{\mathbb{Z}}$ on chain complexes of abelian groups graded by $\mathbb{N}$ with differential lowering degree.
background
The ambient module builds singular Mayer–Vietoris data: singular chain complexes on open sets, inclusions, retractions, and biproducts of complexes of $\mathbb{Z}$-modules. Homology is taken in the abelian category ModuleCat ℤ.
Mathlib supplies HomologicalComplex.homologyFunctor, which sends a chain complex to its degree-$n$ homology object. The complex shape used here is ComplexShape.down ℕ: differentials lower the index, the usual convention for singular chains $C_*$.
This abbreviation simply freezes that functor at fixed $n$, so later lemmas can write $H_n$ instead of the full Mathlib path. Sibling infrastructure (singular generators, inclusions, boundaries) lives in the same file and feeds the complexes on which $H_n$ acts.
proof idea
Definitional one-liner: expand to HomologicalComplex.homologyFunctor (ModuleCat ℤ) (ComplexShape.down ℕ) n. No proof obligations; noncomputable is inherited from the Mathlib homology construction.
why it matters
Local parent is homologyBiprodIso in the same module: additivity $H_n(C_(U)\oplus C_(V))\cong H_n(U)\oplus H_n(V)$, the biproduct step before a Mayer–Vietoris long exact sequence. Without a compact $H_n$ name, every singular MV lemma would restate the full homology functor.
In the Recognition foundation stack this sits under SingularMayerVietoris, which packages classical singular homology tools used when comparing covers and recognition-side chain data. It is scaffolding for exactness and excision-style arguments, not a forcing-chain (T0–T8) step itself.
Name collisions with hereditarily-finite “HF” encodings elsewhere in the repo are unrelated; those PRC set-theory parses do not depend on this functor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.