# How do I know that these definitions of inner product of $k$-vectors and Hodge star are well-defined?

For my background, I read through Spivak's Calculus on Manifolds up to Integration on Chains.

Let's say $V$ is a finite-dimensional real inner product space with $\dim V=n$.

Take a look at these definitions of inner product of $k$-vectors and Hodge star repsectively:

https://en.wikipedia.org/wiki/Exterior_algebra#Inner_product

https://en.wikipedia.org/wiki/Hodge_isomorphism#Formal_definition_of_the_Hodge_star_of_k-vectors

I feel uneasy about these two definitions of the functions. There are some common features in these definitions: they do not use explicit formula to define the functions*, and they just assume that there are really unique functions that satisfy the respective defining property.

The inner product is slightly better than Hodge star, that we can extend by linearity to calculate, but is the inner product well-defined, that the calculation result is independent of the decomposition of k-vectors? Hodge star is worse, that it is rather defining how $\star\beta$ should interact with other $k$-vectors upon wedge product.

So my questions are:

Do we have to show that the two definitions are well-defined, that there really exist unique functions satisfying the respective defining property? Or are they actually intrinsically well-defined but I don't see it? If we have to show the well-definedness, how should we proceed?

If we have to show the well-definedness, I propose that we should first pick a particular bases for $\wedge^k(V)$ and $\wedge^{n-k}(V)$, say $\{e_{i_1}\wedge...\wedge e_{i_k}:1\le i_1\lt...\lt i_k\le n\}$ and $\{e_{i_1}\wedge...\wedge e_{i_{n-k}}:1\le i_1\lt...\lt i_{n-k}\le n\}$ where $\{e_1,...,e_n\}$ is an orthonormal basis for $V$, then assume such bilinear function/linear map satisfying the respective defining property exist and evaluate the values at the basis. Since the values at the basis are determined, the two functions, if exist, are determined uniquely. To show existence, we simply take the bilinear function/linear map defined by the values at basis and show that they satisfy the respective defining property.

Is there anything wrong with the above argument? Is it circular?

*I clarify what it is meant to have an explicit formula in the context of linear algebra with examples. For instance, for matrix product, we have an explicit formula $\sum_j a_{ij}b_{jk}$ to compute the entries; for tensor product, we can find how $\phi_1\otimes\phi_2$ acts on $(v_1,v_2)$ by the formula $\phi_1\otimes\phi_2(v_1,v_2)=\phi_1(v_1)\phi_2(v_2)$; for alternation, albeit a long formula, we can still calculate with an explicit formula $Alt(T)(v_1,...,v_k)=\frac{1}{k!}\sum_{\sigma\in S_k}T(v_{\sigma(1}),...,v_{\sigma(k)})$. Since tensor product and alternation output functions, I think writing down how the output function acts on $(v_1,...,v_k)$ is already explicit enough.

In case of the scalar product, your problem abstracts to the following: Given a vector space $W$ (In your case $\Lambda^kV$) and a spanning set $S$ of $W$ (in your case the set of all pure tensors) and a function $$\langle \cdot \vert \cdot \rangle_0 : S \times S \rightarrow \mathbb{R},$$ under which conditions is there a bilinear extension $\langle \cdot \vert \cdot \rangle$ of $\langle \cdot \vert \cdot \rangle_0$ to all of $W$? Note that if $S$ is a basis, there is no condition at all. What do you need if this is not the case?
First recall that in order to define the Hodge star you have to choose a nonzero element $\omega \in \Lambda^nV$ (this will later be $*1$). Since $\Lambda^nV$ has dimension $1$ this provides you with an isomorphism to $\mathbb{R}$, to make it explicit: $$F: \Lambda^nV \rightarrow \mathbb{R}, \quad \lambda \omega \mapsto \lambda$$ Now you can define linear maps $$S_j: \Lambda^jV \rightarrow (\Lambda^{n-j}V)^\ast, \quad v \mapsto (S_jv: w \mapsto F(w\wedge v))$$ These maps allow us to rewrite the defining equation $\alpha \wedge \ast \beta = \langle \alpha \vert \beta \rangle \omega$ as follows: $$S_{n-k}(*\beta) = \langle \cdot \vert \beta \rangle$$ I.e. defining $\ast \beta$ amounts to the following problem. Given $\beta \in \Lambda^k V$, does there exist a unique element $\gamma\in\Lambda^{n-k}V$ such that $$S_{n-k}(\gamma) = \langle \cdot \vert \beta \rangle.$$ This question can be answered with yes if and only if the map $S_{n-k}$ are isomorphisms. Prove this!