Exactness of products #
A family of exact pairs Xᵢ → Yᵢ → Zᵢ gives an exact pair ∏ᵢ Xᵢ → ∏ᵢ Yᵢ → ∏ᵢ Zᵢ of
componentwise maps. This is the exactness of arbitrary products of abelian groups or modules,
used for instance to pass from a levelwise exact sequence of towers to the exact sequence of the
products of their terms.
theorem
Function.Exact.piMap
{ι : Type u_1}
{X : ι → Type u_2}
{Y : ι → Type u_3}
{Z : ι → Type u_4}
[(i : ι) → Zero (Z i)]
{f : (i : ι) → X i → Y i}
{g : (i : ι) → Y i → Z i}
(h : ∀ (i : ι), Exact (f i) (g i))
:
Products of exact pairs are exact: if Xᵢ → Yᵢ → Zᵢ is exact for every i, then so is the
componentwise pair ∏ᵢ Xᵢ → ∏ᵢ Yᵢ → ∏ᵢ Zᵢ.