Sums of tensor maps differing in one factor

Mathlib's PiTensorProduct.map_update_add says that PiTensorProduct.map is additive in each factor. This file records the form of that statement used when two tensor maps are compared directly: if two families of linear maps agree away from one index k, then the sum of their tensor maps is the tensor map of the family whose k-th factor is the sum of the two k-th factors.

Main results

• TauCeti.PiTensorProduct.map_add_map_eq_map_update: the sum of two tensor maps whose factors agree away from one index.

theorem TauCeti.PiTensorProduct.map_add_map_eq_map_update {ι : Type uι} {R : Type uR} {s : ι → Type us} {t : ι → Type ut} [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f g : (i : ι) → s i →ₗ[R] t i) (k : ι) (h : ∀ (i : ι), i ≠ k → f i = g i) : PiTensorProduct.map f + PiTensorProduct.map g = PiTensorProduct.map (Function.update f k (f k + g k))

Two tensor maps whose factors agree away from one index k add up to the tensor map with the sum of their factors at k.