A single coordinate as a subspace of a dependent product #
def
MagnitudeConjecture.singleCoordinate
{k : Type u_1}
{ι : Type u_2}
[Field k]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(p : ι)
:
Submodule k ((i : ι) → V i)
Vectors vanishing at every coordinate except p.
Instances For
noncomputable def
MagnitudeConjecture.singleCoordinateEquiv
{k : Type u_1}
{ι : Type u_2}
[Field k]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(p : ι)
:
↥(singleCoordinate V p) ≃ₗ[k] V p
Evaluation at p identifies its coordinate subspace with the original vector space.