Algebra on the zero-sum representation

The pre-existing ZeroSum n type is the subtype of functions Fin n → ℝ whose coordinates sum to zero. This module equips it with the pointwise additive and real-linear structures and records the coordinate-sum linear map.

def NRR.coordinateSum (n : ℕ) : (Fin n → ℝ) →ₗ[ℝ] ℝ

Sum of all coordinates, as a linear map.

Equations

• NRR.coordinateSum n = { toFun := fun (v : Fin n → ℝ) => ∑ i : Fin n, v i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NRR.coordinateSum_apply {n : ℕ} (v : Fin n → ℝ) : (coordinateSum n) v = ∑ i : Fin n, v i

def NRR.ZeroSum.equivKernel (n : ℕ) : ZeroSum n ≃ ↥(coordinateSum n).ker

Identify zero-sum coordinate vectors with the kernel of coordinate summation.

Equations

• NRR.ZeroSum.equivKernel n = { toFun := fun (v : NRR.ZeroSum n) => ⟨fun (i : Fin n) => ↑v i, ⋯⟩, invFun := fun (v : ↥(NRR.coordinateSum n).ker) => ⟨↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

noncomputable instance NRR.ZeroSum.instAddCommGroup {n : ℕ} : AddCommGroup (ZeroSum n)

Equations

• NRR.ZeroSum.instAddCommGroup = (NRR.ZeroSum.equivKernel n).addCommGroup

@[instance_reducible]

noncomputable instance NRR.ZeroSum.instModule {n : ℕ} : Module ℝ (ZeroSum n)

Equations

• NRR.ZeroSum.instModule = AddEquiv.module ℝ (NRR.ZeroSum.equivKernel n).addEquiv

@[simp]

theorem NRR.ZeroSum.add_apply {n : ℕ} (u v : ZeroSum n) (i : Fin n) : ↑(u + v) i = ↑u i + ↑v i

@[simp]

theorem NRR.ZeroSum.neg_apply {n : ℕ} (u : ZeroSum n) (i : Fin n) : ↑(-u) i = -↑u i

@[simp]

theorem NRR.ZeroSum.sub_apply {n : ℕ} (u v : ZeroSum n) (i : Fin n) : ↑(u - v) i = ↑u i - ↑v i

@[simp]

theorem NRR.ZeroSum.smul_apply {n : ℕ} (c : ℝ) (u : ZeroSum n) (i : Fin n) : ↑(c • u) i = c * ↑u i

instance NRR.ZeroSum.instContinuousAdd {n : ℕ} : ContinuousAdd (ZeroSum n)

instance NRR.ZeroSum.instContinuousNeg {n : ℕ} : ContinuousNeg (ZeroSum n)

instance NRR.ZeroSum.instIsTopologicalAddGroup {n : ℕ} : IsTopologicalAddGroup (ZeroSum n)

instance NRR.ZeroSum.instContinuousSMul {n : ℕ} : ContinuousSMul ℝ (ZeroSum n)

def NRR.ZeroSum.coeLinearMap {n : ℕ} : ZeroSum n →ₗ[ℝ] Fin n → ℝ

The inclusion of the zero-sum representation into the full coordinate space.

Equations

• NRR.ZeroSum.coeLinearMap = { toFun := fun (v : NRR.ZeroSum n) (i : Fin n) => ↑v i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NRR.ZeroSum.coeLinearMap_apply {n : ℕ} (v : ZeroSum n) : coeLinearMap v = fun (i : Fin n) => ↑v i

instance NRR.ZeroSum.instFiniteDimensional {n : ℕ} : FiniteDimensional ℝ (ZeroSum n)

noncomputable def NRR.ZeroSum.linearEquivKer {n : ℕ} : ZeroSum n ≃ₗ[ℝ] ↥(coordinateSum n).ker

The existing zero-sum subtype is linearly equivalent to the kernel of coordinate summation.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.coordinateSum_surjective {n : ℕ} (hn : 0 < n) : Function.Surjective ⇑(coordinateSum n)

Coordinate summation is surjective when there is at least one coordinate.

theorem NRR.ZeroSum.finrank {n : ℕ} (hn : 0 < n) : Module.finrank ℝ (ZeroSum n) = n - 1

Dimension of the standard zero-sum representation.