English
There is a naturality property for oneEquiv with respect to ιMulti: (oneEquiv R M) (ιMulti R 1 f) = f 0.
Русский
Существует естественная совместимость oneEquiv R M с ιMulti: (oneEquiv R M) (ιMulti R 1 f) = f 0.
LaTeX
$$$oneEquiv R M (ιMulti R 1 f) = f 0$$$
Lean4
/-- The linear equivalence `M ≃ₗ[R] ⋀[R]^1 M`. -/
@[simps! -isSimp symm_apply]
noncomputable def oneEquiv : ⋀[R]^1 M ≃ₗ[R] M :=
LinearEquiv.ofLinear (alternatingMapLinearEquiv (AlternatingMap.ofSubsingleton R M M (0 : Fin 1) .id))
(by
have h (m : M) : (fun (_ : Fin 1) ↦ m) = update (fun _ ↦ 0) 0 m :=
by
ext i
fin_cases i
rfl
exact
{ toFun := fun m ↦ ιMulti _ _ (fun _ ↦ m)
map_add' := fun m₁ m₂ ↦ by
rw [h]; nth_rw 2 [h]; nth_rw 3 [h]
simp only [Fin.isValue, AlternatingMap.map_update_add]
map_smul' := fun r m ↦ by
dsimp
rw [h]; nth_rw 2 [h]
simp only [Fin.isValue, AlternatingMap.map_update_smul] })
(by aesop) (by aesop)
