Additive equivalences of Pi types

Functions into products are additively equivalent to products of function spaces: a family of pairs regroups into a pair of families. In the torsion decomposition of an elliptic curve, each primary component of E[N] is a product of two cyclic groups; regrouping lets the Chinese remainder theorem reassemble the first and second cyclic factors separately into ZMod N.

Coordinate transport by AddEquiv.arrowCongr inverts by reversing both the coordinate and alphabet equivalences.

Main declarations

• TauCeti.AddEquiv.arrowProdEquivProdArrow: (∀ i, B i × C i) ≃+ (∀ i, B i) × (∀ i, C i).
• AddEquiv.arrowCongr_symm: inversion reverses both equivalences in function transport.

@[simp]

theorem AddEquiv.arrowCongr_symm {ι : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] (e : ι ≃ κ) (f : A ≃+ B) : (arrowCongr e f).symm = arrowCongr e.symm f.symm

Inverting additive function transport reverses the equivalences of both the domain and the codomain.

def TauCeti.AddEquiv.arrowProdEquivProdArrow {ι : Type u_1} (B : ι → Type u_2) (C : ι → Type u_3) [(i : ι) → Add (B i)] [(i : ι) → Add (C i)] : ((i : ι) → B i × C i) ≃+ ((i : ι) → B i) × ((i : ι) → C i)

Functions into products are additively equivalent to products of function spaces.

Equations

• TauCeti.AddEquiv.arrowProdEquivProdArrow B C = { toEquiv := Equiv.arrowProdEquivProdArrow ι B C, map_add' := ⋯ }

@[simp]

theorem TauCeti.AddEquiv.arrowProdEquivProdArrow_apply {ι : Type u_3} (B : ι → Type u_1) (C : ι → Type u_2) [(i : ι) → Add (B i)] [(i : ι) → Add (C i)] (f : (i : ι) → B i × C i) : (arrowProdEquivProdArrow B C) f = (fun (i : ι) => (f i).1, fun (i : ι) => (f i).2)

arrowProdEquivProdArrow maps a function to its two component functions.

@[simp]

theorem TauCeti.AddEquiv.arrowProdEquivProdArrow_symm_apply {ι : Type u_3} (B : ι → Type u_1) (C : ι → Type u_2) [(i : ι) → Add (B i)] [(i : ι) → Add (C i)] (f : ((i : ι) → B i) × ((i : ι) → C i)) : (arrowProdEquivProdArrow B C).symm f = fun (i : ι) => (f.1 i, f.2 i)

The inverse of arrowProdEquivProdArrow pairs component functions pointwise.