Lean4
/-- Tensor product of `M` over a singleton set is equivalent to `M`
-/
@[simps symm_apply]
def subsingletonEquiv [Subsingleton ι] (i₀ : ι) : (⨂[R] _ : ι, M) ≃ₗ[R] M
where
toFun := lift (MultilinearMap.ofSubsingleton R M M i₀ .id)
invFun m := tprod R fun _ ↦ m
left_inv
x := by
dsimp only
have : ∀ (f : ι → M) (z : M), (fun _ : ι ↦ z) = update f i₀ z := fun f z ↦
by
ext i
rw [Subsingleton.elim i i₀, Function.update_self]
refine x.induction_on ?_ ?_
· intro r f
simp only [LinearMap.map_smul, LinearMap.id_apply, lift.tprod, ofSubsingleton_apply_apply, this f,
MultilinearMap.map_update_smul, update_eq_self]
· intro x y hx hy
rw [LinearMap.map_add, this 0 (_ + _), MultilinearMap.map_update_add, ← this 0 (lift _ _), hx, ←
this 0 (lift _ _), hy]
right_inv t := by simp only [ofSubsingleton_apply_apply, LinearMap.id_apply, lift.tprod]
map_add' := LinearMap.map_add _
map_smul' := fun r x => by exact LinearMap.map_smul _ r x
