Hopf problem: period family · core 6

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.PeriodFamily.Boundary.EllipticCapKernelWang.map_cover_columns {A : Type u_1} {B : Type u_2} [AddCommGroup A] [Module ℤ A] [AddCommGroup B] [Module ℤ B] (e : A ≃ₗ[ℤ] Fin 2 → ℤ) (L : A →ₗ[ℤ] B) (u v a : A) (c d : ℤ) (hu : e u = ![1, 0]) (hv : e v = ![c, d]) : d • L a = (d * e a 0 - c * e a 1) • L u + e a 1 • L v