Splitting off one factor of an Option-indexed tensor product

A tensor product indexed by Option α is the tensor product of the factors indexed by α with the factor at none:

⨂ₒ Pₒ ≃ (⨂ᵢ P (some i)) ⊗ P none,     ⨂ₜ mₒ ↦ (⨂ₜ m (some i)) ⊗ₜ m none.

This is the inductive step in constructions by induction on a finite index type, such as PiTensorProduct.sigmaEquiv and PiTensorProduct.tensorDistribEquiv.

Main definitions

• PiTensorProduct.optionEquiv: splitting off the factor at none of a tensor product indexed by Option α.

Main results

• PiTensorProduct.optionEquiv_tprod and PiTensorProduct.optionEquiv_symm_tmul: the formula on pure tensors in both directions.

noncomputable def PiTensorProduct.optionEquiv {R : Type u} [CommSemiring R] {α : Type x} (P : Option α → Type v) [(o : Option α) → AddCommMonoid (P o)] [(o : Option α) → Module R (P o)] : (PiTensorProduct R fun (o : Option α) => P o) ≃ₗ[R] TensorProduct R (PiTensorProduct R fun (i : α) => P (some i)) (P none)

A tensor product indexed by Option α is the tensor product of the factors indexed by α with the factor at none.

@[simp]

theorem PiTensorProduct.optionEquiv_tprod {R : Type u} [CommSemiring R] {α : Type x} (P : Option α → Type v) [(o : Option α) → AddCommMonoid (P o)] [(o : Option α) → Module R (P o)] (m : (o : Option α) → P o) : (optionEquiv P) ((tprod R) m) = ((tprod R) fun (i : α) => m (some i)) ⊗ₜ[R] m none

Splitting off the factor at none of a pure tensor.

@[simp]

theorem PiTensorProduct.optionEquiv_symm_tmul {R : Type u} [CommSemiring R] {α : Type x} (P : Option α → Type v) [(o : Option α) → AddCommMonoid (P o)] [(o : Option α) → Module R (P o)] (m : (o : Option α) → P o) : (optionEquiv P).symm (((tprod R) fun (i : α) => m (some i)) ⊗ₜ[R] m none) = (tprod R) m

Reattaching the factor at none to a pure tensor.